EFQ

[Tennant, Neil]

Jo (and all)--

Let P1 be the obvious Core proof of the Core theorem ((AvB)&~A)->B. Note that P1 ends with ->-Introduction.
Let P2 be the proof you have given of the conclusion B from the set {((AvB)&~A)->B, A, ~A} of assumptions.
Note that P2 has ((AvB)&~A)->B as a major premise for its terminal step of ->-Elimination.

Your mistake is to think that you now have a Core proof of B from the set {A, ~A}.

You think that by putting P1 "on top of" P2 you will obtain a Core proof of B from the set {A, ~A}. But you will not. At the "grafting point" of the two proof-trees you have ((AvB)&~A)->B standing as the conclusion of ->-Introduction and as the major premise for a step of ->-Elimination.

This violates a crucial condition on Core natural deductions: their MPEs must "stand proud", with no non-trivial proof-work above them.

In sequent-terminology, you are treating ((AvB)&~A)->B as a Cut-formula. The  sequent version of P1 proves the sequent
          emptyset : ((AvB)&~A)->B
while the sequent version of P2 proves the sequent
          ((AvB)&~A)->B, A, ~A : B .

But sequent proofs in Core Logic have to be both Cut-free and Thinning-free.

So you cannot get a sequent proof of A,~A : B .

In my RSL papers and book on Core Logic it is explained how this apparent "failure" of Cut in more than compensated for by the epistemic gain involved in obtaining a proof of some subsequent of the overall target sequent of a cut.

Whether one is dealing with natural deductions or sequent proofs, the method is the same. There is a computable binary function [P1,P2] on (Classical) Core proofs that can be applied when P1 establishes a sequent X:A and P2 establishes a sequent A,Y:B.  The reduct [P1,P2] will establish a subsequent of the target sequent X,Y:B.

In the case at hand, [P1,P2] establishes the sequent A,~A:#, which is a (proper) subsequent of A,~A:B. Note the epistemic gain this furnishes. By applying the binary function [_,_] you  discover that the would-be premise set of the target sequent is inconsistent.

The inconsistency is of course obvious in such a degenerate example.

In more complicated deductive environments, however, the inconsistency might  be "hidden", and not at all obvious. One might have proved a lemma A from axioms X with one's proof P1, and then used the lemma A with further axioms Y to prove B with one's proof P2.  Where the reduct [P1,P2] establishes a proper subsequent of the target sequent X,Y:B, learning of such epistemic gain can be crucial. This is especially the case where X and Y are sets of axioms in a mathematical theory of whose inconsistency you were formerly unaware. If [P1,P2] establishes X',Y':# (for subsets X' of X, and Y' of Y), you will have learned that your overall axiom-set for your would-be mathematical theory is inconsistent.  Moreover if [P1,P2] establishes X',Y':B (where either X' is a proper subset of X, and/or Y' is a proper subset of Y), then that too can be epistemically gainful; for you will have learned that one can derive the mathematical theorem B from a potentially logically weaker set of the permitted mathematicl axioms.

As has been said over and over: Core natural deductions are in normal form, because all their MPEs stand proud; and Core sequent proofs contain no cuts or thinnings, because in them only the left- and right-rules for the logical operators find application. But "cut" is admissible for Core proofs (including classical ones), affording potential epistemic gain.

These properties of [Classical] Core Logic ensure that it is adequate for the formalization of all deductive reasoning in [classical or] constructive mathematics.

Best regards,
Neil
________________________________
From: Joseph Vidal-Rosset <joseph.vidal.rosset at gmail.com>
Sent: Saturday, May 21, 2022 9:48 AM
To: Tennant, Neil <tennant.9 at osu.edu>
Cc: Arnon Avron <aa at tauex.tau.ac.il>; Lawrence Paulson <lp15 at cam.ac.uk>; fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: EFQ

Hello Neil, hello everybody, I am afraid that the liberalisation of disjunction elimination rule in Core logic cannot eliminate the following problem. It is well known that this deduction: can be understood as showing that, ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍ ‍


Hello Neil, hello everybody,

I am afraid that the liberalisation of disjunction elimination rule in Core logic cannot eliminate the following problem. It is well known that this deduction:

