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

Now that we have specified the characters and formulas of the object language within our nominalistic syntax language, the next problem is to describe the sorts of notational operations that pass for logical proof among the users of that object language. A full solution of this problem would consist in the formulation, in our syntax language, of a condition that is necessary and sufficient in order that an inscription xbe atheoremof the object language.The theorems are those formulas of the object language that follow from certain axioms by certain rules of inference. The axioms should be so chosen that we can obtain from them, by the rules of inference, every formula that is valid according to the logic of alternative denial and quantification and, in addition, a goodly array of formulas whose alleged validity is supposed to proceed from special properties of class-membership. We cannot aspire to completeness in this last regard, in view of Gödel's result. There are many essentially equivalent sets of axioms suitable to the above purposes. The axioms that we shall adopt fall under three heads: axioms of alternative denial, axioms of quantification, andaxioms of membership. In setting them forth let us understand "~ . . ." as short for " ( . . . | . . . ) ".Axioms of alternative denial: All formulas of the form:

((P | (Q | R)) | ((S | ~S) | ((S | Q) | ~(P | S)))), ^{15}like letters being replaced by like formulas.

Axioms of quantification: All formulas of the forms:

- (1)
- ((
v)(P | ~Q) | ~((v)P | ~(v)Q)),

- (2)
- (R | ~(
v)R) (where "v" is not free in "R"),

- (3)
- ((
v)P | ~S) (where "S" is the result of substituting some variable for "v" in "P").If the reader reflects that the sign-combination " | ~" amounts to "-->", he will recognize in the forms (1) -- (3) a familiar set of axiom-schemata for quantification theory.

^{16}Like capitals in (1) -- (3) are of course to be understood as replaced by like formulas, and the vees by like variables. The two brief provisos appended to (2) and (3), above, may be stated more precisely as follows: (i) the formulas supplanting the "R"s contain no free variables like the variables supplanting the vees, and (ii) the formula supplanting the "S" is like the formula supplanting the "P" except perhaps for containing other free variables, like one another, in place of all free variables like the variable supplanting the vee.Axioms of membership: Here it happens that a limited list of specific expressions is adequate; e.g., Hailperin's.^{17}Let us suppose such a list put over into the primitive notation of our object language and set down here; then our axioms of membership are all inscriptions like those in the list.In addition to the axioms, we need two rules of inference: (1) From any formula, together with the result of putting a formula like it for "P" and any formulas for "Q" and "R" in "(P | (Q | R))", infer any formula like the one which was put for ''Q''. ^{18}(2) From any formula infer any quantification thereof. To reach a definition of "Axiom" we must first be able to define what it means to be an axiom of any given one of the five kinds above described. A simple auxiliary definition will be useful:

- D22.
- D
xy= (]z)(Likeyz& ADxyz);i.e., that

xis adenialofymeans thatxis the alternative denial ofyand some other inscription exactly likey.Definition of "AAD x", meaning thatxis anaxiom of alternative denial, is achieved by stating formally what we can observe from the general schema already given: that every axiom of alternative denial is an alternative denial of two formulas; one of these two main components is an alternative denial of formulas of which one is an alternative denial of formulas; the other of the two main components is an alternative denial of formulas of which one is an alternative denial of a formula with a formula like the denial of that formula, while the other is . . . etc., etc. In symbols:

- D23.
- AAD
x= (]f)(]g)(]h)(]i)(]j)(]k) (]l)(]m)(]n)(]p)(]q)(]r) (]s)(]t)(]u)(]w)(]y)(]z)(Fmlaf& Fmlag& Fmlah& Fmlai& Likeki& Likelg& Likemf& Likeni& ADpgh& ADqfp& Dri& ADsir& ADtkl& ADumn& Dwu& ADytw& ADzsy& ADxqz).Formulation of "AQ1 x", meaning thatxis an axiom of quantification of kind (1), proceeds in the same way; we shall omit the definition.Formulation of "AQ2 x" offers the one additional difficulty that in order to express stipulation (i), appearing in the above description of the axioms of quantification, we must have a definition offree venable. A variablexis a free variable in an inscriptionyifxis a segment ofynot followed by any additional accents iny, and if furthermorexis not a segment of any segment ofythat consists of a formula preceded by a quantifier consisting of a variable likexframed in parentheses.

