EFQ

[Joseph Vidal-Rosset]

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>