[\[  \AxiomC{$((A \lor B) \land D) \to C$}  \AxiomC{$A$}  \RightLabel{\scriptsize{$\lor I$}}  \UnaryInfC{$A \lor B$}  \AxiomC{$D$}  \RightLabel{\scriptsize{$\land I$}}  \BinaryInfC{$(A \lor B) \land D$}  \AxiomC{\scriptsize{1}}  \noLine  \UnaryInfC{$C$}  \RightLabel{\scriptsize{$\to E, 1$}}  \TrinaryInfC{$C$}  \DisplayProof  \]]

can be understood as showing that, if there is a proof of the major premiss, then C is also deducible only from {A,D} and it is inconsistent to claim both

[\begin{equation*} \tag{1}  ((A \lor B) \land D) \to C  \end{equation*}]

and

[\begin{equation*} \tag{2}  A, D \nvdash C  \end{equation*}]

Now, because

[\begin{equation*} \tag{3}  ((A \lor B) \land \lnot A) \to B  \end{equation*}]

is a theorem in Core logic (that corresponds to the sequent called « Disjunctive Syllogism »), the Core logician meets a serious problem when D and C are replaced respectively by ¬ A and B. Indeed, we get:

[\[  \AxiomC{$((A \lor B) \land \lnot A) \to B$}  \AxiomC{$A$}  \RightLabel{\scriptsize{$\lor I$}}  \UnaryInfC{$A \lor B$}  \AxiomC{$\lnot A$}  \RightLabel{\scriptsize{$\land I$}}  \BinaryInfC{$(A \lor B) \land \lnot A$}  \AxiomC{\scriptsize{1}}  \noLine  \UnaryInfC{$B$}  \RightLabel{\scriptsize{$\to E, 1$}}  \TrinaryInfC{$B$}  \DisplayProof  \]]

a deduction that can be understood as showing that, because there is a Core proof of the major premiss, then B is also deducible only from {A, ¬A} and it is provable that it is inconsistent to claim in Core logic both

[\begin{equation*} \tag{3}  ((A \lor B) \land \lnot A) \to B  \end{equation*}]

and

[\begin{equation*} \tag{4}  A, \lnot A \nvdash B  \end{equation*}]

If I am not mistaken, the conclusion seems therefore to be that, to avoid « the First Lewis’s Paradox », the Core logician is also constrained to reject Prawitz’s inversion principle (that is a basic principle for normalization of proofs in natural deduction)…

Best wishes,

Jo.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexlsjUyd_ecbcd2d3ebd7cddcd80aded48ead399ab20de386.png
Type: image/png
Size: 724 bytes
Desc: latexlsjUyd_ecbcd2d3ebd7cddcd80aded48ead399ab20de386.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0007.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latex6cUxXv_c5befcd1b17b1063f9aceb8de088415d99d6aaf7.png
Type: image/png
Size: 1069 bytes
Desc: latex6cUxXv_c5befcd1b17b1063f9aceb8de088415d99d6aaf7.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0008.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexukbkvj_627419bc413dbb5abc3719985262daf8a1d7e81e.png
Type: image/png
Size: 2003 bytes
Desc: latexukbkvj_627419bc413dbb5abc3719985262daf8a1d7e81e.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0009.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexQosgz4_c5befcd1b17b1063f9aceb8de088415d99d6aaf7.png
Type: image/png
Size: 1069 bytes
Desc: latexQosgz4_c5befcd1b17b1063f9aceb8de088415d99d6aaf7.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0010.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexxNx68f_5af1842c82a00d73cbab77fdd941eccb37f707c6.png
Type: image/png
Size: 748 bytes
Desc: latexxNx68f_5af1842c82a00d73cbab77fdd941eccb37f707c6.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0011.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexcTwexC_2d30f86112d583d24df488d67a4b806bf35e9418.png
Type: image/png
Size: 1068 bytes
Desc: latexcTwexC_2d30f86112d583d24df488d67a4b806bf35e9418.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0012.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latex92r5FH_612c5935548bf8d5cf0da1d0ba2c2f3734c2c137.png
Type: image/png
Size: 2153 bytes
Desc: latex92r5FH_612c5935548bf8d5cf0da1d0ba2c2f3734c2c137.png
URL: </pipermail/fom/attachments/20220521/f2236657/attachment-0013.png>