Gödel's completeness theorem

Gödel's completeness theorem is a big idea in mathematical logic that helps us understand the relationship between what is true and what we can prove. It tells us that if a statement is true in every possible situation (or "model") for a certain set of rules, then we can actually write down a step-by-step proof for that statement using those rules. In simpler words, anything that seems true in every case can be shown to be true with logic!

This theorem is very important because it connects two parts of logic: model theory, which looks at what is true in different situations, and proof theory, which studies how we build proofs. It shows that these two areas are closely linked.

The theorem was first proven by Kurt Gödel in 1929. Later, Leon Henkin made the proof easier to understand in his Ph.D. thesis in 1949, and Gisbert Hasenjaeger simplified it even more in 1953. Together, these ideas help mathematicians and logicians know when they can trust their proofs to match true statements.

Preliminaries

There are many ways to build rules for deciding if something in math logic is true, called deductive systems. Examples include natural deduction and Hilbert-style systems. In all these systems, a formal deduction is a step-by-step list of statements that leads to a final conclusion. We can check these steps using a computer or by hand.

A statement in math logic is logically valid if it is true in every possible situation. A deductive system is complete if every logically valid statement can be shown to be true using the system's rules. The completeness theorem tells us that for each of these systems, this is possible. The opposite idea, called soundness, means that only statements that are logically valid can be proven using the system's rules. When a system is both sound and complete, it is perfect, meaning any true statement can be proven, and only true statements can be proven.

Statement

Gödel's completeness theorem is a big idea in math logic. It tells us that if a math statement is true in every possible situation (model) we can imagine, then we can also prove it using certain rules. This means there are no "true but unprovable" statements in this system.

The theorem works for any set of math rules called a "first-order theory." If a statement is true for every example of that theory, we can write a step-by-step proof using the theory's rules. This links two ways to think about math: what is true in all situations, and what we can prove with rules.

The theorem also connects to ideas like consistency — meaning a set of rules doesn't contain any contradictions. If a theory is consistent, it always has a model where all its rules hold true.

Consequences

One important result of Gödel’s completeness theorem is that we can list all the results that follow from a theory in a clear way. We do this by listing all the possible proofs we can make from the theory’s basic rules, and this helps us see all the conclusions we can reach.

This theorem also shows that what we call a “proof” or a “theorem” really only depends on the basic rules we start with, not on the specific way we choose to write out our proofs.

Relationship to the incompleteness theorems

Gödel's incompleteness theorems show that in mathematics, there are limits to what we can prove using certain systems. These theorems tell us that in any system that is strong enough to handle basic arithmetic, there will always be statements that cannot be proven true or false within that system.

The completeness theorem and the incompleteness theorems are related but different. While the completeness theorem tells us that if a statement is true in every possible model of a theory, then it can be proven, the incompleteness theorems show that there will always be true statements in mathematics that cannot be proven within the same system. This means that even if a theory seems complete, there will always be some questions it cannot answer.

Relationship to the compactness theorem

The completeness theorem and the compactness theorem are very important ideas in first-order logic. The compactness theorem states that if a statement follows from a large set of statements, it also follows from just a few of them. This idea comes directly from the completeness theorem.

We can also use the compactness theorem to prove the completeness theorem in many systems. These two theorems are closely connected and, for certain types of languages, they are equivalent to a basic idea in mathematics called weak Kőnig's lemma.

Completeness in other logics

The completeness theorem is special to first-order logic and doesn't apply to every type of logic. For example, second-order logic doesn’t have a completeness theorem when looking at its standard meanings, although it does work with a different idea called Henkin semantics.

There are also completeness theorems for other kinds of logic, like modal logic and intuitionistic logic, when we use certain ways of understanding them, such as Kripke semantics.

Proofs

Gödel's original proof of the theorem was a unique way of solving a specific problem. Today, many books use Henkin's proof instead. Henkin's proof has three main steps: adding special constants to the theory, using Lindenbaum's lemma to expand it, and building a model from it.

In 2004, James Margetson created a computer proof using the Isabelle theorem prover, and there are other known proofs as well.