Frege on Indirect Proof

Abstract

Frege's account of indirect proof has been thought to be problematic. This thought seems to rest on the supposition that some notion of logical consequence – which Frege did not have – is indispensable for a satisfactory account of indirect proof. It is not so. Frege's account is no less workable than the account predominant today. Indeed, Frege's account may be best understood as a restatement of the latter, although from a higher order point of view. I argue that this ascent is motivated by Frege's conception of logic.

Acknowledgements

I am grateful to Haim Gaifman, Achille Varzi, and two anonymous referees for helpful criticisms and suggestions. I thank Melissa Weissberg for help in editing the paper.

Notes

¹The locus classicus of the view that Frege rejected independence arguments – indeed ‘metatheory’ more generally – is Ricketts (1997); also see Goldfarb (1979).

²See Tappenden (2000, §4), for a good survey of Frege's statements to this effect.

³It is worth noting that what I am imputing to Frege involves no appeal to possible worlds. That is, I am not saying that Frege evades counterfactual assumptions by regarding them from the point of view of a possible world in which they are true. Indeed, by Frege's lights, we may take contradictions as counterfactual assumptions, but they are true in no possible world.

⁴It should be noted that if the treatment of indirect proof just outlined is actually Frege's, his doctrine that axioms must be true does not preclude his trying to prove an axiom. For Frege, the possibility that one axiom can be proved from some others is just the possibility that the first is not, after all, an axiom – or rather an axiom alongside the axioms from which it has been proved. In short, when Frege says things like ‘it is part of the concept of an axiom that it can be recognized as true independently of other truths’ (Frege 1979b, p. 168), he should be understood as giving a criterion for something being an axiom.

⁵Frege recognized no difference between the supposition A in an indirect proof and A as it appears, after the indirect proof, in the triviality A→B. Let A be the supposition that √2 is rational. Frege would derive lnot A as described above, while the tautology lnot A→(A→B) would be proved from his axioms, with A→B following by detachment. Granting Frege his axioms and that they are logical (and setting aside their inconsistency), these derivations show that lnot A, lnot A→(A→B), and A→B are all logically true. This is exactly as it would be if we replaced A throughout with a sentence of the form D∧¬D. I am grateful to an anonymous reviewer for bringing to my attention this point of possible misunderstanding. The point, and the conception of logic that lies behind it, is elaborated below.

⁶The deduction theorem is sometimes called the ‘Tarski–Herbrand deduction theorem’. Herbrand first proved it for a particular system, in his dissertation published in 1930; in the same year, Tarski raised it to a ‘general methodological principle for logistic systems’ (Church 1956, p. 164). According to the syntactic version proved by Herbrand, corresponding to every formal proof from premises is a formal proof without premises.

⁷Cf. Heck (2000).

⁸Goldbach communicated this conjecture in a letter to Euler dated 7 June 1742. According to the conjecture, every even integer greater than two is the sum of two primes. As of 23 December 2009, the conjecture has been verified for integers up to 16×10¹⁷.