Explosion and Cut Required
Joseph Vidal-Rosset
joseph.vidal.rosset at gmail.com
Sun Jun 5 11:19:50 EDT 2022
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/21c428a8/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexgOdpV3_55cae5b97a32df061891bdc023cbb61433a6b01f.png
Type: image/png
Size: 766 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220605/21c428a8/attachment-0004.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexJx2X5V_b95323a6586b27c329ce20cc1266b8bb1109ceb0.png
Type: image/png
Size: 879 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220605/21c428a8/attachment-0005.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexxcrBZb_39b55c2a58373ebce08d95b0b19885293f785b27.png
Type: image/png
Size: 745 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220605/21c428a8/attachment-0006.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexJhzFmy_dc76b9f351e76c657ff8d5a67b8df172d92cfd56.png
Type: image/png
Size: 616 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220605/21c428a8/attachment-0007.png>
More information about the FOM
mailing list