1 The core conception

What in general is a formal proof? It is a straightforward matter to say what is a formal proof in a particular formal proof system: for example, a particular axiomatic (Frege/Hilbert style) proof system for classical first-order logic, or a particular tableaux system for a certain modal logic, or a particular natural deduction system for intuitionistic propositional logic, or a particular sequent calculus for a certain substructural logic, and so on. But what makes all these things formal logical proofs? Or, to look at things from a slightly different angle, what makes all these different systems count as systems of formal logical proof?Footnote ¹

Two features of formal proofs are immediately striking. First, a formal proof is always a proof of some claim. A proof is never just ‘a proof’, full stop. It is a proof that a certain formula is a tautology, or that a certain argument is valid, or that a certain set of formulas is unsatisfiable, and so on. So one obvious condition on a formal logical proof is that it is a proof of a logical claim as opposed to a claim of some other kind: for example, of geometry or physics. For purposes of this paper, we need not determine a precise boundary between logical and nonlogical claims, nor even assume that the boundary is precise.

Second, a formal proof is always a proof in a certain proof system. A given sequence of well-formed formulas (wffs) is a proof (that, say, the last wff in the sequence is a valid formula in classical first-order logic) in a certain axiomatic proof system—but not in a different system (that has different axioms or different rules of inference). So we are naturally led to the question: what is a formal proof system? According to what I shall call the core conception of formal proof—the name will be justified shortly—there are two essential features of a proof system. The first is a specification of (a) the symbols that are allowed to appear in proofs and (b) the format of proofs in the system—that is, which arrangements of the symbols are allowable. I shall (as in Smith [Reference Smith43]) use the term proof candidate for any array of the specified symbols in the specified format.Footnote ² The second essential feature of a proof system is a decision procedure that takes as input a proof candidate and a claim and returns Yes (this is a proof of that claim) or No (this is not a proof of that claim). It is this second feature—the decision procedure—that is the heart of the matter. Such a decision procedure requires well-defined inputs and the first feature of a proof system—the specification of symbols and format—is needed to provide one of these inputs: the proof candidate. The other input to the decision procedure is a logical claim. Each proof system is associated with certain kinds of claim (e.g., this argument of classical propositional logic is valid; or this set of formulas of classical first-order logic is satisfiable; or these two modal formulas are equivalent). These are the kinds of claim of which the proof system can provide proofs. The second input to the decision procedure is a claim of one of these kinds.

A couple of points of clarification about the decision procedure. First, in accordance with standard usage, by ‘decision procedure’ I mean an effective procedure that always (i.e., on all input pairs) terminates after a finite number of steps of computation with the answer Yes or the answer No—and by ‘effective procedure’ I mean a finite set of instructions, to be followed in a specified order, where each individual instruction is mechanical (no ingenuity or insight is required to carry it out), deterministic (it involves no random devices such as coin tosses) and finitely achievable (only a finite amount of time is required to complete it). Second, we are talking about a procedure for checking whether a given (as input) proof candidate is indeed a proof of a certain claim (also given as input). We are not talking about a procedure for finding or building proofs. Some familiar proof systems—for example, tableaux systems for classical propositional logic—come with mechanical procedures for building proofs, while others—for example, axiomatic proof systems—do not: to find an axiomatic proof of a tautology, one has to use ingenuity, insight or trial and error. But all familiar proof systems come (at least implicitly) with a procedure for checking the correctness of a candidate proof (however it was found in the first place)—and it is this kind of procedure that, according to the core conception, is central to the very idea of a formal proof system.

According to the core conception, then, a formal proof (of claim P, in proof system S) is a proof candidate (of S) that the decision procedure (for S) classifies as a proof (of P). In the remainder of this section I shall substantiate the claim that this is indeed the core conception of formal proof in the logical literature.

First, formulations of it can be found in textbooks including—besides Smith [Reference Smith43]—Bostock [Reference Bostock6], Hughes and Cresswell [Reference Hughes and Cresswell22] and Tennant [Reference Tennant44]:

Second, the core conception is bound up in the historical origins of the modern notion of formal logical proof: the essential features of formal proofs, according to the core conception, are indeed essential if formal proofs are to serve the purpose for which they were originally introduced. Although, like all major theoretical advances, it has precursors, the idea of formal proof under discussion in this paper essentially goes back to Frege’s Begriffsschrift:

Now consider what Frege wrote in the first paragraph of the Preface of Begriffsschrift:

and consider also his remarks in the Introduction to Grundgesetze:

