Explosion and Cut Required
Joseph Vidal-Rosset
joseph.vidal.rosset at gmail.com
Sun Jun 5 04:56:41 EDT 2022
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.
More information about the FOM
mailing list