Syntax, Truth, and Completeness

A formula can follow from assumptions in two different senses. There may be a derivation of it according to specified rules. Alternatively, it may be true in every interpretation in which the assumptions are true. The first relation concerns proofs; the second concerns models.

Their distinction became one of the organizing ideas of modern logic. It made possible exact questions about whether a calculus proves too much, too little, or precisely what its semantics requires.

The previous note examined a constructive interpretation of assertion. This note develops the classical first-order setting. The presentation follows a useful explanatory order; historically, the concepts emerged through overlapping work rather than through this finished sequence of definitions.

Syntax specifies the expressions

A first-order language begins with logical symbols and a signature of nonlogical symbols. The signature may contain constants, function symbols, and relation symbols, each with a specified number of arguments.

For arithmetic, a signature might contain

Terms are built recursively from variables, constants, and function application. Atomic formulas compare terms by equality or apply relation symbols. Connectives and quantifiers then form more complicated formulas.

For example,

is a sentence because it has no free variables. The expression $x<y$, considered alone, has free variables.

The syntax determines whether an expression is well formed. It does not determine whether the expression is true. A relation symbol such as $<$ need not yet denote the familiar order on numbers.

A theory supplies a collection of sentences in the language. The group axioms and Peano arithmetic are theories; first-order logic is the logical framework in which such theories may be written.

Semantics supplies an interpretation

A structure $\mathcal M$ provides a nonempty domain and an interpretation of each nonlogical symbol. An assignment $s$ gives values to free variables.

The satisfaction relation

is defined recursively. Conjunction is satisfied when both conjuncts are satisfied. An existential formula is satisfied when some domain element supplies an appropriate value for its variable:

For a sentence, the choice of assignment does not affect truth, so we write $\mathcal M\models\varphi$.

The sentence $\forall x\exists y(x<y)$ is true in the natural numbers with their usual order. It is false in the two-element ordered structure $0<1$, because the largest element has no greater element.

The same syntax therefore receives different truth values in different structures. An axiom restricts the permitted structures by requiring its interpretation to be true.

Tarski and the levels of a truth definition

Alfred Tarski's work in the 1930s supplied a systematic account of truth for formalized languages. A definition is given in a metalanguage capable of describing the object language and the relevant mathematical structures.

The familiar form

illustrates the distinction between naming a sentence and using a sentence to state its truth condition. For a formal language, the substantial work is to define satisfaction recursively and show that the resulting definition has the required adequacy properties.

The metalanguage is doing real work. It may quantify over assignments, domain elements, and formulas, using background mathematical resources. A truth definition for one formal language does not automatically provide an unrestricted truth predicate within that same language.

Tarski's truth-definition project should also be distinguished from the separate 1936 treatment of logical consequence and from later textbook presentations that combine these developments into one familiar definition.

Derivation and consequence

Write

when a formal derivation of $\varphi$ from assumptions in $\Gamma$ exists. Write

when every structure satisfying all of $\Gamma$ satisfies $\varphi$.

A calculus is sound if

It is semantically complete if the converse holds.

Soundness is usually proved by induction on a derivation: the axioms are valid and each inference rule preserves truth under the relevant assumptions. Completeness requires a more substantial argument. If no proof of $\varphi$ exists, one must construct or otherwise establish a model of the assumptions in which $\varphi$ fails.

These properties concern a relationship between a calculus and a semantics. A theory is called complete in another sense if, for every sentence $\varphi$ in its language, it proves either $\varphi$ or $\neg\varphi$. That property is not implied by semantic completeness of first-order logic.

Gödel's completeness theorem

Gödel proved completeness for first-order logic in his 1929 dissertation, publishing a revised account in 1930. It connected the formal proof methods with semantic validity.

In the standard general formulation,

The theorem does not supply a procedure that always decides whether a given formula is valid. It establishes that a proof exists whenever validity holds. Systematic proof enumeration will eventually find such a proof, but may continue indefinitely when the formula is not valid.

The distinction between existence of a proof and a terminating decision procedure is essential. It is one reason completeness can coexist with Church's later undecidability theorem.

The propositional case had its own history. Truth-functional methods were developed through several traditions, and work by Post and Wittgenstein in the early 1920s contributed to the familiar systematic treatment of truth tables. Quantifiers introduced a further difficulty: arbitrary domains cannot generally be handled by checking one finite table of assignments.

Henkin's construction: making a model from syntax

Leon Henkin's 1949 proof gave an influential way to establish completeness. The following sketch assumes a countable language and a consistent set of sentences.

First, expand the language with witness constants. For an existential sentence $\exists x\,A(x)$, arrange that the theory contains a sentence of the form

where $c$ is a suitably fresh constant. The construction must be organized so that adding these witnesses preserves consistency.

Next, extend the theory to a maximally consistent collection $\Delta$: for every sentence $B$, choose $B$ or $\neg B$ in a way that preserves consistency. Countability permits the choices to be organized along an enumeration.