Frege’s purpose in introducing a system of formal proof is epistemological or foundational. The aim is to be able to see on what exactly a mathematical theorem depends: from what axioms it follows by what rules of inference. (Furthermore, once we see that a theorem follows from clearly acceptable axioms via clearly acceptable rules, we thereby gain justification for believing the theorem.) To this end there must be no gaps in the proof and each step of the proof must be maximally small and simple.Footnote ⁴ Frege repeatedly talks of “the rigorous avoidance of gaps in the chains of inference” [Reference Frege11, p. 7]—or in an alternative translation “strict gaplessness of the chains of inferences” [Reference Frege12, p. x]—and “my gapless procedure” [Reference Frege11, p. 9].Footnote ⁵ The upshot of this is that checking a proof becomes a mechanical matter: one that does not require insight, ingenuity or intuition. If the latter were not the case—if insight, ingenuity or intuition were required to see that the proof is a proof—then the former goal would not in fact have been reached: the proof would not be sufficiently gapless. Anything beyond simple mechanical checking that you need to bring to a proof to see that it works—that it is indeed a genuine proof—has to be built into the formal proof itself, explicitly, so that checking it becomes a purely mechanical matter. So in sum: our current idea of formal proof—the idea under discussion in this paper—had its origins in an epistemologico-foundational project, and an essential upshot of a proof’s being fit for this purpose is that checking its correctness becomes a purely mechanical matter. Thus the central feature of the core conception—the requirement that there be an effective proof-checking procedure—is embedded right in the historical origin of the idea of formal proof.

Following Frege, the next great figure in the history of formal proof is Hilbert, whose concerns are summed up with admirable concision by Gandy:

Hilbert’s motivations are also epistemological or foundational—but they are not exactly the same as Frege’s. Frege assumes that his axioms and rules of inference are OK and wants to close all gaps in a piece of reasoning so that we can see conclusively that the conclusion follows from the given axioms by the given rules: nothing else creeps in. But Hilbert does not assume that given axioms are OK: he wants to prove that they are consistent, by proving in finitary mathematics—which he does assume to be OK—that there can be no proof from the axioms of a contradiction.Footnote ⁶ To this end, Hilbert requires that statements about proofs such as ‘P is a proof of C’ be part of finitary mathematics.Footnote ⁷ But all statements of finitary mathematics are decidable—hence claims of the form ‘P is a proof of C’ must be decidable.Footnote ⁸ So in sum: for formal proofs to serve their purpose—which (as with Frege) is epistemologico-foundational (although it is not exactly the same such purpose)—claims about formal proofs such as ‘P is a proof of C’ have to lie within the province of finitary mathematics, and hence must be decidable.Footnote ⁹ Thus the central feature of the core conception—the requirement that there be an effective proof-checking procedure—is embedded right at the core of Hilbert’s proof theory.Footnote ¹⁰

Third, the core conception of proof is central to many landmark results in modern formal logic concerning what can and cannot be proved. Consider, for example, Gödel’s incompleteness theorems. Gödel writes:

It is crucial to Gödel’s entire line of thought that the relation that holds between a formal proof P and a theorem C when P is a proof of C has the kind of concrete simplicity that Hilbert took it to haveFootnote ¹¹ —or as Gödel puts it more precisely, that the relation is primitive recursive. But then this relation must be decidable. So again, the central feature of the core conception—the requirement that there be a decision procedure for the question whether X is a proof of Y—is embedded right at the heart of Gödel’s incompleteness theorems. To jump from an early example to a recent one, Kripke’s [Reference Kripke, Copeland, Posy and Shagrir28] derivation of the Church–Turing thesis from Gödel’s completeness theorem for first-order logic with identityFootnote ¹² turns essentially on the assumption that claims of the form ‘P is a proof of C’ must be decidable.Footnote ¹³

So the core conception deserves its name: it is found in the textbooks, rooted in the history and embedded in the results of formal logic as we know it.Footnote ¹⁴

2 The strengthened conception

Nevertheless, a strengthened conception of formal proof has emerged in the last 50 or so years—in particular in the literature on propositional proof complexity. The strengthened conception imposes an additional requirement on a formal proof system: not only must there be (as on the core conception) an effective or mechanical proof-checking procedure, but furthermore this procedure must be feasible in the sense of being able to be carried out in polynomial time. That is, the running time of the procedure must be bounded above by a polynomial function of the length of its input. Recall that on the core conception, the input to the proof-checking procedure is a proof candidate plus a claim, and the procedure returns Yes (this is a proof of that claim) or No (this is not a proof of that claim) after a finite number of steps of computation. The strengthened conception imposes an upper bound on this finite number—or more precisely on the rate at which this number grows as the length of the input to the procedure increases.Footnote ¹⁵

Here are some statements of the strengthened conception of formal proof:Footnote ¹⁶

