Explosion and Cut Required - Inference Systems

dennis.hamilton at acm.org dennis.hamilton at acm.org
Thu Jun 16 12:55:44 EDT 2022

-----Original Message-----
From: FOM <fom-bounces at cs.nyu.edu> On Behalf Of Joseph Vidal-Rosset
Sent: Wednesday, June 15, 2022 16:08
Subject: Re: Explosion and Cut Required

> Le 15/06/2022 à 19:20, dennis.hamilton at acm.org a écrit :
>>> -----Original Message-----
>>> ]I pointed out to you that this argument is valid in minimal logic,
>>> because it is provable in minimal logic as in Core logic that
 >>>  A -> B, B -> A |- (~B -> ~A) & (~A -> ~B)
>>>  Semantically, the above sequent is transparent: it says, if A is
>>> true if  and only if B is also true (that is to say, A and B are
>>> equivalent), therefore  B is false if and only if A is false. Let us
>>> replace A and B respectively by  top (the truth constant) and ~bot
>>> (the negation of the absurdity constant), we
>>>  have:
>>  top -> ~bot,  ~bot -> top |- (~ ~bot -> ~top) & (~top -> ~ ~ bot)
>>[ ... ]
>> This strikes me as sleight of hand.
>> The first deduction is consistent with the definition of
>> bi-conditional, equivalence.  It is effectively by definition.
>> But arbitrary substitutions do not hold.  Substitutions of constants
>> for A and B in *premises* do not work unless the premises remain
>> sound.  > I suggest that all you have shown is that the substitutions
>> you make are unsound and cause inconsistency.
>> No surprise.

> If you talk about this substitution in my paper online  ( 
> https://www.vidal-rosset.net/paraconsistent_tennants_logic_is_inconsistent.html
), where A is interpreted by this sequent

> [orcmid] long employment of inference system omitted ....

> I do not see the least unsoundness in this substitution: because it is 
> provable that sequent A and sequent B are interderivable (equivalent), then 
> it is provable that the respective antisequents are interderivable too.

>> The same injuries arise from proffered deductions such as
>> A, ~A |- anything (including A & ~A)
>> when the law of excluded middle is axiomatic.

>Because it is indeed provable that the intuitionistic absurdity rule  is 
>derivable in classical logic, I do not understand your analogy.

>> The parading of deduction schemes strikes me as a smoke screen, as in
>> well-known demonstrations that 0 = 1 after sneaking in 0 as a divisor.
>> I don't understand why it is not just this simple.

[orcmid] > I am sorry to tell you that analogies, suggestions and feelings 
cannot be considered as rebuttals.

It's this simple.

In a logical system, given a claim,

      P1, p2, ..., pn |- s

If (p1) & (p2) & ... & (pn) is not satisfiable, there is *nothing* 
**derivable**  from such premises.

It might as well be

                   bot |- s

i.e.,                 ? |- s

since logical constants seem to be allowed and Tarski can be smiling down at 

And, of course, if the conjunction of premises is tautological, the claim 
would be tantamount to

                     ?  |- s

simply               |- s

I do not need to know the system of inference to know that, for a recognizable 
logic that is sufficient for well-known propositional situations, 
unsatisfiable conjunctions of premises do not justify deduction of anything 

Perhaps the system of inference (and associated logic?) is under-specified, 
admitting such mishaps tantamount to ? |- s.  I do not know.  I am reluctant 
to consider that Tennant is so careless.

I do know that there is a well-known label for computational procedures 
(including inference rules taken as such) that do not reject such things.  It 
is called "garbage-in, garbage-out."

 I trust that I am being specific enough now.


 - Dennis

More information about the FOM mailing list