A Reduction in the number of the Primitive Propositions of Logic
A Reduction in the number of the Primitive Propositions of Logic. By J. G. P. Nicod, Trinity College. (Communicated by Mr G. H. Hardy.)
[Received and read 30 October 1916.]
Of the four elementary truth functions needed in logic, only two are taken as indefinables in Principia Mathematica. These two have now been defined by Mr Sheffer in terms of a single new function , "p stroke q." I propose to make use of Mr Sheffer's discovery in order to reduce the number of primitive propositions needed for the logical calculus.
There are two slightly different forms of the new indefinable, for we may treat as meaning the same thing as either , or . The definition of is the same in both cases, namely , while that of simply changes from with the AND-form into with the OR-form.
However, the best course is for us to define all the four truth-functions directly in terms of the new one. In so doing, we find that, while the definition of remains the same, and those of , simply permute, as we pass from the AND-form to the OR-form, the definition of is simpler in the latter form. It is , as against .
The OR-form is therefore to be preferred.
Remarks on these Definitions.
One ought not to aim at retaining before one's mind the complex translation into the usual system, "," as the "real meaning" of the stroke. For the stroke, in the stroke-system, is simpler than either or , and from it both of them arise. We may not be able to think otherwise than in terms of the four usual functions; it will then be more in accordance with the nature of the new system to think of the , not as some fixed compound of and , but as a bare structure, out of which, in various ways, and will grow.
The above definitions give clear expression to the symmetry between OR and AND; and this, notwithstanding the choice that we had to make between an OR-form, and an AND-form. This is of some interest, because, in general, the very symmetry forces upon us an arbitrary choice, which, in turn, quite obscures the symmetry.I shall use for whenever convenient. Observe that , i.e. , forms a natural symbol for implication, allowing of permutation . We may notice in general that the new system brings the four functions into relations far closer than those in Mr Russell's system. For instance in
Every stroke-formula falls into two parts on the right and left of a central stem. It will, therefore, add to clearness to use black type instead of dots to indicate the central symbol. Further, slanting strokes are covered by straight ones: thus stands for .
The definition of the two primitive notions of the Principia in terms of a single new one tends to reduce the number of the primitive propositions needed. But how far does this reduction actually occur? Does it extend beyond the obvious substitution of "If and are elementary propositions, is an elementary prop." (Sheffer, p. 488) for *1·7 and *1·71, stating the same for and respectively? The reduction goes, as we shall presently find, very much farther.
It has first to be said, in order that we may be as precise as possible, that the whole amount gained in applying the stroke-definitions cannot with complete certainty be attributed to them. For Mr Russell's system, as it now stands, has not said its last word in that matter.
Incidentally I found that *1·4, , can be proved by means of the other four, with the unimportant change of *1·3, into . In "Association," *1·5, write for :
The left hand side, by the help of and "Summation," will be found to be implied in . The right-hand side, likewise, by , and "Summation," will be found to imply . The result then follows using "Syllogism" (obtained from "Summation" with the transformation ) twice.
Let us, however, take Mr Russell's eight propositions in the form given in Principia. It is my object to reduce them to three—two non-formal and one formal—by means of the stroke-definitions given above.
It can be shown, as a first stage, that two formal propositions are enough, namely:
It will however be found that the inverted order, , is much more advantageous than the normal syllogistic order, . For, owing to this "twist," Identity and (2) yield "Permutation," , which now enables us to eliminate the twist in (2), and revert to the normal order. From the three propositions thus obtained, the rest follow.
This, by the way, illustrates the following fundamental fact. Which form of a given principle is the most general, and contains the maximum assertion, is a function of the symbolic system used. Thus, for instance, in Mr Russell's system,
is more general than (b)
A further step has to be made in order to be left with only one formal primitive proposition. It consists in adapting to better advantage the form of the primitive propositions to the properties of the stroke-symbolism where implication is concerned. We had above
This leads us to substitute for in the "left-hand sides" of both the non-formal rule of implication and the syllogistic proposition (2) above. The reform may be further extended to the proposition (2) as a whole, which might be given in the form instead of with the proviso, if the proposition is to remain true, that must be implied in . Now, for , write the proposition (1) above, ; for (as we at this early stage know "unofficially") a true proposition will be implied by everything.
We then have the three primitive propositions of the stroke-system:
|I. If is an elementary proposition, and is an elementary proposition, then is an elementary proposition.|
|II. If is true, and is true, then is true.|
This is the non-formal rule of implication, *1·1, with the modification just explained.
I shall call II "the Rule," and III "the Prop."
Remarks on these Primitive Propositions.
Observe in II, while in III. This alternance will prove essential for the working of the calculus.
In III, I shall use for , for , for and shall speak of III as .
, by the Rule, yields the same result as the syllogistic proposition (2) above, when the left-hand side is a truth of logic. This restriction of the syllogistic form to its categorical use with an asserted premiss is a peculiar character of the first proofs to follow, and is of some philosophical interest.
One feels inclined to think that III merely asserts together (1) and (2) above. This, view, whatever may be the amount of truth it contains, takes AND too much as a matter of course, and tends to lose sight of (α) the fact that III, as a structure, is simpler than (2) alone: for III is (2) with instead of ; and (β) the very real step from to , together with the philosophical difference between two assertions and only one.
The main steps in the formal deduction are:
- Proof of "Identity," .
- Passage from to the usual implicative form .
- Elimination of the twist in , and return to the normal order .
- Proof of "Association," .
- Theorems equivalent to the definitions of , in Principia.
Proof of Identity, .
As this first proof from a single formal premiss stands in a unique position I shall, without in any way obscuring the precise play of the symbols, expound it after a more heuristic order than is usually followed.
We start with the Prop. , and the Rule enabling us to pass from the truth of to that of ; and we have to prove . This can only be reached through some proposition of the form , where is a truth of logic. The proof will thus consist in passing from to by some permutative process.
A simple two-terms permutative law we do not yet possess. Our Prop. yields only a roundabout three-terms permutation, , subject to the condition of being a truth of logic. This, however, is enough for our purpose.
In the Prop., write for , , :
being . Write now for , ; for : then by (a) and the Rule,
From (b) in the same manner,
This enables us to pass, by the Rule, from to
In order to complete the proof of , we need only find some expression which: (α) can be a value for , i.e. is a case of , and (β) is implied in some truth of logic, say . For, by , the Prop., and the Rule, as above,
In (e), write for : first by (d) and the Rule, then by and the Rule, we obtain , and so
To obtain the strictest development of the proof we have only to write for and for all through the preceding argument.
Dem.: Prop. , Id., and Rule.
Dem.: Id. , Perm., and Rule.
Dem.: By Perm. (twice), (a)
By Prop. Id.,
By Perm., result.
Return from Generalised Implication to .
Dem.: By Perm. (twice), (a)
By Prop. (a),
Write for : by Id. and Perm. (twice), result.
Dem.: Prop. Lemma, result.
Hence, by Perm., , i.e.
Dem.: In this Dem., Permutation is used to correct the twisting action of , much as handwriting has first to be inverted, if it is to be seen right in a mirror.
By Perm., and Perm.,
By Perm., , and Perm.,
By , result.
The structure of the proof is this:
We now need only the Lemma for our result to follow by Syll. twice.
The proof of this lemma—call it L—is as follows: We prove (a) , (b) . From this, by Syll. and Tautol., the result follows.
Dem.: (a) By ,
The right side of (2) implies, by Syll.,
By Id., Perm., Add.,
By Syll. twice, (2), (3), (4),
|, i.e. .|
(b) By lemma to Syll., ; by Perm. and Syll., . Hence, ; by Perm., .
Now, by Syll.:
By b, a, and Taut., result. We can now complete the proof of 'Association.'
Dem: By Syll.,
By Syll. twice, Lemma, result.
Dem.: By Syll., Assoc.,
By (1) , result.
Theorems Equivalent to the Definitions of , in Principia.
, and reciprocal theorem.
Dem.: Taut., and Syll.
Reciprocal theorem by Add., and Syll.
, and reciprocal theorem.
Reciprocal theorem by Add. instead of Taut.
and reciprocal theorem.
Dem.: Id., Def. of , preceding theorem, and Syll.
Reciprocal theorem in the same manner.
After the substance of this paper had been written, I was given the opportunity of seeing Mr Van Horn's very interesting and original paper dealing with what is practically the same subject. Mr Van Horn recognises clearly the superiority of what has been called above the OR-form over the AND-form chosen in Sheffer's text. This deserves the more notice, as Mr Van Horn, I understand, had not Sheffer's article at hand in the time he was writing his own paper. His , as will be seen from the definition he gives, is indistinguishable from . I was much attracted by the harmonious character of Mr Van Horn's third Axiom. It seems to me therefore all the more desirable that certain objections, which Mr Van Horn's proofs in their present form naturally suggest to the reader, should be dealt with.
(α) It is not quite plain to me whether "of the same truth-value" (say for short), "of opposite truth-values" (say ), are used as indefinables, or as abbreviations. If the former, we have no right to go, e.g., from and , to , etc., without some axiom to that effect, connecting and with . If, on the other hand, and are abbreviations—as it seems to me they are—the two parts of Axiom 3 stand for not less than four propositions:
|1.||If and ,||.|
|2.||If and ,||.|
|3.||If and ,||.|
|4.||If and ,||.|
We cannot assert the first two, or the last two, or all four, propositions together, because we should then need , , before we could make any use of such a synthetic Axiom.
This uncertainty as to the status of and is not without its effect upon the proofs. Consider, for instance, Th. 3. In the proof, "1°: true. By Axiom 3, false" will be seen to require , concerning the origin of which, and the relation it has to (Th. 4), which it indirectly serves to prove, Mr Van Horn says nothing.
(β) In his extensive use of the Principle of Excluded Middle, Mr Van Horn makes no explicit mention of the last steps, that lead from , to . These steps would seem to require several propositions: (1) those carrying us from to —"Summation," plus "Permutation," presumably—and (2) "Tautology" . As Mr Van Horn uses the principle of Excluded Middle in this particular way in the first formal proof given—that of Th. 3—both the principle itself and the propositions required for its use ought, I think, to be deduced immediately from Axiom 3; and I do not see how this is possible.
- Sheffer, Trans. Amer. Math. Soc. Vol. xiv. pp. 481–488.
- Sheffer, loc. cit., footnote, p. 488.
- thus corresponds to what is termed the Disjunctive relation in Mr W. E. Johnson's writings.
- By or I mean (following Mr Russell) the substitution of for or , for , . By (e.g.) I mean the result of effecting the substitution in .
- This is the proposition shown by Sheffer to imply the analogous propositions *1·7 and *1·71 in Principia.
- This use of the Rule by anticipation, with still undetermined 's and 's, is in truth contrary to the nature of a non-formal rule, which must never be used to build up the structure of an argument. It must always be possible to dispense with all such 'anticipated' assertions in the final form of a proof. This will be seen to be very easy in the present case.
- (a) means the use of the Rule to pass from to in .