Explosion and Cut Required - Inference Systems

[dennis.hamilton at acm.org]

-----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 
us.

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 
whatsoever.

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.

Regards,

 - Dennis