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 x be a theorem of 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, and axioms 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.
- Dxy = (]z)(Like yz & ADxyz);
i.e., that x is a denial of y means that x is the alternative denial of y and some other inscription exactly like y.
Definition of "AADx", meaning that x is an axiom 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.
- AADx = (]f)(]g)(]h)(]i)(]j)(]k) (]l)(]m)(]n)(]p)(]q)(]r) (]s)(]t)(]u)(]w)(]y)(]z)(Fmla f & Fmla g & Fmla h & Fmla i & Like ki & Like lg & Like mf & Like ni & ADpgh & ADqfp & Dri & ADsir & ADtkl & ADumn & Dwu & ADytw & ADzsy & ADxqz).
Formulation of "AQ1 x", meaning that x is 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 of free venable. A variable x is a free variable in an inscription y if x is a segment of y not followed by any additional accents in y, and if furthermore x is not a segment of any segment of y that consists of a formula preceded by a quantifier consisting of a variable like x framed in parentheses.
- D24.
- Free xy =. Vbl x & Seg xy & (z)(w)(Ac w & Czxw & .--> ~Seg zy) & (q)(r)(s)(t)(u)(LPar q & Like rx & RPar s & Fmla t & Cuqrst & Seg uy & .--> ~Seg xu).
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 of substitution, involved in stipulation (ii) . Let z and w be the respective formulas supplanting the "P" and "S" of (3), let y be the variable supplanting the "v", and let z be like the free variables which are to appear in w in place of the free variables like y in z. We have to find a way within nominalistic syntax of defining "Subst wzyz", meaning that the formula w is like the formula z except for having free variables like x wherever z contains free variables like y. Our method of definition depends upon the fact that the condition in the foregoing italics is equivalent to the following one: What remains when all free variables like y are omitted from the formula z is like what remains when some free variables like x are omitted from the formula w. The formal definition is as follows:
- D25.
- Subst wxyz =. Fmla w & Fmla z & (]t)(]u){Like tu & (s)[Char s --> : (r)(Like ry & Free rz .--> ~Seg sr) & Seg sz .<--> Seg su : (r)(Like rx & Free rw .--> ~Seg sr) .-->. Seg sw <--> Seg st] & (s)(r)(Like rz & Free rw & Seg sr & Seg st .--> Seg rt)}.
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 x to be an axiom of our object language. It means simply that x is an axiom of one of the five kinds specified.
- D26.
- Axiom x =. AADx V AQ1 x V AQ2 x V AQ3 x V AMx.
An inscription x is called an immediate consequence of inscriptions y and z just in case x follows from y and z by one application of rule of inference (1), or from y by rule of inference (2).
- D27.
- ICzyz = (]r)(]s)(]t)(]u)(]w)(Like rx & Like sy & Like tz : ADurw & ADstu V ADtsu .V Qfn rs).
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 of modus ponens see footnote 15. Contents -- Go to §10