I have explained in §1 why there must be a mechanical proof-checking procedure if formal proofs are to do the work for which they were introduced in the first place and if central results about what can and cannot be proved are to remain valid. So there are good reasons behind the core conception of proof. What about the proposed strengthening? Why should we think that the proof-checking procedure must be computable in polynomial time? In the remainder of this paper I shall discuss four arguments for the strengthened conception: one in each of §§3–6. Some of the arguments are drawn from the literature and some are of my own construction. They are all the reasonable arguments in favour of the strengthened conception that I can find or devise. I shall reject them all. My conclusion will be that we have no good reason to move beyond the core conception of formal proof to the strengthened conception.

3 The argument from convenience

Consider an example of a central theorem from the literature on propositional proof complexity—one proven in the paper in which the polynomial-time constraint on proof-checking entered the literature [Reference Cook and Reckhow9]:

This claim would not be true if it were not built into the meaning of ‘proof system’ that the proof-checking procedure runs in polynomial time. That is, the existence of a proof system that yields short proofs of all tautologies is only equivalent to the identity of $\mathsf {NP}$ and $\mathsf {coNP}$ provided that all proofs in the system can be checked in polynomial time. (Why this is so—specifically, why the ‘only if’ direction depends on polynomial checkability—is explained in the Appendix.)

This is not an isolated example: many results in the propositional proof complexity literature are stated in a way that requires for their truth that proofs are always checkable in polynomial time. And this is no surprise, because the standard definition of ‘formal proof system’ in this literature builds in the requirement of polynomial time checkability (not just effective checkability, as on the core conception). But our concern now is why we should adopt this definition. I can imagine two lines of thought stemming from the observation I have just made about the formulations of results in this literature—but as I shall now explain, neither of them yields a good argument for the conclusion that polynomial-time (as opposed to merely effective) checkability is or should be part of the very idea of what makes something a formal proof system.

First, someone might think that authors in the literature on propositional proof complexity are not in the business of contributing to the project of analysis of the very idea of formal proof. They are simply setting up formal definitions in a way that is convenient and that allows them to prove interesting results. Note that the main preexisting proof systems studied in this literature—Frege–Hilbert style axiomatic proof systems, natural deduction systems, sequent calculi and so on—all in fact meet the requirement that proofs in these systems can be checked in polynomial time. The formal definition of ‘proof system’ simply abstracts away certain features of these existing proof systems—and there’s nothing more to it than that.

If this is true, then for purposes of this paper there is nothing to see here and we can move on. Our interest here is (analysis of) the very idea of formal logical proof. If the definition of ‘formal proof system’ in the propositional proof complexity literature is not actually intended as a proposal to strengthen the core conception of formal proof but is merely a convenient definition for ‘internal use only’ within this literature, then it poses no challenge to the core conception and we can simply pass on. However it is worth noting that this is not the way the literature actually reads.Footnote ²¹ See, for example, the quotes in §2 and note the following formulations (my emphases): “one basic property which all formalizations of the concept of a proof must satisfy”; “The crucial property of a proof system”; “three properties that seem necessary for any method of certifying tautologies.”

Second, someone might think that we should adopt the strengthened definition of proof because it is more convenient: it allows for simpler statements of results. One can, for example, present the result above in the way I did, rather than as follows:

But this is pretty obviously a terrible argument for altering the very definition of ‘formal proof system’. All it warrants is (sticking with the core conception and) adding a rider: “For simplicity, it will henceforth be assumed that all proof systems under discussion have polynomial-time proof-checking procedures.” Furthermore, that way of proceeding would be in keeping with the treatment of other notions in the literature on computational complexity. One standardly talks, for example, of feasibly (i.e., polynomial-time) computable functions, using ‘feasible’ as an explicit qualifier rather than building it into the very definition of ‘computable’. There is something oddly asymmetric and out of keeping with general usage in treating ‘short’ (i.e., polynomial length bounded) as an explicit qualifier on ‘proofs’ but building ‘feasible’ (i.e., polynomial-time bounded) into the word ‘proof’ itself, rather than adding it explicitly—whether on individual occasions, or as an initial overall rider.Footnote ²²

Before moving on, it is worth discussing a line of thought that connects Gödel’s famous letter to von Neumann and the $\mathsf {P}\stackrel {?}{=}\mathsf {NP}$ problem and turns on polynomial-time proof-checking. Gödel writes:

Aaronson [Reference Aaronson1, p. 7] writes:

I take it that Gödel’s line of thought is as follows. To see whether F has a proof of length n, go through all the strings of symbols of length n and for each one, check whether it is a proof of F. This part of the reasoning depends on the fact that proof-checking is a mechanical matter: it is decidable whether or not a certain string is a proof of F. Now suppose the Turing machine that does this checking of strings runs in linear (in n) time (or even quadratic time)—and suppose we want to know whether F. To warrant the answer Yes, we need a proof of F. We ask the machine if there is a proof of length up to some very large n—so large that proofs longer than this are beyond our grasp (i.e., even if there is such a proof, it will never warrant us in believing F, because we cannot even read through the whole proof). If the machine says Yes then we know F is true. If it says No, then the question whether F is in effect closed: perhaps there does exist some astronomically long proof, or perhaps there is no proof of F at all, but either way, as far as we are concerned, we are not and cannot ever be warranted in believing or asserting F, and so the question whether F is effectively terminated.

I take it that Aaronson’s line of thought is as follows. Suppose that the ‘proves’ relation (between proof candidates and formulas) is not merely decidable but polynomially so. Consider the set G of pairs $(\alpha ,x)$ of a formula $\alpha $ and a number x (encoded in unary) such that $\alpha $ has a proof of length x or less. This set is in $\mathsf {NP}$ : the membership certificate (see the Appendix) for a pair $(\alpha ,x)$ is just the proof of $\alpha $ of length at most x—and we have just supposed that this can be checked (by a deterministic Turing machine) in polynomial time. Now suppose also that $\mathsf {P}=\mathsf {NP}$ . Then we cannot merely confirm in polynomial time (given the proof as a certificate) that $(\alpha ,x)\in G$ : we can, given only $(\alpha ,x)$ , decide in polynomial time whether $(\alpha ,x)\in G$ . So if $\mathsf {P}=\mathsf {NP}$ then one can feasibly (i.e., polynomially) determine for any formula $\alpha $ whether or not it has a proof of length up to some n so large that proofs longer than this are beyond our grasp.

Note that Aaronson’s line of thought does not require that it be part of the very idea of a proof system that proofs can be checked in polynomial time. All we need to reach the conclusion that we can feasibly determine for any formula $\alpha $ whether or not it has a proof (in system S) of length up to some big n is the supposition that $\mathsf {P}=\mathsf {NP}$ together with the fact that we have some proof system S in which proofs can be checked in polynomial time. It would not undermine the argument at all if we did not build polynomial-checkability into the very idea of a proof system—that is, if we allowed the possibility of other (legitimately so-called) proof systems in which proof-checking is mechanical but not polynomial.

4 The argument from intuition

A second possible argument in favour of the strengthened definition of proof is that it is simply intuitively obvious (at least once attention was drawn to the matter by Cook and Reckhow) that a proof must be easy to check (in the sense of ‘easy’ discussed in n. 19). Many of the writers quoted in §2 seem to present the new definition this way: they give no argument for it but write as if it is simply obvious:

In response to this (argument from) intuition, I present the following exhibits. First, Hughes and Cresswell [Reference Hughes and Cresswell22, pp. 24–25] introduce an axiomatic proof system K:

They then write “We shall first prove two theorems in full detail” [p. 26] and then present the following proof [p. 27]:

$$\begin{align*}\begin{array}{lll} \text{PC}1 & (1) & (p\wedge q)\supset p \\ (1) \times \text{N} & (2) & L((p\wedge q)\supset p) \\ \textbf{K} & (3) & L(p\supset q)\supset (Lp\supset Lq) \\ (3)[p\wedge q/p, p/q] & (4) & L((p\wedge q)\supset p)\supset (L(p\wedge q)\supset Lp) \\ (2), (4) \times \text{MP} & (5) & L(p\wedge q)\supset Lp \\ \text{PC}2 & (6) & (p\wedge q)\supset q \\ (6) \times \text{N} & (7) & L((p\wedge q)\supset q) \\ (3)[p\wedge q/p] & (8) & L((p\wedge q)\supset q)\supset (L(p\wedge q)\supset Lq) \\ (7), (8) \times \text{MP} & (9) & L(p\wedge q)\supset Lq \\ \text{PC}3 & (10) & (p\supset q)\supset((p\supset r)\supset(p\supset(q\wedge r))) \\ (10)[L(p\wedge q)/p, Lp/q, Lq/r] \\ & (11) & (L(p\wedge q)\supset Lp)\supset((L(p\wedge q)\supset Lq)\supset \\ & & (L(p\wedge q)\supset(Lp\wedge Lq))) \\ (5), (11) \times \text{MP} & (12) & (L(p\wedge q)\supset Lq)\supset (L(p\wedge q) \\ & & \supset(Lp\wedge Lq)) \\ (9), (12) \times \text{MP} & (13) & (L(p\wedge q)\supset(Lp\wedge Lq)) \hfill \textbf{Q.E.D.} \\ \end{array} \end{align*}$$