Build a structure whose elements are closed terms, identifying terms $t$ and $u$ when $t=u$ belongs to $\Delta$. Interpret function symbols by forming the corresponding terms. Interpret relation symbols by membership of their atomic instances in $\Delta$.

The central truth lemma states, with the appropriate treatment of assignments,

The witness constants handle the existential step of the induction. If an existential statement belongs to $\Delta$, a named witness has been supplied. Conversely, a witness instance yields the existential statement.

To prove completeness, suppose $\Gamma\not\vdash\varphi$. Classical proof rules imply that $\Gamma\cup\{\neg\varphi\}$ is consistent. The construction gives a model of that set, so $\Gamma\not\models\varphi$.

This proof explains the mechanism behind the theorem. Consistency can be used to assemble an interpretation, rather than merely being announced as the absence of contradiction.

Compactness and nonstandard arithmetic

First-order proofs are finite. Together with completeness, this yields compactness:

If every finite subset of a set of sentences has a model, the entire set has a model.

If the entire set were inconsistent, a finite proof of contradiction would use only finitely many of its assumptions. That finite subset would have no model by soundness.

Let $\operatorname{Th}(\mathbb N)$ be the set of all first-order sentences true in the standard natural numbers. Expand the language by a constant $c$, and add

Every finite subset is satisfiable in $\mathbb N$: interpret $c$ as a number larger than the finitely many named bounds. Compactness gives a model of the whole collection.

In that model, the interpretation of $c$ exceeds every standard numeral. The model satisfies all first-order truths of $\mathbb N$, yet it is not isomorphic to $\mathbb N$.

Nothing here supplies a multiplicative inverse for $c$. The construction concerns arithmetic. An infinitesimal obtained as the reciprocal of a positive infinite element requires an appropriate ordered-field setting, which is discussed in the model-theory note.

Löwenheim–Skolem and the size of models

Löwenheim's 1915 work and Skolem's subsequent refinements investigated the relationship between first-order descriptions and cardinality. In a countable language, a theory with an infinite model has a countable model. The upward theorem also supplies models of larger infinite cardinalities under its standard hypotheses.

These results prevent a first-order theory with infinite models from determining one model up to isomorphism across all cardinalities. They do not prevent a theory from being categorical within one cardinality. The theory of dense linear orders without endpoints, for example, has exactly one countable model up to isomorphism.

Skolem's discussion of countable models of set theory raised an apparent paradox: such a model may satisfy a sentence asserting that a set is uncountable. The resolution is that the model's assertion concerns the absence of a bijection inside that model. An external enumeration of its elements need not be an object available within it.

The internal and external viewpoints must therefore be kept distinct. The theorem does not show that a formal model contains a contradiction about cardinality.

Stronger languages and different tradeoffs

Under full second-order semantics, quantifiers over predicates range over all the appropriate subsets or relations on the domain. Second-order arithmetic with full induction characterizes the natural-number structure up to isomorphism.

That expressiveness comes with a different collection of metatheorems. Full second-order validity has no sound, complete, effective proof calculus, and the familiar compactness and Löwenheim–Skolem properties fail.

Henkin semantics allows a specified collection of predicates or functions rather than requiring all of them. Appropriate higher-order calculi can be complete for that semantics. The same-looking formal language can therefore participate in different foundational settings depending on its interpretation.

Lindström's 1969 theorem gives a precise maximality result for first-order logic within an appropriate class of abstract logics satisfying closure conditions, compactness, and a downward Löwenheim–Skolem property. It is not simply a theorem that effective enumeration of consequences forces every feature of first-order logic.

The available choices are thus substantial: expressive power, semantic commitments, categoricity, and proof-theoretic properties must be considered together.

From complete logic to incomplete arithmetic

Semantic completeness says that all consequences true in every model of a theory have proofs. It does not say that the axioms settle every sentence, or that they uniquely specify the intended infinite structure.

Gödel's next result exploited the capacity of arithmetic to express facts about formal derivations. The next note explains how that capacity produces undecidable sentences, and why there is no conflict with the completeness theorem established here.

Sources and further reading

• Leopold Löwenheim, “Über Möglichkeiten im Relativkalkül” (1915), and Thoralf Skolem's papers of 1920 and 1922.
• Kurt Gödel, “Die Vollständigkeit der Axiome des logischen Funktionenkalküls” (1930), following his 1929 dissertation.
• Alfred Tarski, The Concept of Truth in Formalized Languages (Polish publication 1933; expanded German publication 1935), and “On the Concept of Logical Consequence” (1936).
• Leon Henkin, “The Completeness of the First-Order Functional Calculus” (1949), and “Completeness in the Theory of Types” (1950).
• Per Lindström, “On Extensions of Elementary Logic” (1969).
• Tarski's Truth Definitions and Generalized Quantifiers, for historical and semantic qualifications.