On the fully rigorous formalization of deductive reasoning in mathematics

[Tennant, Neil]

Let X be the set of axioms of any first-order mathematical theory.

The lemmas, theorems, and corollaries in the theory all rest, ultimately, on members of X.

If you are morally certain that X is consistent (equivalently: has a model), then your proofs of those lemmas, theorems, and corollaries make you certain of their truth in any model of X.

I take it that this much is an agreed starting point among logicians and foundationalists.

Now: the classification of proven results from X as lemmas, theorems, and corollaries is really a subjective matter. From a logical point of view, they are 'on a par'. They are all of them just proven consequences of X.

I want to use the word "theorem", though, to describe any "terminus" of deductive reasoning from X. Call such a terminus T. I shall be looking at proofs of results ("sequents") of the form Y:T, where Y is a finite subset of X. Note that these are all single-conclusion sequents, even in the classical case.

'On the way' to T from Y there could be many an intermediate result. Let us call such results lemmas. Consider a particular lemma L within an overall proof of Y:T.
It would feature thus:

         There would be a proof of a sequent Y1:L (Y1 a subset of X) and
         another proof of a sequent L,Y2:T (Y2 a subset of X).
         Together they would convince the mathematician that T has been
         established from Y1,Y2. That is, s/he would take the argument
         (or sequent) Y1,Y2:T to have been established.

Suppose you are rigorously formalizing the proofs of all known results in any mathematical theory with axiom-set X. You are focusing on some particular theorem T. You would identify all the lemmas involved in proofs 'on the way' to T from axioms in X. This would result in a decomposition of the informally rigorous reasoning into 'internally lemma-free' chunks, establishing sequents of the form (for Y a finite subset of X)

       L1,...Ln,Y:L or (finally) L1,...Ln,Y:T

By soundness of proof, every one of these sequents is truth-preserving. So one can say, respectively,

      X |= L and X |= T

as appropriate. The double turnstile |= of logical consequence does actually satisfy cut:

      Z |= C      C, W |= D
      ________________
             Z,W |= D

But there is no need to apply the Rule of Cut within any sequent proof!

The aforementioned identification of lemmas can be very thorough. Mathematicians might not call a particular intermediate result a lemma. But we logicians can---if we are so minded when formalizing---do that on their behalves, in the interests of complete formalization.

Because proofs are finite, there will be an end to this 'lemma interpolation' process. It can be carried out to the point where---in the context

     Y1:L. and L,Y2:T

---the lemma L is not both the conclusion of an introduction (or step of Classical Reductio, or of Dilemma) in the proof of the sequent Y1:L and the major premise of an elimination in the proof of the sequent L,Y2:T.

This means that all the proofs of the sequents thus identified will be in normal form (if formalized as natural deductions) or cut-free (if formalized as sequent proofs).

The process of fully formal, rigorous codification of the proofs the sequents one has identified can now proceed in (Classical) Core Logic.

There will be no exponential explosion. For no cuts-within-proofs will be performed, and therefore no cut-elimination will need to take place.

Moreover, the core proofs involved will actually be shorter than the normal proofs in Gentzen-style natural deduction, or, respectively, shorter than the cut-free proofs in the sequent calculus. This is because the Gentzenians will be insinuating unnecessary steps of EFQ in the former, and unnecessary steps of Thinning on the Right in the latter. The Core logician, by contrast, can simply cut to the chase (please excuse the pun) by applying the Core rules, which do not need those "toppings up" supplied by EFQ (resp., by Thinning on the Right).

Once again, I wish to emphasize: Classical Core Logic is adequate for the fully rigorous formalization of the classical mathematical reasoning that you actually find in the mathematical literature.

Neil


[The Ohio State University]
Neil Tennant
Arts & Sciences Distinguished Professor in Philosophy
Distinguished University Scholar
College of Arts & Humanities Department of Philosophy
322 University Hall, 230 North Oval Mall, Columbus, OH 43210
614-292-7914 Office

tennant.9 at osu.edu<mailto:tennant.9 at osu.edu> u.osu.edu/tennant.9/<http://u.osu.edu/tennant.9/.osu.edu>

To appear in early 2022:
<https://urldefense.com/v3/__https:/global.oup.com/academic/product/the-logic-of-number-9780192846679?q=tennant&lang=en&cc=gb__;!!KGKeukY!ggJbW10iBUYMMKcoCgolseYFg2BwL2R-IuyEKmcEjVXk0cUP3-4HF1qYhSHh1Ztv$>The Logic of Number<https://global.oup.com/academic/product/the-logic-of-number-9780192846679?q=tennant&lang=en&cc=gb>



Land Acknowledgment: The Ohio State University occupies the ancestral and contemporary lands of the Shawnee, Potawatomi, Delaware, Miami, Peoria, Seneca, Wyandot, Ojibwe, and Cherokee peoples. The university resides on land ceded in the 1795 Treaty of Greeneville and the forced removal of tribal nations through the Indian Removal Act of 1830.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220528/90094be6/attachment-0001.html>