Explosion and Cut Required

[Joseph Vidal-Rosset]

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>