EFQ
Tennant, Neil
tennant.9 at osu.edu
Sat May 21 14:44:08 EDT 2022
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>
More information about the FOM
mailing list