N. Goodman and W. V. Quine, "Steps Toward a Constructive Nominalism", Journal of Symbolic Logic, 12 (1947).

10. Proofs and Theorems

An inscription is a theorem if it has a proof; and a proof is constructed by a series of steps of immediate consequence, starting from axioms. Roughly, a proof is describable as composed of one or more lines such that each is either an axiom or an immediate consequence of preceding lines. Actually we need not require that the so called 'lines' of a proof be at different levels on a page, or be segregated from one another by any other device. They could even be written end to end without intervening punctuation, and we could still single them out uniquely as separate 'lines'. For, the grammar of the object language is such that the result of directly concatenating two formulas z and w will never be a segment of a larger formula, nor will it contain as segments any formulas other than those that are segments of z alone or w alone. Accordingly it will be convenient in general to speak of x as a line of y (where y may or may not be a proof) if x is a formula that is part of y but not part of any other formula in y.

D28.
Line xy = (z)(Fmla z & Part xz & Part zy .<-->. z = x).

If a theorem is to be defined as a formula for which a proof exists, it is important not to demand that all lines of the proof be assembled in proper order in any one place and time. Accordingly we shall so define a proof as to allow it to consist of lines wherever they may be -- perhaps scattered at random throughout the universe, and perhaps not even all existing at any one moment or within any one century.

According to the rough characterization of proof proposed two paragraphs back, each line must be either an axiom or an immediate consequence of preceding lines. The reason for the word "preceding" here is to rule out cases where every line is deducible from other lines, in circular fashion, while not all lines are deducible ultimately from axioms. However, we must now resort to some other expedient for excluding such circularity; for we have chosen to dispense with the ordering of lines of a proof, and this deprives us of the notion of a 'preceding' line.

An expedient which will be shown to meet the requirements is this: We stipulate that if any individual y contains as parts some lines of a proof x but none that are axioms, then some line of x that lies in y must be an immediate consequence of lines of x that lie outside y. The following, then, is our definition:

D29.
Proof x = (y){(]z)(Line zx & Part zy) & (w)(Axiom w & Line wx .--> ~Part wy) .--> (]s)(]t)(]u)(Line sx & Part sy & Line tz & ~Part ty & Line ux & ~Part uy & ICstu)}.

In order to establish that this definition is adequate to our purposes, we shall now show (1) that if x is a 'proof' in the sense of D29, then we can specify an order of 'precedence' among the lines of x such that every line is either an axiom or an immediate consequence of 'earlier' lines; and we shall show conversely that (2) if x is such that an order of precedence of the above kind can be specified among its lines, then x is a 'proof' in the sense of D29.

(1) is established as follows. Suppose x is a 'proof' in the sense of D29. We can begin our specification of an order of precedence among the lines of x by picking out, in an arbitrary order L1, L2 . . . , Lk, all those lines of x that are axioms. Next, from among the remaining lines of x, we pick one, call it Lk+1, which is an immediate consequence of lines from among L1, L2, . . . , Lk. (There will be such a line; for, by D29, that individual y which consists of all lines x except L1, L2, . . . , Lk must contain a line that is an immediate consequence of lines of x outside y.) Next, from among the remaining lines of x, we pick one -- call it Lk+2 -- which is an immediate consequence of lines from among L1, L2 . . . , Lk+1. (There will be such a one, for the same reason as before.) Continuing this, we eventually specify an order of precedence of the required kind.

(2) is established as follows. Suppose the lines of x can be counted off in some order such that each line is an axiom or an immediate consequence of earlier lines. Now consider anything y that contains some lines of x but none that are axioms. From among those lines of x that are parts of y, pick out the one that is earliest according to the assumed order. It must be either an axiom or an immediate consequence of earlier lines of x. But it is not an axiom, for y contains none of the lines of x that are axioms. Hence it is an immediate consequence of earlier lines of x; and those earlier lines are not in y. We see therefore that y contains a line of x that is an immediate consequence of lines of x outside y. Since y was taken as any individual containing some lines of x but none that are axioms, it follows that x is a proof in the sense of D29.

So it is now clear that D29, without stipulating any order among lines, gives us an adequate version of 'proof'.

Note incidentally that D29 abstains even from any requirement that a proof consist wholly of formulas; the 'lines' of a proof x are indeed formulas, but x may contain also any manner of additional debris without ill effect. Proofs are not in general 'inscriptions', in the sense of D5.

If a theorem is any inscription for which there is a proof, then an inscription is a theorem if and only if it is a line of some proof. But this formulation is a little too narrow. Given any inscription y for which a proof x exists, it will be true that for each inscription z that is like y, and that lies outside of x, a proof will also exist, consisting for example of z together with those lines of x that are not identical with y. Hence if y is a theorem all such inscriptions like it will also be theorems. But suppose that some inscription w that is like y lies embedded within some line t in the proof x, and suppose that no other line like t exists; in this case there may be no proof for w, so that some inscriptions like the theorem y may not be theorems. To prevent this anomaly, we construct our definition so that an inscription will be a theorem if and only if it is like some line of some proof. ("Like" has of course been so defined as to be reflexive.)

D30.
Thm x = (]y)(]z)(Proof y & Line zy & Like xz) .

With the definition so constructed, it follows that all immediate consequences of theorems are theorems. But some formulas may still fail to qualify as theorems solely because no inscription exists anywhere at any time to stand as a needed intermediate line in an otherwise valid proof. Such limitations would prove awkward if we had to depend upon the accidental existence of inscriptions that are perceptibly marked out against a contrasting background. But we may rather, as suggested earlier (2), construe inscriptions as all appropriately shaped portions of matter. Then the only syntactical descriptions that will fail to have actual inscriptions answering to them will be those that describe inscriptions too long to fit into the whole spatio-temporally extended universe. This limitation is hardly likely to prove embarrassing. (If we ever should be handicapped by gaps in the proof of an inscription wanted as a theorem, however, we can strengthen our rules of inference to bridge such gaps; for, the number of steps required in a proof depends upon the rules, and the rules we have adopted can be altered or supplemented considerably without violation of nominalistic standards.)

It may be interesting to observe in passing that the theoretical limitations just considered obtain under platonistic syntax as well, if that syntax construes expressions as shape-classes of inscriptions; for, shapes having no inscriptions as instances reduce to the null class and are thus identical.19 The platonist may indeed escape the limitations of concrete reality by hypostatizing an infinite realm of abstract entities -- the series of numbers -- and then arithmetizing his syntax; the nominalist, on the other hand, holds that any recourse to platonism is both intolerable and unnecessary.

Notes

19 According to the classical principles of syntax, any two expressions x and y have concatenate x^y, and moreover x^y is always distinct from z^w, unless the characters occurring in x and in y are successively the same as those in z and in w. This combination of principles is as untenable from the point of view of a platonistic syntax of shape-classes as from the point of view of nominalism.

Contents -- Go to §11