Proof by Contradiction / EFQ

[Curtis Franks]

I /think/ what HF is asking about when he says both that he wants a sort of
rewrite procedure that eliminates what he has called "proof by
contradiction" and also that he is fine with a fully classical proof is
this:

By "proof by contradiction," he means neither what people usually mean by
this nor EFQ. He means the specific use of reasoning from exhaustive cases,
some of which lead directly to the desired conclusion and some of which
lead there only indirectly (typically via EFQ) which in Core Logic would be
reasoning from exhaustive cases some of which lead directly to the desired
conclusion and some of which lead to contradiction (and are thereby
revealed to be cases that didn't deserve consideration in the first place).
So he is not worried about EFQ /per se/ but this specific sort of use of
it. The proof could have EFQ in it elsewhere.

Considering the case of the derivation of disjunctive syllogism in Core
Logic, I think Harvey's point would be -- aside from whether this rule is
demonstrably valid -- whether one would ever have to use it in a proof of
B. Why first establish AvB and then later establish B based on the
realization that A leads to a contradiction. When one can do this, is there
not always some sort of (fully classical) way of proceeding more directly
to B?

Also, the "proof" of disjunctive syllogism in Core Logic that NT displayed
is probably not what HF means by a "proof," because it is a derivation from
the assumptions AvB and ~A, whereas I gather that the question only makes
sense when speaking about proofs from no assumptions.

Curtis


On Fri, May 20, 2022 at 2:28 PM Tennant, Neil <tennant.9 at osu.edu> wrote:

> 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/de1473e9/attachment-0001.html>