Explosion and Cut Required - Inference Systems

[Joseph Vidal-Rosset]

Le 17/06/2022 à 10:25, Mario Carneiro a écrit :

>>     In ND
>>    for Core logic
>>
>>        B
>>    ------ -> I
>>    A -> B
>>
>>     is allowed, by contrast with
>>
>>        bot
>>    --------- -> I
>>     A -> bot
>>
>>    which is not allowed in Core logic.

> Those are both allowed.

No, they are not both allowed, you are wrong!

See for example "Autologic", p. 189, where  Tennant repeats that IR
“requires non-vacuous discharge of assumptions,” but he adds in footnote
6 on the same page, “except, crucially, in one half of the rule of
implication introduction!” This means that it is only for the other half
of implication introduction (i.e. for the conditional introduction rule
that allows the derivation of
~A |- A->B ) that vacuous discharge (i.e. weakening) is forbidden.

When you wrote

x, ((a -> b) -> b) |- b
-----------------------
x, a |- b/#

to contest that the invertibility of DNS.1 is provable in Core logic, I
am afraid you show that the Core logician falls into formal sophistry. I
understand that this means that if {x,a} is inconsistent, then # instead
of b, in other words, the conclusion is  x, a |- b if and only if
x, a |/- # .  But nothing is farther from the transparency and the
automated deduction of mathematical logic.

I prefer to stop this discussion now, because we are in a dead end, like
if  you persisted in denying  that 1 + 1 = 2. Finally, you show that
there is not a big difference between the dialetheist and the Core
logican, too bad for the latter.

All the best,

Jo.