Explosion and Cut Required - Inference Systems

[Joseph Vidal-Rosset]

Hello Mario and hello everyone,

Le ven. 06/17/22 juin 2022 à 01:12:10 , « Mario Carneiro » <di.gama at gmail.com> a envoyé ce message:

> It is tiresome for me as well, but I’m not sure how else to resolve the situation. This is why you should do your proofs formally; so many of these issues seem to simply be type errors that a bit of formalization would solve.

First many thanks to you and also to the FOM editors who accepted to publish this discussion.

I thought about your arguments yesterday evening, and I realized that I was too impressed with your confidence in your rebuttal of my argument.

First, I persist in saying that this use of Cut in my paper online:

[\[
\AxiomC{}
\RightLabel{$\scriptsize{Ax.}$}
\UnaryInfC{$\varphi \vdash \varphi$}
\AxiomC{}
\RightLabel{$\scriptsize{Ax.}$}
\UnaryInfC{$\psi \vdash \psi$}
\RightLabel{$\scriptsize{L\to}$}
\BinaryInfC{$\varphi, \varphi \to \psi \vdash \psi$}
\RightLabel{$\scriptsize{R\to}$}
\UnaryInfC{$\varphi \vdash (\varphi \to \psi) \to \psi$}
\AxiomC{$\Delta, \varphi \vdash \psi $}
\RightLabel{$\scriptsize{R \to}$}
\UnaryInfC{$\Delta \vdash \varphi \to \psi$}
\AxiomC{}
\RightLabel{$\scriptsize{Ax.}$}
\UnaryInfC{$\psi \vdash \psi$}
\RightLabel{$\scriptsize{L\to}$}
\BinaryInfC{$ \Delta, (\varphi \to \psi) \to \psi \vdash \psi$}
\RightLabel{$\scriptsize{Cut}$}
\BinaryInfC{$\Delta, \varphi \vdash \psi $}
\DisplayProof
\]]

is perfectly valid in Core logic. Pay attention to [\(\Delta,
\varphi \vdash \psi\)] on the top, please. You do not contest the top-bottom derivation of DNS.1, therefore you cannot contest the conclusion of this Cut, because this conclusion is exactly the premise you just admitted. You cannot say « B can degenerate to #.

Second point, DNS.1 (like DNS tout court in minimal logic) says nothing about the consistency or inconsistency of premises, because context [\(\Delta\)] can be void and it is provably invertible, even without context:

A |- B ================== ((A -> B) -> B) -> B

SEQUENT 1: ((a -> b) -> (((a -> b) -> b)-> b)) & ((((a -> b) -> b)-> b) -> (a -> b))

a -> b ASSUMPTION
(a -> b) -> b ASSUMPTION
b arrowE
((a -> b) -> b) -> b arrowI
(a -> b) -> (((a -> b) -> b) -> b) arrowI
((a -> b) -> b) -> b ASSUMPTION
a ASSUMPTION
a -> b DoubleNegation
b arrowE
a -> b arrowI
(((a -> b) -> b) -> b) -> (a -> b) arrowI

((a -> b) -> (((a -> b) -> b) -> b)) & ((((a -> b) -> b) -> b) -> (a -> b)) &I

Therefore, the Core logician can neither reject the invertibility of DNS.1, nor its logical consequence that is anti-DNS.1 and the conclusion that the claim of antisequent ~A, A|/- entails a contradiction in Core logic.

Best wishes,

Jo.

PS Not online this week-end.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220618/02857f6a/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexCBbmrG_67235daac75c83e28cbb47e3be48526f71bfad9b.png
Type: image/png
Size: 240 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220618/02857f6a/attachment-0003.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexoIxa6D_a8149481f2f956594a1fc4f2b6ea8a4543c6b6d5.png
Type: image/png
Size: 486 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220618/02857f6a/attachment-0004.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latex416ORc_63ca83eca196a5fb9b09a64810621ed2ce4009eb.png
Type: image/png
Size: 3722 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220618/02857f6a/attachment-0005.png>