On the fully rigorous formalization of deductive reasoning in mathematics

Tue May 31 03:08:58 EDT 2022

Your argument seems to be that one can separate any proof involving cut
into a bunch of subtrees, each internally not containing cut, which are
metatheoretically glued together by Cut. But isn't it a bit unsatisfactory
for the theory if it can't validate such "gluing" itself? We just end up
with a bag of proof-pieces and some instructions saying "some assembly
required", but Core logic itself can only perform the gluing at great
cost.  The rigorous development of a mathematical topic would like to
encode both the proof-pieces and also the connections between them, not
losing track of which ones prove which other ones. So you end up needing
another proof system on top of the Core logic proof system.

I think this amounts to saying "any theorem can be expressed as a cut-free
proof except for the cuts", which is obviously true but not obviously
helpful.

Mario Carneiro

On Mon, May 30, 2022 at 5:27 PM Tennant, Neil <tennant.9 at osu.edu> wrote:

> 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
>
> [image: 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 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/20220531/e203893f/attachment-0001.html>