The Finiteness Problem for Principia Mathematica

Emil Post was a graduate student at Columbia University from 1917 to 1920 and attended during those years a seminar by his advisor Cassius Keyser on Whitehead and Russell’s [61] Principia Mathematical Nevertheless, the main influence on his programmatic approach to Principia Mathematica and symbolic logic more gener- 2The source of all biographical data concerning Post is Martin Davis [11].—Keyser wrote a review of the first two volumes of Principia Mathematica, see (Keyser [29]). In Sect. 7.8 we will discuss some of his views that seem to have influenced Post.

ally seems to have been C. I. Lewis.[1] Lewis’s Survey of Symbolic Logic from 1918 [34] distinguishes, in Chapter 6, Sects. 2 and 3, between the heterodox and orthodox views of “the nature of mathematics and of logistic”. On the orthodox view Lewis writes:

“Logistic” may be taken to denote any development of scientific matter, which is expressed exclusively in ideographic language and uses predominantly the operations of symbolic logic. (Lewis [34], p. 340)

From that viewpoint mathematical systems are “nothing more nor less than ... complex logical structure[s]”. Their subject matter is “freed from ... appeal to intuition or perception”; after all, in proofs that proceed in accord with logical principles, “nothing depends upon the fact that the terms denote certain . entities”. (Lewis [34], pp. 340-341).

Lewis views the treatment of Principia Mathematica as orthodox and remarks on its logistic:

One might characterize the logistic of Principia Mathematica roughly by saying that the order of logistic is assumed, and the order of the other branches then follows from the meaning of their terms. (Lewis [34], p. 354)

From the heterodox view the individual steps in proofs are not logical operations, but “fundamentally arbitrary” and definitely pre-logical, since “they underlie the proofs of logic as well as of other branches”. Lewis explains, “The assumption of these operations—substitution, etc.—is the most fundamental of all the assumptions of logistic.” Thus, a quite different view of the subject emerges:

It is possible to view the subject in a way, which makes such pre-logical principles the fundamentally important thing, and does not regard as essential the use of symbolic logic as foundation. (Lewis [34], p. 355)

As a consequence of the non-foundational view of logic, a mathematical system “is any set of strings of recognizable marks in which some of the strings are taken initially and the remainder derived from these by operations performed according to rules which are independent of any meaning assigned to the marks.” (Lewis [34], p.355).

Post takes up Lewis’s heterodox view and, in his Columbia dissertation, investigates the sentential subsystem of Principia Mathematica from a strictly metamathematical perspective. The thesis is identical with the article Introduction to a General Theory of Elementary Propositions that was published in 1921 as [38]. The work aimed for the “highest generality” that, according to Post, had not been reached by Whitehead and Russell:

.owing to the particular purpose the authors [Whitehead and Russell] had in view they decided not to burden their work with more than was absolutely necessary for its achievement, and so gave up the generality of outlook which characterized symbolic logic.

(Post [38], p. 163)

In the first part of the paper, Post attempts to recover this generality of outlook. The resulting developments are viewed, in accord with the heterodox perspective, as purely formal ones; thus, any useful “instruments of logic or mathematics” will be employed for their study. In the Introduction, Post emphasizes the central point that the theorems of the first part of his paper are about the system of sentential logic; they are not included in it.

To underline the significance of this central point, Post states that his “most important theorem” gives a “uniform method for testing the truth [i.e., provability] of any proposition of the system” and allows establishing relations between propositions. Such relations show definitely “that the postulates of ‘Principia’ are capable of developing the complete system of the logic of propositions without ever introducing results extraneous to that system—a conclusion that could hardly been arrived at by the particular processes used in that work.” (Post [38], p. 164) This remark appeals to the completeness theorem for the calculus that can be extracted from the corollary Post formulated on page 171: The set of true formulae [i.e., provable ones] is identical with the set of positive ones [i.e., tautologies].4

How is the heterodox view of the system realized? Through, what is for us today, a standard presentation of the syntax of a logical system. The well-formed formulae (enunciations) are inductively defined from variables p, p1, p2,..., q, q1, q2,..., r, r1, r2,... using only the connectives (primitive functions) ~ and v; the definition is labeled by I. Then the rule of substitution is stated and labeled by II: “The assertion of a function involving a variable p produces the assertion of any function found from the given one by substituting for p any other variable q, or ~ q, or (q v r).” The only inference (production) rule for deducing theorems (assertions) is modus ponens. It takes the form III:

“b P” and “b:~ P. v .Q” produce “b Q.”,

where P and Q are meta-variables. Finally, the axioms (primitive assertions) are taken from Principia Mathematica and presented under IV:

b:~ (p v p). v .p,

b:~ q. v .p v q,

b:~ (p v q). v .q v p.

b:~ [p v (q v r)]. v .q v (p v r),

b: . ~ (~ q v r).v :~ (p v q). v .p v r,

Truth-values and tables are then introduced. The truth-value of a proposition is denoted by +, if it is true, and by -, if it is false. Post emphasizes that “this meaning of + and - is convenient to bear in mind as a guide to thought, but in the actual [2]