Note the lines in this proof annotated ‘PC1’, ‘PC2’ and ‘PC3’. To check the proof, you need to check that each of the wffs on these lines really is a tautology of propositional logic. We have no polynomial-time procedure for that—and if $\mathsf {P}\neq \mathsf {NP}$ then there is no such procedure.Footnote ²⁶ So according to the strengthened conception of proof, this is not a formal proof. Yet, I submit, it clearly is a perfectly good formal proof: Hughes and Cresswell thought it was one, and generations of their readers have accepted this without demur.

Note that Hughes and Cresswell describe this as a proof in full detail. They do not regard it as a placeholder for a full formal proof, that could be spelled out into a formal proof if one wanted to by inserting extra lines before each wff labelled ‘PC’: extra lines mirroring a proof of that wff in a standard axiomatic proof system for propositional logic. They regard this as a formal proof in itself, as it stands.Footnote ²⁷ Furthermore, they say quite explicitly:

The requirement on a satisfactory set of axioms that they are talking about here is the one already quoted in §1: “An axiomatic basis must be formulated in such a way that we can determine effectively $\ldots $ of any wff whether or not it is an axiom” [p. 23]. So Hughes and Cresswell are quite explicit that the truth table method is a perfectly good effective procedure for checking a proof (or more precisely, a perfectly good sub-procedure, that is, part of the overall proof-checking procedure: the part that checks whether a given line of a proof in system K is an instance of the axiom schema $\mathbf {PC}$ ). Yet it is well known that the truth table procedure runs in exponential time. So Hughes and Cresswell are extremely close here to denying explicitly that the proof-checking procedure must run in polynomial time.

In this connection, note Kleene [Reference Kleene23]. On p. 224 he says—in accordance with the core conception—that the question “Is a given finite sequence of formulas a proof?” is decidable:

In n. 163 on the next page, he then notes that even when we have a decision procedure for answering a certain question:

He immediately continues:

Kleene is effectively saying here that the core conception is all we need: claims of the form ‘P is a proof of C’ must be decidable, but it does not matter whether or not the decision procedure is feasible.

Burgess [Reference Burgess7] does the same sort of thing as Hughes and Cresswell: when defining the system $\mathbf {L}_0$ of minimal temporal logic, one of his axiom schemas is “A, where A is any tautology” [p. 21]. Furthermore, he also introduces a rule of inference—the rule of tautological consequence (Taut)—defined as follows: “from $A_1,\ldots ,A_n$ to infer any tautological consequence B” [p. 22].Footnote ²⁸ He goes on to present the following proof [p. 28]:

$$\begin{align*}\begin{array}{llr} \text{i} & \mathsf{GP}A\to\mathsf{GGP}A & \text{Ax} \\ \text{ii} & A\to\mathsf{GP}A & \text{Ax} \\ \text{iii} & A\to\mathsf{GGP}A & \text{i, ii, Taut} \\ \text{iv} & \mathsf{PP}A\to\mathsf{PPGGP}A & \text{iii, Becker} \\ \text{v} & \mathsf{PGGP}A\to\mathsf{GP}A & \text{Ax} \\ \text{vi} & \mathsf{PPGGP}A\to\mathsf{PGP}A & \text{v, Becker} \\ \text{vii} & \mathsf{PGP}A\to\mathsf{P}A & \text{Ax} \\ \text{viii} & \mathsf{PP}A\to\mathsf{P}A & \text{iv, vi, vii, Taut} \\ \end{array} \end{align*}$$

Similar remarks apply to this proof as to the proof of Hughes and Cresswell discussed earlier. To check line iii (and mutatis mutandis for line viii), you need to check that it really follows logically from i and ii. We have no polynomial-time procedure for that—and if $\mathsf {P}\neq \mathsf {NP}$ then there is no such procedure.Footnote ²⁹ So according to the strengthened conception of proof, this is not a formal proof.

There are two ways to take the material in this section: as an appeal to your intuitions—look at the proofs from Hughes and Cresswell and from Burgess and agree that they are satisfactory formal proofs—or as an appeal to the authority of the authors discussed (Hughes and Cresswell, Kleene and Burgess). Either way, one clearly cannot maintain that it is just intuitively obvious that proofs have to be checkable in polynomial time.

