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

8. Formulas

An atomic formula of the object language consists of two variables with an epsilon between them.

AtFmla x = (]w)(]y)(]z)(Vbl w & Ep y & Vbl z & Cxwyz).

We are supposing that the class logic to be developed in the object language will use one or another of the alternatives to the theory of types, so that the epsilons may grammatically occur between any variables without restriction.

The non-atomic formulas of the object language are constructed from the atomic formulas by quantification and alternative denial. In order to define an alternative denial we first need to be able to say that a given inscription x contains exactly as many left as right parentheses. This will be the case if x lacks parentheses altogether; and it will be the case also if the inscription which consists of all the left parentheses in x and the inscription which consists of all the right parentheses in x are equally long in the sense of D11. In symbols:

EqPar x =. (u)(LPar u V RPar u .--> ~Seg ux) V (]y)(]z){EqLng yz & (w)(Char w --> : LPar w & Seg wz .<--> Seg wy : RPar w & Seg wx .<--> Seg wz)}.

Now for an inscription x to be the alternative denial of y and z it is necessary that x consist of a left parenthesis followed by y, then a stroke, then z, and finally a right parenthesis. But this is not enough. We must make sure that the beginning and ending parentheses are 'mates' -- that is, that they are paired with each other and not with other parentheses that occur between them. Also we must make sure that the stroke between y and z is the main connective in x. We can accomplish all this by requiring that y contain an equal number of left and right parentheses, and similarly for z, but that this be true of no initial segment of x (except x itself).

ADxyz =. EqPar y & EqPar z & (r)(s)(Cxrs -->. ~EqPar r) & (]t)(]u)(]w)(LPar t & Str u & RPar w & Cxtyuzw).

The formulas of the object language comprise the atomic formulas and every inscription constructed from them by means of quantification and alternative denial. Some ways in which one might naturally seek to reduce this to a formal definition are not feasible in a nominalistic syntax.14 Our method is to begin by defining a quasi-formula as anything that is an atomic formula, an alternative denial, or a quantification of an atomic formula or alternative denial.

QuasiFmla x = (]y)(x = y .V Qfn xy : AtFmla y V (]w)(]z)ADywz).

A quasi-formula will not necessarily be a formula, since the components of the alternative denial are not required to be formulas. But in terms of this notion of quasi-formula we can now easily define formula:

Fmla x =. QuasiFmla x & (w)(y)(z)(ADwyz & Seg wx .-->. QuasiFmla y & QuasiFmla z).

In other words, a formula is a quasi-formula such that every alternative denial in it is an alternative denial of quasi-formulas.

By requiring even the shortest alternative denials in a formula x to be alternative denials of quasi-formulas, the definition requires them to be alternative denials of atomic formulas or of quantifications of atomic formulas, and this makes them genuine formulas in the intuitively intended sense of the word. Accordingly, by requiring also the next more complex alternative denials in x to be alternative denials of quasi-formulas, the definition guarantees that these also will be formulas in the intuitively intended sense; and so on, to x itself.


14 Using essentially the method of Frege's definition of the ancestral of a relation, we might say that x is a formula if it belongs to every class that contains all atomic formulas and all quantifications and alternative denials of its members. But this definition is unallowable because of its use of quantification over classes; cf. 4 above. -- There is indeed a completely general method, in syntax, of deriving ancestrals and kindred constructions without appeal to classes of expressions. This is the method of 'framed ingredients' which appears in Quine, Mathematical Logic, §56. The method consists essentially of these two steps: (1) the Frege form of definition is so revised that the classes to which it appeals can be limited to finite classes without impairing the result; (2) finite classes of expressions are then identified with individual expressions wherein the 'member' -- expressions occur merely as parts marked off in certain recognizable ways. However, when as nominalists we conceive of expressions strictly as concrete inscriptions, we find the method of framed ingredients unsatisfactory, because its success depends too much on what inscriptions happen to exist in the world. Actually, though, the nominalistic definition of proof in the present paper will be simpler than that in terms of framed ingredients; for it will not require the lines of a proof to be concatenated, nor to be marked off by intervening signs.

Contents -- Go to §9