development that follows they are to be considered merely as symbols which we manipulate in a certain way”. (Post [38], p. 166) Thus, even truth-values and tables are treated as syntactic objects that can be manipulated on the basis of rules. The “most important theorem”, called by Post Fundamental Theorem, is formulated as follows:

Theorem. A necessary and sufficient condition that a function [formula] of F be asserted [proved] as a result of the postulates II, III, IV is that all its truth-values be +.

(Post [38], p. 169)

Post states, the (proof of the) Fundamental Theorem solves the flniteness problem of the sentential subsystem of Principia Mathematica as it obviously “gives a direct method for testing whether that function can or cannot be asserted”; moreover, he claims:

„.if the test shows that the function can be asserted the above proof [of the Fundamental Theorem] will give us an actual method for immediately writing down a formal derivation of its assertion by means of the postulates of Principia. (Post [38], p. 171)

There are many further informative observations, theorems, and corollaries; for example, on page 172, the “Post completeness” of the calculus is formulated as a theorem in this way:

Theorem. Every function of the system can either be asserted by means of the postulates or else is inconsistent with them.

However, here we are interested in the generalizations of the heterodox outlook on systems Post suggests developing. According to Post, two directions of further development can be pursued. The first direction concerns the extension of the decision procedure for sentential logic to other parts of Principia Mathematica. In [39], an abstract from 1921 entitled On a Simple Class of Deductive Systems, Post reports to have solved the decision problem for what we now call monadic predicate logic; the full paper was never published. More ambitious, but as we will see closely related, is the second direction:

„we might take cognizance of the fact that the system of “Principia” is but one particular development of the theory—particular in the primitive functions it employs and in the postulates it imposes on those functions—and so [we] might construct a general theory of such developments. (Post [38], p. 164)

The “syntactic” and “semantic” parts of the theory concerning sentential logic are both generalized. As to the latter and the truth-tables involved, Post considers functions with m truth-values, where m is greater than 2. His pioneering work on m-valued Truth-Systems proved to be influential; together with Lukasiewicz, Post is considered as one of the founders of many-valued logic. As to the former and the method


of postulation, Post considers a more general syntax of the subsystem he investigated. Instead of assuming only ~ and v as primitive functions, he introduces p functions fl( Pl, P2, ... Pmi), f2( Pi, P2, ••• Pm2), •••, fp( Pi, P2, ••• Pm,f) with

arbitrary numbers of arguments in order to obtain “complete generality”. The rules for constructing formulae under I are standard, and substitution II is modified from the earlier discussion to suit the wider syntactic context. Finally, modus ponens is replaced in III by production rules of a much more general form, and so are the axioms in IV. The resulting system is later considered to be in canonical form A, and the details are discussed at the beginning of Sect.7.3 below.

The remainder of this section of Post’s paper, entitled Generalization by Postulation, is viewed as “merely an introduction to the general theory”. (Post [38], p. 177) Post defines (in)consistency of a system in a new way, as one cannot make use of the function ~, which might not be among the primitive ones:

Definition. A system will be said to be inconsistent if it yields the assertion of the unmodified variable p. [Thus, the system asserts every formula.] (Post [38], p. 177)

Post’s further definitions and considerations reveal his expectations at this time. For a consistent system, a true formula is defined to be one “that can be asserted as a result of the postulates”; i.e., all the theorems of such a system are true by definition. If adding a formula to the postulates of the system makes the system inconsistent, then that formula is defined to be false.

Without any further explanation, Post asserts after the definition offalse, “We can then state that in the system ‘Principia’ every function is true or false.” That suggests to him a further definition for an arbitrary consistent system; namely, such a system is called closed if every function is either true or false. In a footnote, he remarks that he would have called such a system categorical, if that name had not been used “in a different connection”.[3] Justifying his terminology Post writes:

.. .the postulates of such a [closed] system automatically exclude the possibility of any added assertion—a state of affairs we believe to be highly desirable in the final form of a logical theory. (Post [38], p. 177)

Post clearly expected Principia Mathematica to be closed or syntactically complete, in the modern sense of this notion. Furthermore, Post emphasized already in the introduction the virtue of such a broadened outlook, namely, that it will “serve to prepare us for a similar analysis of that complete system [i.e., of Principia], and so ultimately of mathematics”. (Post [38], p. 164) It is against the background of these expectations that Post’s work in the early 1920s should be seen.

  • [1] C. I. Lewis’s influence on Post is discussed also in (Urquhart [60], pp. 619-620).
  • [2] The completeness theorem for sentential logic had been established in its modern formulation inBernays’s [2] Habilitationsschrift of 1918, for the same calculus of Principia Mathematica. Theindependence investigations that are also contained in that work were published in (Bernays [3]).—Post’s [43] book on Iterative Systems originated as a “companion piece” to his dissertation. Therehe determined “all the non-equivalent sub-languages of the language of the complete two-valuedpropositional calculus”. (Post [43], p. 3) For a contemporary view of this highly interesting work,see (Urquhart [60], Sect. 5).
  • [3] The emergence of categoricity and completeness is described in (Awodey and Reck [1]).
< Prev   CONTENTS   Source   Next >