Before moving on, I can imagine someone objecting: the strengthened definition of proof comes from the literature on propositional proof complexity—but Hughes and Cresswell and Burgess are talking about modal and tense logics, not propositional logic. The latter observation is true—but it is hard to see how it is supposed to help the argument from intuition for the strengthened conception. Is the point supposed to be that the strengthened conception applies to all formal logical proofs—but the intuitions that support it concern only propositional proofs? Setting aside (for now)Footnote ³⁰ the issue of whether we really have any such intuitions (i.e., about propositional proofs specifically), how could they possibly justify an analysis of proof that rules out as formal proofs things that seem to be perfectly good formal proofs, such as the proofs of Hughes and Cresswell and Burgess? That broad thesis would clearly require broader support. Or is the idea supposed to be that the strengthened analysis applies only to proofs in propositional logic? But then the proponents of the strengthened (but now narrower in scope) analysis have actually given themselves more work to do: now they must explain what is special about propositional proofs that makes them subject to more stringent conditions than other logical proofs. The (alleged) existence of intuitions concerning the easy checkability of propositional proofs plus the non-existence of intuitions concerning the easy checkability of non-propositional proofs (vide Hughes and Cresswell and Burgess) does not add up to a compelling reason for a two-sorted analysis of formal proof that adheres to the core conception for non-propositional proofs and the strengthened conception for propositional proofs: such a disjunctive analysis would require more compelling support. But here the prospects seem dim: when we move from formal logical proofs in propositional logic to formal logical proofs in predicate logic or modal logic or any other kind of logic, there seem only to be changes in the details of the languages and proof systems under consideration—not a change in the fundamental nature of the objects (formal proofs) under consideration which requires a different analysis of formal proof once we move outside the realm of classical propositional logic.

5 The argument from no-self-proof

In introducing (what I am calling) the strengthened conception of formal proof, Beame and Pitassi [Reference Beame, Pitassi, Păun, Rozenberg and Salomaa4, p. 43] write:

The final sentence could be read as an expression of an intuition that a proof must be easy to check. That approach was covered in the previous section. But taken as a whole, the passage could be read as offering an argument for the strengthened conception that goes beyond the argument from intuition:

1. 1. If we do not impose the additional requirement of feasibility of proof-checking on formal proofs then we get the result that a formula of propositional logic counts as a proof of itself (of its own tautologousness, or satisfiability, or unsatisfiability, as the case may be).

2. 2. This is the wrong result: intuitively, a formula cannot prove itself or act as its own proof.

3. 3. Therefore we should impose the feasibility requirement.

The argument from intuition argues for the feasibility requirement by appealing directly to its intuitive obviousness. This new argument appeals only to a more focussed intuition: that formulas cannot prove themselves.Footnote ³¹

My response to this argument will be to show that even if we impose the feasibility requirement, we still get a pervasive class of self-proving wffs—so avoiding self-proving formulas is not an adequate motivation of the feasibility requirement.Footnote ³²

In order to show this, we start with some definitions. Write the basic propositions of the language (of propositional logic) as: $p_1, p_2, p_3, \ldots $ .Footnote ³³ A literal is a basic proposition or a negation of a basic proposition. A conjunction of distinguished literals (cdl) is a conjunction of one or more literals in which no basic proposition occurs more than once—for example:

$$ \begin{align*}p_1\quad \neg p_3\quad (p_1\wedge\neg p_2)\quad (\neg p_2\wedge\neg p_4)\quad (p_7\wedge p_8\wedge\neg p_6).\end{align*} $$

The signature of a cdl is a sequence of positive integers comprising the subscripts on the basic propositions in the order in which they occur in the cdl. So the signatures of the example cdls above are, respectively:

$$ \begin{align*}(1)\quad (3)\quad (1,2)\quad (2,4)\quad (7,8,6).\end{align*} $$

Two cdls are cosigned if they have the same signature. A set of cdls is cosigned if its members are pairwise cosigned; in this case we also say that the cdls in the set are cosigned. A cosigned disjunctive normal form (cdnf) is a disjunction of zero or more distinct cosigned cdls—for example:

$$ \begin{align*}(p_2\wedge p_7\wedge\neg p_5)\vee (p_2\wedge p_7\wedge p_5)\vee (p_2\wedge\neg p_7\wedge\neg p_5).\end{align*} $$

We stipulate that $\bot $ is the unique disjunction of zero cdls and is false on every model.

Figure 1

Truth table and cdnf.

Figure 1 Long description

The table consists of five columns and nine rows.

Header Row:

* Column 1: p sub 3

* Column 2: p sub 1

* Column 3: p sub 4

* Column 4: (p sub 3 arrow p sub 1) double arrow (p sub 1 arrow p sub 4)

* Column 5: (p sub 3 and p sub 1 and p sub 4) or (not p sub 3 and p sub 1 and p sub 4) or (not p sub 3 and not p sub 1 and p sub 4) or (not p sub 3 and not p sub 1 and not p sub 4)

Data Rows (p sub 3, p sub 1, p sub 4 | Column 4 result | Column 5 result):

* Row 1: 1, 1, 1 | 1 | 1

* Row 2: 1, 1, 0 | 0 | 0

* Row 3: 1, 0, 1 | 0 | 0

* Row 4: 1, 0, 0 | 0 | 0

* Row 5: 0, 1, 1 | 1 | 1

* Row 6: 0, 1, 0 | 0 | 0

