Proof by Contradiction / EFQ

[Tennant, Neil]

Curtis Franks writes:

'In Core Logic, EFQ isn't needed because the "liberalized" v-Elimination inference can just proceed with one or more subproof ending in C and the others ending in contradictions. The question remains, though: Can these proofs be (effectively) rewritten so that the liberalized v-Elimination isn't needed (for that still counts as "proof by contradiction" as HF is using the phrase).'

Certainly not all such proofs can be rewritten in this way. As a counterexample consider the Core proof of Disjunctive Syllogism, using the liberalized v-Elimination:

                           __(1)
                   ~A    A
                   ______    __(1)
     AvB            #          B
     _________________(1)
                       B

I do not see how this proof can count as a "proof by contradiction" in Harvey's sense. It does not use EFQ at any step. EFQ is not a rule of inference in the natural-deduction system of Core Logic. Correspondingly, the sequent system of Core Logic does not allow Thinning (on either the left or the right).

Curtis continues:

'Notice that HF is not asking for a proof that doesn't use EFQ: A fully classical proof is fine.'

But my impression--please correct me if it is mistaken--was that Harvey had clarified that what he meant by "proof by contradiction" was "proof by appeal to EFQ". (Indeed from the first quote from Curtis above, he seems to recognize this point.) As far as Core Logic itself is concerned--which has no strictly classical rules such as Classical Reductio, or Dilemma--the debate over liberalized v-Elimination is thereby focused on EFQ.

The whole motivation behind Core Logic was to ensure relevance of premises to conclusions of proofs, while also remaining constructive (as a relevant subsystem of Intuitionistic Logic). This involved subtly tweaking Gentzen's original formulation of the rules of Introduction and Elimination for the logical operators so as to ensure relevance of inferences, and fully respect the meanings of the logical operators without appealing to EFQ. Careful inspection of the formal rules of Core Logic will show that they enshrine the left-to-right readings of the familiar truth tables.

Because Gentzen insisted that the two case-proofs for v-Elimination had to have exactly the same conclusion, he was forced to include EFQ in order to be able to prove Disjunctive Syllogism. But the truth table for v delivers the insight that the truth of  AvB, when A is false, requires the truth of B---hence also the truth of any consequence of B (modulo possible side-assumptions). The liberalized v-Elimination rule simply formalizes that insight. No appeal to EFQ is called for.

Likewise, because Gentzen formulated ->-Introduction with the tacit insistence that the immediate subproof have as its conclusion the consequent of the conditional being inferred, he was forced to include EFQ in order to be able to deduce A->B from ~A. But the truth table for -> delivers the insight that the falsity of A (all by itself) secures the truth of A->B, regardless of the truth-value of B. This insight is formalized in Core Logic by the new part it provides for the rule of ->-Introduction. This new part allows one to conclude A->B, thereby discharging assumption A, upon having reduced A to absurdity (modulo side assumptions). No appeal to EFQ is called for "to get B into the picture" before applying Gentzen's unliberalized form of ->-Introduction.

Core Logic is what one arrives at by thanking Gerhard sincerely for the framework of natural deduction, but tipping one's hat to Gottlob for the truth tables; and consequently tweaking v-Elimination and  ->-Introduction as just described. The Core Logician also politely declines EFQ in a belated reproach to logicians from Peter [Abelard] through to Lutyens and Arend for having muddied the logical waters with it.

Classical Core Logic is then obtained by adding relevantized versions of Classical Reductio or Dilemma to Core Logic.

Neil Tennant
________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Curtis Franks <Curtis.D.Franks.7 at nd.edu>
Sent: Wednesday, May 18, 2022 9:31 PM
To: fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: Proof by Contradiction / EFQ

Some of the discussion about Harvey Friedman's question is jumbled because by "proof by contradiction" many readers assume he is referring to the method of establishing a conclusion (C) by assuming its negation and deriving a

Some of the discussion about Harvey Friedman's question is jumbled because by "proof by contradiction" many readers assume he is referring to the method of establishing a conclusion (C) by assuming its negation and deriving a contradiction. He is instead referring to the use of the ex falso quodlibet (EFQ) principle in a specific context: at one or more of the penultimate steps of a proof by cases. What he has asked about is a proof transformation procedure that will remove all instances of these ex falso quodlibet steps. I don't think Neil Tennant meant for his last message to contribute to this question, but it is related: In Core Logic, EFQ isn't needed because the "liberalized" v-Elimination inference can just proceed with one or more subproof ending in C and the others ending in contradictions. The question remains, though: Can these proofs be (effectively) rewritten so that the liberalized v-Elimination isn't needed (for that still counts as "proof by contradiction" as HF is using the phrase). Notice that HF is not asking for a proof that doesn't use EFQ: A fully classical proof is fine. On the other hand, simply replacing instances of EFQ with the classical "assume ~C, get a contradiction however you got one before, infer ~~C, and conclude C" (what is ordinarily called proof by contradiction") shouldn't suffice either and would return a proof that still qualifies as a "proof by contradiction" in HF's sense. I think the goal is to eliminate the contradictory cases themselves.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220520/c5c5df11/attachment-0001.html>