Explosion and Cut Required

[Tennant, Neil]

Jo,
The relevant notion of validity is relevant validity.
A,~A:# is relevantly valid. A,~A:B is not.
Neil

Get Outlook for iOS<https://aka.ms/o0ukef>
________________________________
From: Joseph Vidal-Rosset <joseph.vidal.rosset at gmail.com>
Sent: Sunday, June 5, 2022 11:19:50 AM
To: Tennant, Neil <tennant.9 at osu.edu>
Cc: Joseph Vidal-Rosset <joseph.vidal.rosset at gmail.com>; Harvey Friedman <hmflogic at gmail.com>; fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: Explosion and Cut Required

Le dim. 06/05/22 juin 2022 à 11:30:45 , « Tennant, Neil » <tennant.9 at osu.edu> a envoyé ce message: Jo, I was simply defining what is meant by “subsequent”. Since you did not realize that, everything you said is a non-sequitur.


Le dim. 06/05/22 juin 2022 à 11:30:45 , « Tennant, Neil » <tennant.9 at osu.edu> a envoyé ce message:

Jo, I was simply defining what is meant by “subsequent”. Since you did not realize that, everything you said is a non-sequitur.

I understood that

[\begin{equation*} \tag{1}  \lnot A, A \vdash  \end{equation*}]

is a « subsequent » of

[\begin{equation*} \tag{2}  \lnot A, A \vdash B  \end{equation*}]

because we have on the left

[\begin{equation*} \tag{3}  \{\lnot A, A\} \subseteq \{\lnot A, A\}  \end{equation*}]

and on the right

[\begin{equation*} \tag{4}  \emptyset \subseteq \{B\}  \end{equation*}]

If this is not what you meant by « subsequent », I am sorry to have misunderstood your subsequent theory.

But the most difficult for me is to understand how a valid sequent like (1) can be, in Core logic, a valid subsequent of an invalid sequent like (2). Note that a set theory based on Johansson’s logic can certainly prove (3), but is inadequate to prove (4) if this truth of set theory is a vacuous truth based on the use of the intuitionistic absurdity rule, as my quotation of Holmes’s proof of this theorem showed this, to contradict also your claim according to which this rule is useless in mathematics. I guess that there are probably other counterexamples of your claim that can be given by mathematicians on this list.

Best wishes,

Jo

PS You did not reply to my suggestion of accepting another rule -> E. I guess that you need time to think about it.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220605/326a69cb/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexgOdpV3_55cae5b97a32df061891bdc023cbb61433a6b01f.png
Type: image/png
Size: 766 bytes
Desc: latexgOdpV3_55cae5b97a32df061891bdc023cbb61433a6b01f.png
URL: </pipermail/fom/attachments/20220605/326a69cb/attachment-0004.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexJx2X5V_b95323a6586b27c329ce20cc1266b8bb1109ceb0.png
Type: image/png
Size: 879 bytes
Desc: latexJx2X5V_b95323a6586b27c329ce20cc1266b8bb1109ceb0.png
URL: </pipermail/fom/attachments/20220605/326a69cb/attachment-0005.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexxcrBZb_39b55c2a58373ebce08d95b0b19885293f785b27.png
Type: image/png
Size: 745 bytes
Desc: latexxcrBZb_39b55c2a58373ebce08d95b0b19885293f785b27.png
URL: </pipermail/fom/attachments/20220605/326a69cb/attachment-0006.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexJhzFmy_dc76b9f351e76c657ff8d5a67b8df172d92cfd56.png
Type: image/png
Size: 616 bytes
Desc: latexJhzFmy_dc76b9f351e76c657ff8d5a67b8df172d92cfd56.png
URL: </pipermail/fom/attachments/20220605/326a69cb/attachment-0007.png>