* Row 7: 0, 0, 1 | 1 | 1

* Row 8: 0, 0, 0 | 1 | 1

The results in Column 4 and Column 5 are identical for every row, demonstrating logical equivalence.

To get a feeling for what cdnfs are—and to see that every wff of propositional logic is equivalent to a cdnf—take any formula, say, for example, $(p_3\to p_1)\leftrightarrow (p_1\to p_4)$ , and consider its truth table: the middle column in Figure 1. For each row in which the formula is true, write down a ‘description’ of that row in the form of a cdl. For example, the wff is true in row 1, in which $p_3$ is true and $p_1$ is true and $p_4$ is true, so the description of this row is $(p_3\wedge p_1\wedge p_4)$ ; and in row 5, in which $p_3$ is false and $p_1$ is true and $p_4$ is true, so the description of this row is $(\neg p_3\wedge p_1\wedge p_4)$ ; and so on. Note that (a) each description is true in and only in the row it describes and (b) these descriptions will always be cosigned cdls. Now write down the disjunction of all these cdls: because of (a) (and the truth conditions of $\vee $ ) it will be equivalent to the original formula and because of (b) it will be a cosigned cdnf. In the case where the original formula was false in all rows, the resulting cdnf will be $\bot $ .

A cdnf is its own proof. More precisely, a cdnf $\alpha $ is (simultaneously) a proof candidate of the claims:

• • $\alpha $ is unsatisfiable;

• • $\alpha $ is satisfiable;

• • $\alpha $ is a tautology;

and is a proof of the claim(s) for which it passes the following proof-checking test—which runs in polynomial time:

1. 1. Is $\alpha $ the wff $\bot $ ?

   Yes: $\alpha $ is (a correct proof that $\alpha $ is) unsatisfiable.

   No: $\alpha $ is (a correct proof that $\alpha $ is) satisfiable; go to 2.

2. 2. Count the number n of basic propositions in $\alpha $ ’s first disjunct and the number m of disjuncts in $\alpha $ . Can you halve m (recursively) n times?

   Yes: $\alpha $ is (a correct proof that $\alpha $ is) a tautology.

   No: $\alpha $ is (a correct proof that $\alpha $ is) not a tautology.

There are a couple of things to explain here. First, there is nothing odd about a certain object—in this case a formula—being a proof candidate of multiple claims. This situation is very familiar. For example, a truth table for a formula $\alpha $ is simultaneously a proof candidate for the three claims bullet-pointed above and a tableau (tree) beginning with the formula $\neg \alpha $ is simultaneously a proof candidate for the claims:

• • $\neg \alpha $ is unsatisfiable;

• • $\neg \alpha $ is satisfiable;

• • $\alpha $ is a tautology.

The truth table is a proof of the claim(s) for which it passes the associated test (respectively: check whether $\alpha $ is false on all rows; check whether $\alpha $ is true on some rows; check whether $\alpha $ is true on all rows) and similarly for the tableau (where the tests are respectively: check whether all paths close; check whether some path remains open; check whether all paths close).Footnote ³⁴

Second, to explain the test itself. The point behind step 1 is that $\bot $ is unsatisfiable and every other cdnf is satisfiable. To see the latter, note that a disjunction of one or more disjuncts is true if at least one of those disjuncts is true. In this case the disjuncts are cdls: conjunctions of distinguished literals—that is, no basic proposition occurs more than once. So every cdl is satisfiable, and indeed shows on its face how to assign truth values to basic propositions in such a way as to make it true: a basic proposition that occurs unnegated should be assigned True (1) and a basic proposition that occurs negated should be assigned False (0). Therefore every cdnf with one or more disjuncts—that is, every cdnf other than $\bot $ —is satisfiable. The idea behind step 2 is as follows. There are n basic propositions in the cdnf so there are $2^n$ ways of assigning truth values to those basic propositions. The wff as a whole is a tautology if it is true on all those valuations. Each disjunct describes exactly one such valuation—and different disjuncts describe different valuations, because a cdnf is a disjunction of distinct cdls and no two distinct cdls with the same signature describe the same valuation. Thus if there are $2^n$ disjuncts then every valuation is covered: the cdnf is true on all of them and hence a tautology. If there aren’t that many then it isn’t a tautology. So we want to know whether $m=2^n$ . We do not simply calculate $2^n$ and then check whether it equals m because we want to ensure that the procedure runs in polynomial time. Instead we start with m, noting that $m=2^n$ iff you can halve m (recursively) n times (i.e., halve m, then halve the result, and so on), where the halving procedure fails if you attempt to perform it on an odd number.

