Explosion and Cut Required

[Joseph Vidal-Rosset]

Le   dim.   06/05/22   juin   2022  à   06:52:15   ,   "Tennant,   Neil"
<tennant.9 at osu.edu> a envoyé ce message:
> Jo,
> The relevant notion of validity is relevant validity.
> A,~A:# is relevantly valid. A,~A:B is not.
> Neil

Hello Neil, hello everyone,

This is an  irrelevant answer, because it is not  logical relevance that
is at  stake here. Nobody contests  that A,~A:# is relevantly  valid and
that A,~A:B is not. My point about these sequent is that, with
Heyting's logic,  both are claimed,  while with Johansson's  logic, only
the  former  is  valid,  which  means  also  A,~A:#  cannot  be  said  a
"subsequent"  of A,~A:B,  because the  assertion of  such a  relation is
finally based on the use of the intuitionistic rule of absurdity.

Now, reading "Core logic" p. 316, I  see that you will reply that ~A,A:#
is *perfectly*  valid and that is  this "more exigent notion  of sequent
validity"  that   is  Core  logician's.  "Perfectly"   for  you  means
"relevantly". The  trouble is it  is indisputable that we  find again,
even with this more "exigent notion of sequent validity", a difference
in treatment between  what concerns sequents with  an inconsistent set
of premises, and others. I quote the end of page 316:

#+begin_quote
3.  If  \(\Delta\)  is  unsatisfiable   but  every  proper  subset  of
   \(\Delta\) is  satisfiable, then the  sequent \(\Delta :  \bot\) is
   perfectly valid.
4. If \(\Delta : \psi\) is  perfectly valid, then some atomic sentence
   occurs within some member of \(\Delta\) and within \(\psi\).
#+end_quote

If I  understand correctly  your English,  it seems  to me  that with
claim 4,  \(\Delta :  \psi\) is said  "perfectly valid",  because some
atomic sentence  occurs within  some member  of \(\Delta\)  and within
\(\psi\),  by contrast  with \(\Delta  : \bot\)  that is  is perfectly
valid, "tout  court". And I guess  that you would reject  the validity
(perfect or not)  of \(\bot : B\) or  that of \(\lnot A, A  : B\). But
now, I  wonder how the  Core logician can  justify the theorem  of set
theory according to which \(\{\} \subset C\) for every set /C/?

Last, I repeat  that it seems to me that  such presupposed distinction
between consistent set of premises and inconsistent set of premises do
not  allow  to  the  Core   logician  to  state  consistency  theorems
independently of Gentzen's,  for example, and that  such a distinction
is not  in agreement with  the usual  rule of sequents  systems, where
nothing  is said  about the  consistency  or inconsistency  of set  of
premises.

All the best,

Jo.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexwUdC86_3d6b2005b1d888f7e61b2d246053a95c93fd1826.png
Type: image/png
Size: 433 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0013.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexmWDfoa_00c2b98573eb83f456066cb863572669100d8d1a.png
Type: image/png
Size: 489 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0014.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexNX074f_41d33a1564a6fec774213911aeacaedab88b02c9.png
Type: image/png
Size: 339 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0015.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexmdfrNo_f1db6282935e1f6c0545910ea6e6fe31cee6af78.png
Type: image/png
Size: 297 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0016.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexpfU6Lv_0dc89834f3dd07706f797fb74d1aed197b731392.png
Type: image/png
Size: 258 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0017.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexlo7KKR_67235daac75c83e28cbb47e3be48526f71bfad9b.png
Type: image/png
Size: 240 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0018.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexsEzyGn_b57cd65daf1217c38aad5cfde68b3a2a5384b265.png
Type: image/png
Size: 368 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0019.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexlX2y0x_0dc89834f3dd07706f797fb74d1aed197b731392.png
Type: image/png
Size: 258 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0020.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexrSAYew_67235daac75c83e28cbb47e3be48526f71bfad9b.png
Type: image/png
Size: 240 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0021.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexpdgUpt_ffe7bdb88782f193b1c6bb818f34d42e46a5d2df.png
Type: image/png
Size: 368 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0022.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexzutcv8_dc9639445a526fda3041df4c73712601e4fecfd7.png
Type: image/png
Size: 297 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0023.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latex9L8FOX_67235daac75c83e28cbb47e3be48526f71bfad9b.png
Type: image/png
Size: 240 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0024.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: latexlVQ2OE_67235daac75c83e28cbb47e3be48526f71bfad9b.png
Type: image/png
Size: 240 bytes
Desc: not available
URL: </pipermail/fom/attachments/20220606/5174ed06/attachment-0025.png>