Explosion and Cut Required

[Joseph Vidal-Rosset]

Hello Neil, hello everyone,

Many thanks Neil for your patience, and congratulations for your bravery
to defend your Core logic work. :)

Le   dim.   06/05/22   juin   2022  à   12:45:51   ,   "Tennant,   Neil"
<tennant.9 at osu.edu> a envoyé ce message:

>      X |- A    A,Y |- B
>      _____________
>           X,Y |- B/#
>
> But this  is a potentially  misleading graphic display, since  it does
> not get  the logical form  of the metalinguistic  statement absolutely
> right. It serves, however, to  give expression to the ADMISSIBILITY of
> "cut with epistemic gain". Note that if Z' is a subset of Z, then Z':#
> counts as a subsequent of Z:B.

It seems to  me that the problem  is what you wrote  cannot be justified
without the use of Ex  Contradictione Quodlibet. Indeed, Z':# means that
Z' is a  set of contradictory formulas, and  if Z' is a subset  of Z, it
means that  there is  a contradiction  in Z. So,you  claim that  Z':# is
always a subsequent of Z:B, whenever Z' is a subset of Z. Now, assume Z'
= Z. It is  true that every set is a subset of  itself. Then translating
your claim in sequent calculus  style and reading the derivation *from
bottom to top* and one gets:

{#}:#
-----
{#}:B

i.e.

----Ax.
#:#
----
#:B

that is exactly the intuitionistic absurdity rule, i.e. ECQ.

Q.E.D.

About  set theory,  it should  be noted  Holmes's proof  of the  theorem
according to which the empty set is a subset of any set A: "If x is an
element  of  {}  ...  (anything,  including  "x  is  an  element  of  A"
follows).  (Elementary Set  Theory with  a Universal  Set, p.  22). Same
proof developed by Mauro Allegranza here:
https://math.stackexchange.com/questions/656331/why-is-the-empty-set-a-subset-of-every-set
It  is a  vacuous truth  that  is a  truth proved  semantically via  the
implication "false => C". I remind that the Core logician justifies also
the fact that
¬A: A -> B
and
:¬A -> (A -> B)
are  valid in  Core logic,  because Core  logic is  respectful of  truth
tables (a claim  that is *not* genuinely intuitionistic). So  we have in
Core logic, with top=true and bot=false:
bot: top -> B
and
:bot -> (top -> B)
but
top,bot:B
is unprovable.

Last, there  is a lack  of harmony in Core  logic: indeed, in  there are
*two introduction rules  for conditional* in this system,  but only *one
elimination rule* for this connective,  and that is certainly the reason
of many puzzles.

I suggest  therefore this  new rule  -> E  for natural
deduction in Core logic that is a second rule -> E for this system:

X -> C        X
--------------- -> E
        #

if and only if X:#

and I  wonder why, Neil,  the reason why you  did adopt this  rule for
your  logical system,  because it  seems to  me that  it fits  with your
admissible restricted Cut rule for Core logic.

You are the  father of this logical system, therefore  you'll see better
than me  if this rule  can help your child;  unless you think,  like all
parents, that your child is and has always been perfect. ;)

All the best,

Jo.