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 zandwwill never be a segment of a larger formula, nor will it contain as segments any formulas other than those that are segments ofzalone orwalone. Accordingly it will be convenient in general to speak ofxas alineofy(whereymay or may not be a proof) ifxis a formula that is part ofybut not part of any other formula iny.

- D28.
- Line
xy= (z)(Fmlaz& Partxz& Partzy.<-->.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 precedinglines. 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 ycontains as parts some lines of a proofxbut none that are axioms, then some line ofxthat lies inymust be an immediate consequence of lines ofxthat lie outsidey. The following, then, is our definition:

- D29.
- Proof
x= (y){(]z)(Linezx& Partzy) & (w)(Axiomw& Linewx.--> ~Partwy) .--> (]s)(]t)(]u)(Linesx& Partsy& Linetz& ~Partty& Lineux& ~Partuy& ICstu)}.In order to establish that this definition is adequate to our purposes, we shall now show (1) that if xis a 'proof' in the sense of D29, then we can specify an order of 'precedence' among the lines ofxsuch that every line is either an axiom or an immediate consequence of 'earlier' lines; and we shall show conversely that (2) ifxis such that an order of precedence of the above kind can be specified among its lines, thenxis 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 xby picking out, in an arbitrary order L_{1}, L_{2}. . . , L_{k}, all those lines ofxthat are axioms. Next, from among the remaining lines ofx, we pick one, call it L_{k+1}, which is an immediate consequence of lines from among L_{1}, L_{2}, . . . , L_{k}. (There will be such a line; for, by D29, that individual y which consists of all linesxexcept L_{1}, L_{2}, . . . , L_{k}must contain a line that is an immediate consequence of lines ofxoutside y.) Next, from among the remaining lines ofx, we pick one -- call it L_{k+2}-- which is an immediate consequence of lines from among L_{1}, L_{2}. . . , L_{k+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 xcan 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 ofxbut none that are axioms. From among those lines ofxthat are parts ofy, 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 ofx. But it is not an axiom, forycontains none of the lines ofxthat are axioms. Hence it is an immediate consequence of earlier lines ofx; and those earlier lines are not in y. We see therefore that y contains a line ofxthat is an immediate consequence of lines ofxoutside y. Since y was taken asanyindividual containing some lines ofxbut none that are axioms, it follows thatxis 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 xare indeed formulas, butxmay 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 yfor which a proofxexists, it will be true that for each inscriptionzthat is likey, and that lies outside ofx, a proof will also exist, consisting for example ofztogether with those lines ofxthat are not identical withy. Hence ifyis a theorem all such inscriptions like it will also be theorems. But suppose that some inscriptionwthat is likeylies embedded within some line t in the proofx, and suppose that no other line liketexists; in this case there may be no proof forw, so that some inscriptions like the theoremymay 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)(Proofy& Linezy& Likexz) .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 expressionsxandyhave concatenatex^y, and moreoverx^yis always distinct fromz^w, unless the characters occurring inxand inyare successively the same as those inzand inw. 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