METALOGIC

the study and analysis of the semantics (relations between expressions and meanings) and syntax (relations among expressions) of formal languages and formal systems. It is related to, but does not include, the formal treatment of natural languages. (For a discussion of the syntax and semantics of natural languages, see the articles linguistics and semantics.) the study and analysis of formal languages and formal systems with regard to their semantics (the relations between expressions and meanings) and syntax (the relations among expressions). The discipline thus includes the study of both mathematics and logic insofar as these are treated formally and in abstraction from their practical applications. The chief early impetus to the development of metalogic was the discovery, in the 19th century, of different geometries and the consequent desire to separate abstract mathematics from spatial intuition. David Hilbert, in his Grundlagen der Geometrie (1899; The Foundations of Geometry), organized Euclid's geometry into a more rigorous axiomatic system that uncovered many hidden axioms and opened the way for related attempts to axiomatize other areas of mathematics and logic. As a consequence of this desire for transparency and complete specification, greater attention came to be paid to the formal syntactic features of the languages and systems used rather than merely to their intuitive meanings. The use of predicate calculus in the determination of relationships further advanced the convergence of axiomatic mathematics, semiotics, and logic toward metalogic. Certain aspects of metalogic made possible an attempt to develop a metalogical formalization of the physical and behavioral sciences. Building on Ludwig Wittgenstein's early work, Rudolf Carnap and other exponents of Logical Positivism sought to analyze these sciences into formal languages consisting of logically valid sentences with universal logical ranges (sentences that are true in all possible worlds) and factually true sentences of a more restricted range. One product of this attempt was to be a formal solution to the problem of meaning. The collapse of these expectations led to a narrowing of the scope of metalogic. A great deal of work of a mathematical nature has been done in the areas of axiomatic set theory, model theory, and recursion theory. Currently the central questions of metalogic are those of the completeness and consistency of a formal system based on axioms. Two fundamental contributions to the understanding of these questions were made by Kurt Gdel. In 1931 he established that for any formal system that is sufficiently complex to generate an elementary arithmetic, it is impossible for that system to prove its own consistency, i.e., there exists no consistency proof of such a system that can be formalized in the system itself. Then in 1934 he introduced the concept of recursive functions (functions mechanically computable by a finite series of purely combinatorial steps); this idea, further elaborated by the work of Alonzo Church, Alan M. Turing, and Emil L. Post, resulted in the development of recursion theory. By means of this theory it was possible to prove that certain classes of problems are either mechanically solvable or unsolvable, and it became possible for logicians to arrive finally at a sharply defined concept of a formal axiomatic system and at sharply defined concepts of decidability. Church extended Gdel's findings in 1936 to show that interesting formal systems are undecidable both with regard to theorems and with regard to true sentences. The incompleteness theorem shows that truth in a system to which the theorem applies is undecidable, for if they were decidable then all true sentences would form a recursive set and could be taken as the axioms of a formal system that would be complete. Or alternatively, since truth in the language of a system is itself not representable (definable) in the system, it cannot, if all recursive or computable functions and relations are representable in the system, be recursive (i.e., decidable) itself. From this it follows that a consistent system is undecidable with respect to theorems as well. Despite the proof that interesting formal systems are incomplete and undecidable, it has been shown by M. Presburger and Thoralf Skolem (both in 1930) that arithmetic is decidable with regard to addition or multiplication alone. Alfred Tarski also developed (in 1951) a decision procedure for elementary geometry and elementary algebra. With regard to consistency proofs the work of Gerhard Gentzen (1936) opened up an area of extensive work in classical number theory. Gdel (in 1958) extended his interpretation from classical number theory to intuitionistic theory and obtained constructive interpretations for sentences of classical number theory in terms of primitive recursive functionals. Recent work in consistency proofs has extended the work of both these men and has tried to make constructive notations for the second number class of Georg Cantor. Consistency proofs have sparked much discussion about their implications for epistemology. The metalogic concern with completeness and consistency has produced important results with regard to formal logic. It can be shown that propositional calculus is complete because every valid sentence in it is a theorem. Its consistency follows from the validity claim of its axioms, that they are true in all possible worlds, and because the rules of inference carry from valid sentences to valid sentences. Since all and only valid sentences are theorems, the calculus is decidable. With regard to first order predicate calculus, it can be proved that it is consistent and that all its theorems are valid. More importantly it has been proved that the calculus is complete but undecidable. The former was proved by Gdel in 1930 and the latter by Church and Turing in 1936 using very different methods. Another important field of metalogic has been model theory, in which the interpretation of theories formalized in the framework of formal logic are studied. Model theory has yielded, for example, proof that no theory with an infinite model can be categorical or such that any two models of the theory are isomorphic, whether the model be constructed of infinite cardinal numbers or of any uncountable cardinality. Model theory also enabled Per Linstrm in 1969 to establish roughly that within a broad class of possible logics, elementary logic is the only one that satisfies the requirements of axiomatizability of the LwenheimSkolem theorem. Model theory has branched out to develop models of second order logic and infinitary logics, and with its concepts of ultrafilters, ultraproducts, and ultrapowers it has been used to develop an exact foundation for the classical differential calculus using infinitesimals. Additional reading Jon Barwise and S. Feferman (eds.), Model-Theoretic Logics (1985), emphasizes semantics of models. J.L. Bell and A.B. Slomson, Models and Ultraproducts: An Introduction, 3rd rev. ed. (1974), explores technical semantics. Richard Montague, Formal Philosophy: Selected Papers of Richard Montague, ed. by Richmond H. Thomason (1974), uses modern logic to deal with the semantics of natural languages. Martin Davis, Computability & Unsolvability (1958, reprinted with a new preface and appendix, 1982), is an early classic on important work arising from Gdel's theorem, and the same author's The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems, and Computable Functions (1965), is a collection of seminal papers on issues of computability. Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey (1988), takes a look at where Gdel's theorem on undecidable sentences has led researchers. Hans Hermes, Enumerability, Decidability, Computability, 2nd rev. ed. (1969, originally published in German, 1961), offers an excellent mathematical introduction to the theory of computability and Turing machines. A classic treatment of computability is presented in Hartley Rogers, Jr., Theory of Recursive Functions and Effective Computability (1967, reissued 1987). M.E. Szabo, Algebra of Proofs (1978), is an advanced treatment of syntactical proof theory. P.T. Johnstone, Topos Theory (1977), explores the theory of structures that can serve as interpretations of various theories stated in predicate calculus. H.J. Keisler, Logic with the Quantifier There Exist Uncountably Many', Annals of Mathematical Logic 1:193 (January 1970), reports on a seminal investigation that opened the way for Jon Barwise et al. (eds.), Handbook of Mathematical Logic (1977); and Carol Ruth Karp, Language with Expressions of Infinite Length (1964), which expands the syntax of the language of predicate calculus so that expressions of infinite length can be constructed. C.C. Chang and H.J. Keisler, Model Theory, 3rd rev. ed. (1990), is the single most important text on semantics. F.W. Lawvere, C. Maurer, and G.C. Wraith (eds.), Model Theory and Topoi (1975), is an advanced, mathematically sophisticated treatment of the semantics of theories expressed in predicate calculus with identity. Michael Makkai and Gonzalo Reyes, First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories (1977), analyzes the semantics of theories expressed in predicate calculus. Saharon Shelah, Stability, the F.C.P., and Superstability: Model-Theoretic Properties of Formulas in First Order Theory, Annals of Mathematical Logic 3:271362 (October 1971), explores advanced semantics.