Model Theory - First-order Logic

First-order Logic

Whereas universal algebra provides the semantics for a signature, logic provides the syntax. With terms, identities and quasi-identities, even universal algebra has some limited syntactic tools; first-order logic is the result of making quantification explicit and adding negation into the picture.

A first-order formula is built out of atomic formulas such as R(f(x,y),z) or y = x + 1 by means of the Boolean connectives and prefixing of quantifiers or . A sentence is a formula in which each occurrence of a variable is in the scope of a corresponding quantifier. Examples for formulas are φ (or φ(x) to mark the fact that at most x is an unbound variable in φ) and ψ defined as follows:

(Note that the equality symbol has a double meaning here.) It is intuitively clear how to translate such formulas into mathematical meaning. In the σ_smr-structure of the natural numbers, for example, an element n satisfies the formula φ if and only if n is a prime number. The formula ψ similarly defines irreducibility. Tarski gave a rigorous definition, sometimes called "Tarski's definition of truth", for the satisfaction relation, so that one easily proves:

is a prime number.

is irreducible.

A set T of sentences is called a (first-order) theory. A theory is satisfiable if it has a model, i.e. a structure (of the appropriate signature) which satisfies all the sentences in the set T. Consistency of a theory is usually defined in a syntactical way, but in first-order logic by the completeness theorem there is no need to distinguish between satisfiability and consistency. Therefore model theorists often use "consistent" as a synonym for "satisfiable".

A theory is called categorical if it determines a structure up to isomorphism, but it turns out that this definition is not useful, due to serious restrictions in the expressivity of first-order logic. The Löwenheim–Skolem theorem implies that for every theory T which has an infinite model and for every infinite cardinal number κ, there is a model such that the number of elements of is exactly κ. Therefore only finite structures can be described by a categorical theory.

Lack of expressivity (when compared to higher logics such as second-order logic) has its advantages, though. For model theorists, the Löwenheim–Skolem theorem is an important practical tool rather than the source of Skolem's paradox. In a certain sense made precise by Lindström's theorem, first-order logic is the most expressive logic for which both the Löwenheim–Skolem theorem and the compactness theorem hold.

Due to Gödel, the compactness theorem says that every unsatisfiable first-order theory has a finite unsatisfiable subset. This theorem is of central importance in infinite model theory, where the words "by compactness" are commonplace. One way to prove it is by means of ultraproducts. An alternative proof uses the completeness theorem, which is otherwise reduced to a marginal role in most of modern model theory.