Explosion and Cut Required - Inference Systems
Joseph Vidal-Rosset
joseph at vidal-rosset.net
Fri Jun 17 11:15:38 EDT 2022
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.
More information about the FOM
mailing list