The foregoing considerations can readily be extended from single formulas to sets of formulas and arguments. Say that the signature of a cdnf is the signature of any (and all) of its disjuncts (and that the signature of $\bot $ is the empty sequence of integers). A set of cdnfs is cosigned if its members all have the same signature. A cosigned set of cdnfs is a proof of its own un/satisfiability: we just need to check whether there is a disjunct that appears in every formula in the set. If so, the set is satisfiable; if not, the set is unsatisfiable. Say that an argument is cosigned if its premisses and conclusion are cdnfs that all have the same signature. A cosigned argument is a proof of its own in/validity: we just need to check whether there is a disjunct that appears in every premise and does not appear in the conclusion. If so, the argument is invalid; if not, the argument is valid.

So, even if we demand that proof-checking procedures must run in polynomial time, we still have self-proving formulas (and sets of formulas and arguments): so many of them, indeed, that every wff of the language of propositional logic is equivalent to one (or more). We can even consider a language in which only cdnfs count as wffs. It has the same expressive power as the standard language of propositional logic, because every wff of the standard language has an equivalent cdnf. In this language, every formula serves as its own proof—so we do not need separate proof objects at all. The formulas themselves are all we need: the language is simultaneously a language of formulas and a language of proofs.Footnote ³⁵ Thus, requiring that proofs be easy to check does not ban wffs’ being their own proofs—nor even a language in which every wff is its own proof. So an intuition against endemic self-proof is not an adequate motivation of the strengthened conception of proof over the core conception.Footnote ³⁶

6 The argument from epistemology

I turn now to a final argument for the strengthened conception (one of my own devising—not drawn from the literature) which runs as follows. Proof is an epistemological notion. A proof of a theorem is what enables you to know the theorem. But you do not know the theorem just in virtue of holding the proof in your hands: you have to work through it, step by step. But this process of going through the proof and seeing that each step follows from the previous steps until ultimately the theorem is reached, is exactly the same as the procedure of checking the proof for correctness. So if theorems are to be knowable, this checking procedure must be feasible—that is, it must be polynomial-time computable.

I think there is a correct argument in there—and also an incorrect one. To distinguish them clearly I’ll need to use words carefully. So far I’ve been following standard practice in the computational complexity literature (see n. 18 and n. 19) and using ‘feasible’ (and ‘easy’) as a shorthand for ‘computable in polynomial time’. I’m going to stop doing that now because—at least in the present context—it would foster confusion between two very different notions. One is the notion of an efficient procedure. This is what complexity theorists mean by ‘feasible’.Footnote ³⁷ The other is the notion of an achievable task. This is what ordinary folk often mean by ‘feasible’.

The key underlying distinction here is between procedures and tasks. By a ‘task’ I mean a singular (one-off) item of work.Footnote ³⁸ By a ‘procedure’ I mean a general process or set of instructions that can be followed in order to perform a task.Footnote ³⁹ For example, adding up 67 and 58 (on some occasion) is one task and adding up 324 and 42 (on some occasion) is a different task—but you can follow the same procedure to carry out both tasks.Footnote ⁴⁰ Note that even though you follow the same procedure, the number of steps involved in carrying out that procedure will be greater on the second occasion than on the first.

An efficient procedure is one whose running time (in the sense of n. 15) has a rate of growth that is bounded above by a polynomial function. An achievable task is one that does not involve too many steps Footnote ⁴¹ (or steps that are too difficult—but when we are talking about effective procedures, as we are in the case of proof-checking procedures, every step is simple and mechanical and hence there is no question of any step’s being too difficult to perform). Note that these are different notions. A task can be achievable even though we have no efficient procedure for carrying it out; and a task can fail to be achievable even though we do have an efficient procedure for carrying it out. As an example of the former, consider the task of writing out a truth table for a formula with five basic propositions. We have an effective procedure for doing this, but no efficient procedure. Nevertheless the task is perfectly achievable: it is the kind of thing one might set students as a homework exercise. As an example of the latter, consider the task of checking a 30000-odd page truth table (i.e., roughly as many pages as Encyclopaedia Britannica) for a wff involving twenty propositional letters. We do have an efficient procedure for doing that,Footnote ⁴² yet the task of checking the table is not achievable. No normal person has the time available to do it: it would simply take too long.Footnote ⁴³

Now returning to the argument at the beginning of this section, supposing (what is extremely plausible—and can at the very least be granted for purposes of argument) that to get to know a theorem one must work through a proof of it, we may indeed conclude that if you are to know the theorem, the task of checking its proof must be achievable. But this is not the conclusion that the proponents of the strengthened conception need. They want to conclude that the procedure for checking the proof must be efficient. And that simply does not follow. As we have just seen, a task’s being achievable is a different thing from the existence of an efficient procedure for performing the task: a task can be perfectly achievable even though we have no efficient procedure for performing it. So the argument from epistemology fails.