Proof by Contradiction / EFQ

[Curtis Franks]

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