# 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...
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>