1967:33). This foundational choice, and their equivalence also applies to predicate logic (Kleene 1967:318). In his introduction to Post 1921, van Heijenoort observes that both the "truth-table and the axiomatic approaches are clearly presented". This matter of a proof of consistency both ways (by a model theory, by axiomatic proof theory) comes up in the more-congenial version of Post's consistency proof that can be found in Nagel and Newman 1958 in their chapter V "An Example of a Successful Absolute Proof of Consistency". In the main body of the text they use a model to achieve their consistency proof (they also state that the system is complete but do not offer a proof) (Nagel & Newman 1958:45–56). But their text promises the reader a proof that is axiomatic rather than relying on a model, and in the Appendix they deliver this proof based on the notions of a division of formulas into two classes K1 and K2 that are mutually exclusive and exhaustive (Nagel & Newman 1958:109–113). Gödel (1930): The first-order predicate calculus is complete The (restricted) "first-order predicate calculus" is the "system of logic" that adds to the propositional logic (cf Post, above) the notion of "subject-predicate" i.e. the subject x is drawn from a domain (universe) of discourse and the predicate is a logical function f(x): x as subject and f(x) as predicate (Kleene 1967:74). Although Gödel's proof involves the same notion of "completeness" as does the proof of Post, Gödel's proof is far more difficult; what follows is a discussion of the axiom set. Completeness Kurt Gödel in his 1930 doctoral dissertation "The completeness of the axioms of the functional calculus of logic" proved that in this "calculus" (i.e. restricted predicate logic with or without equality) that every valid formula is "either refutable or satisfiable" or what amounts to the same thing: every valid formula is provable and therefore the logic is complete. Here is Gödel's definition of whether or not the "restricted functional calculus" is "complete": "... whether it actually suffices for the derivation of every logico-mathematical proposition, or where, perhaps, it is conceivable that there are true propositions (which may be provable by means of other principles) that cannot be derived in the system under consideration." The first-order predicate calculus This particular predicate calculus is "restricted to the first order". To the propositional calculus it adds two special symbols that symbolize the generalizations "for all"