EFQ
Joseph Vidal-Rosset
joseph.vidal.rosset at gmail.com
Sat May 21 09:48:36 EDT 2022
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/2187f8e7/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexlsjUyd_ecbcd2d3ebd7cddcd80aded48ead399ab20de386.png
Type: image/png
Size: 724 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0007.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latex6cUxXv_c5befcd1b17b1063f9aceb8de088415d99d6aaf7.png
Type: image/png
Size: 1069 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0008.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexukbkvj_627419bc413dbb5abc3719985262daf8a1d7e81e.png
Type: image/png
Size: 2003 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0009.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexQosgz4_c5befcd1b17b1063f9aceb8de088415d99d6aaf7.png
Type: image/png
Size: 1069 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0010.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexxNx68f_5af1842c82a00d73cbab77fdd941eccb37f707c6.png
Type: image/png
Size: 748 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0011.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexcTwexC_2d30f86112d583d24df488d67a4b806bf35e9418.png
Type: image/png
Size: 1068 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0012.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latex92r5FH_612c5935548bf8d5cf0da1d0ba2c2f3734c2c137.png
Type: image/png
Size: 2153 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220521/2187f8e7/attachment-0013.png>
More information about the FOM
mailing list