- D24.
- Free
xy=. Vblx& Segxy& (z)(w)(Acw& Czxw& .--> ~Segzy) & (q)(r)(s)(t)(u)(LParq& Likerx& RPars& Fmlat& Cuqrst& Seguy& .--> ~Segxu).The definition of "AQ2

x" is then quite straightforward and may be omitted here.Formulation of "AQ3 x" offers a further complication for nominalistic syntax. The problem lies in the notion ofsubstitution, involved in stipulation (ii) . Letzandwbe the respective formulas supplanting the "P" and "S" of (3), letybe the variable supplanting the "v", and letzbe like the free variables which are to appear in w in place of the free variables likeyinz. We have to find a way within nominalistic syntax of defining "Substwzyz", meaning thatthe formula w is like the formula z except for having free variables like. Our method of definition depends upon the fact that the condition in the foregoing italics is equivalent to the following one:xwhereverzcontains free variables like yWhat remains when all free variables like y are omitted from the formula. The formal definition is as follows:zis like what remains when some free variables likexare omitted from the formula w

- D25.
- Subst
wxyz=. Fmlaw& Fmlaz& (]t)(]u){Liketu& (s)[Chars--> : (r)(Likery& Freerz.--> ~Segsr) & Segsz.<--> Segsu: (r)(Likerx& Freerw.--> ~Segsr) .-->. Segsw<--> Segst] & (s)(r)(Likerz& Freerw& Segsr& Segst.--> Segrt)}.It was largely for the purpose of this definition that we so defined likeness of inscriptions as to allow their characters to be differently spaced.

Now that this definition is accomplished, the definition of "AQ3 x" offers no further difficulty (and is omitted here).Definitions of axioms of the fifth and final kind -- the axioms of membership, "AM" -- present no problem; we can specify them in our syntax simply by spelling them out explicitly with the help of our primitive predicates. We are then ready for a general definition of what it means for xto be an axiom of our object language. It means simply thatxis an axiom of one of the five kinds specified.

- D26.
- Axiom
x=. AADxV AQ1xV AQ2xV AQ3xV AMx.An inscription xis called animmediate consequenceof inscriptionsyandzjust in casexfollows fromyandzby one application of rule of inference (1), or fromyby rule of inference (2).

- D27.
- IC
zyz= (]r)(]s)(]t)(]u)(]w)(Likerx& Likesy& Liketz: ADurw& ADstuV ADtsu.V Qfnrs).Notes ^{15}This is Lukasiewicz's simplification of Nicod's axiom schema. See Jan Lukasiewicz, "Uwagi o Aksyomacie Nicod'a i o 'Dedukeyi Uogolniajacej' ", Ksiega pamiatkowa Polskiego Towarzystwa Filozoficznego we Lwowie, 1931, pp. 2-7; also Jean Nicod, "A Reduction in the Number of Primitive Propositions of Logic",Proceedings of the Cambridge Philosophical Society,Vol. 19 (1917-1920), pp. 32-41.^{16}They answer to 4.4.4, 4.4.5, and 4.4.6 of F. B. Fitch, "The consistency of the Ramified Principia",Journal of Symbolic Logic, Vol. 3 (1938), pp. 140-149; also to *102-*104 of W. V. Quine,Mathematical Logic, p. 88.^{17}Theodore Hailperin, "A Set of Axioms for Logic,"Journal of Symbolic Logic, Vol. 9 (1944), pp. 1-19.^{18}This is Nicod's generalization ofmodus ponenssee footnote 15.Contents -- Go to §10