Mathematical Logic: Proofs of Completeness and Incompleteness

views updated

Mathematical Logic: Proofs of Completeness and Incompleteness

Overview

Philosophers, logicians, and mathematicians in the first half of the twentieth century made significant progress toward understanding the connections between mathematics and logic. Major results of these investigations include the Löwenheim-Skolem theorem (1920), Gödel's first and second incompleteness theorems for axiomatic systems (1931), and Henkin's completeness theorem for first-order logics (1949).

Background

Logicians use the terms "formal system," "formal theory," "formal language," and "logic" almost interchangeably to refer to any set K whose members are in practice subject to rules of inference. Each formal system has three components: grammar, deductive system, and semantics, which together determine the logic of K. The grammar consists of the members of K, such as symbols, logical operators, constants, variables, etc., and the rules governing the formation of terms. A "wellformed formula" (known as a wff) is any statement made according to these formation rules. The deductive system is the process by which proofs are generated. A proof in a formal system is a series of wffs (p₁...p_n) where p_n=q and where q is the statement which was to be proved. The semantics is the meaning of statements in K. The same grammar and semantics can have different deductive systems; similarly, the same grammar and deductive system can have different semantics.

These three components of actual practice are designated respectively by "G,D,S"; the components of the model or formal structure of practice are designated by the corresponding Greek letters: "Γ,Δ,Σ." A model is a planned structure that exhibits in a formal system a precise way. Both mathematics and logic contain formal systems that can be modeled.

The logic of mathematics is metamathematics, and generally has two aspects: proof theory, which studies and Δ, and model theory, which studies Γ and Σ. The major founders of proof theory and model theory were, respectively, David Hilbert (1862-1943) and Alfred Tarski (1901-1983).

Among the concerns of metamathematics are the completeness and soundness of formal systems.

In Δ, the desired characteristic of sentences is provability or deducibility; in Σ, truth or logical consequence. A proved sentence in Δ is a theorem of the system. A valid sentence in Σ is a logical truth or a logical consequence of the system. Logicians designate the provability of q by ⊢ q and the logical truth of q by ⊢ q.

A formal system is complete if every valid or true statement in that system is provable within the system. Completeness can be either strong or weak. Strong completeness says that when q is a logical consequence of premises p in the semantics of K (p ⊢q in Σ_K), then q is provable from p in the deductive system of K (p ⊢ q in Δ_K), then q is a logical consequence of p in the semantics of K (p ⊢ q in Σ_K). Weak soundness says that when there is a proof of q in K from no assumptions (⊢ q in Δ_K), then q is logically true in K (⊢ q in Σ_K).

One of the most important results of model theory is the Löwenheim-Skolem theorem, produced in 1915 by Leopold Löwenheim (1878-1957) and improved in 1920 by Thoralf Albert Skolem (1887-1963). It says that any mathematical theory that has a model has a countable model. That is, the set of all the members of the model can be put into one-to-one correspondence with either the set of positive integers or some subset of it. The Skolem paradox (1922) of this theorem is that if an uncountably infinite set, such as the set of real numbers, has a model, then in that model the real numbers would be countable.

There are many completeness proofs. Paul Isaac Bernays (1888-1977) proved completeness for propositional logic in 1918. Kurt Gödel (1906-1978) proved it for first-order predicate logic in 1930. Garrett Birkhoff (1911-1996) offered a proof of strong completeness for equational logics. Probably best known is the proof of Leon Henkin (1921- ). Henkin did not use the "weak/strong" terminology at that time, but in 1996 he claimed that in his 1947 doctoral dissertation at Princeton University he had proved strong completeness for the first-order calculus. Weak completeness follows trivially as a corollary to Henkin's proof.

In 1931 Gödel proved incompleteness for formal systems. His first incompleteness theorem states that for any consistent formal system adequate for number theory, there exists at least one true statement that is not provable or decidable within the system. His second incompleteness theorem, a corollary to the first, states that no such system can serve as its own metalanguage, i.e., it cannot be employed to show its own consistency.

Impact

Gödel's incompleteness proofs had wide-ranging and serious impact. They disproved Hilbert and Bernays' belief that all mathematics could be formulated as a single internally consistent and coherent theory. They proved that the internal consistency of several basic mathematical theories, including the arithmetic of Giuseppe Peano (1858-1932) and the set theory of Ernst Zermelo (1871-1953) and Abraham Fraenkel (1891-1965) cannot be proved within their own languages, but only in stronger metalanguages. This negative result does not mean that these theories are inconsistent, but only that their consistency must be established by theories other than themselves.

Completeness and soundness are important in computer science, especially with regard to software design. Results in mathematical logic are applicable to the theories of monoids, strings, groups, semi-groups, rings, fields, Boolean algebras, and lattices. Logic illuminates the mathematics of very large or inaccessible cardinals, the connection between ordinality and cardinality, countably infinite sets, number theory, and recursion theory.

ERIC V.D. LUFT