Theory (mathematical logic)

A theory ${\displaystyle {\mathcal {S}}}$ is a subtheory of a theory ${\displaystyle {\mathcal {T}}}$ if ${\displaystyle {\mathcal {S}}}$ is a subset of ${\displaystyle {\mathcal {T}}}$. If ${\displaystyle {\mathcal {T}}}$ is a subset of ${\displaystyle {\mathcal {S}}}$ then ${\displaystyle {\mathcal {S}}}$ is called an extension or a supertheory of ${\displaystyle {\mathcal {T}}}$

A theory is said to be a deductive theory if ${\displaystyle {\mathcal {T}}}$ is an inductive class, which is to say that its content is based on some formal deductive system and that some of its elementary statements are taken as axioms. In a deductive theory, any sentence that is a logical consequence of one or more of the axioms is also a sentence of that theory.[1] More formally, if ${\displaystyle \vdash }$ is a Tarski-style consequence relation, then ${\displaystyle {\mathcal {T}}}$ is closed under ${\displaystyle \vdash }$ (and so each of its theorems is a logical consequence of its axioms) if and only if, for all sentences ${\displaystyle \phi }$ in the language of the theory ${\displaystyle {\mathcal {T}}}$, if ${\displaystyle {\mathcal {T}}\vdash \phi }$, then ${\displaystyle \phi \in {\mathcal {T}}}$; or, equivalently, if ${\displaystyle {\mathcal {T}}'}$ is a finite subset of ${\displaystyle {\mathcal {T}}}$ (possibly the set of axioms of ${\displaystyle {\mathcal {T}}}$ in the case of finitely axiomatizable theories) and ${\displaystyle {\mathcal {T}}'\vdash \phi }$, then ${\displaystyle \phi \in {\mathcal {T}}'}$, and therefore ${\displaystyle \phi \in {\mathcal {T}}}$.

A syntactically consistent theory is a theory from which not every sentence in the underlying language can be proven (with respect to some deductive system, which is usually clear from context). In a deductive system (such as first-order logic) that satisfies the principle of explosion, this is equivalent to requiring that there is no sentence φ such that both φ and its negation can be proven from the theory.

A satisfiable theory is a theory that has a model. This means there is a structure M that satisfies every sentence in the theory. Any satisfiable theory is syntactically consistent, because the structure satisfying the theory will satisfy exactly one of φ and the negation of φ, for each sentence φ.

A consistent theory is sometimes defined to be a syntactically consistent theory, and sometimes defined to be a satisfiable theory. For first-order logic, the most important case, it follows from the completeness theorem that the two meanings coincide.[2] In other logics, such as second-order logic, there are syntactically consistent theories that are not satisfiable, such as ω-inconsistent theories.

A complete consistent theory (or just a complete theory) is a consistent theory ${\displaystyle {\mathcal {T}}}$ such that for every sentence φ in its language, either φ is provable from ${\displaystyle {\mathcal {T}}}$ or ${\displaystyle {\mathcal {T}}}$ ${\displaystyle \cup }$ {φ} is inconsistent. For theories closed under logical consequence, this means that for every sentence φ, either φ or its negation is contained in the theory.[3] An incomplete theory is a consistent theory that is not complete.

(see also ω-consistent theory for a stronger notion of consistency.)

An interpretation of a theory is the relationship between a theory and some subject matter when there is a many-to-one correspondence between certain elementary statements of the theory, and certain statements related to the subject matter. If every elementary statement in the theory has a correspondent it is called a full interpretation, otherwise it is called a partial interpretation.[4]

Each structure has several associated theories. The complete theory of a structure A is the set of all first-order sentences over the signature of A that are satisfied by A. It is denoted by Th(A). More generally, the theory of K, a class of σ-structures, is the set of all first-order σ-sentences that are satisfied by all structures in K, and is denoted by Th(K). Clearly Th(A) = Th({A}). These notions can also be defined with respect to other logics.

For each σ-structure A, there are several associated theories in a larger signature σ' that extends σ by adding one new constant symbol for each element of the domain of A. (If the new constant symbols are identified with the elements of A that they represent, σ' can be taken to be σ ${\displaystyle \cup }$ A.) The cardinality of σ' is thus the larger of the cardinality of σ and the cardinality of A.

The diagram of A consists of all atomic or negated atomic σ'-sentences that are satisfied by A and is denoted by diag_A. The positive diagram of A is the set of all atomic σ'-sentences that A satisfies. It is denoted by diag⁺_A. The elementary diagram of A is the set eldiag_A of all first-order σ'-sentences that are satisfied by A or, equivalently, the complete (first-order) theory of the natural expansion of A to the signature σ'.

There are many formal derivation ("proof") systems for first-order logic. These include Hilbert-style deductive systems, natural deduction, the sequent calculus, the tableaux method and resolution.

A formula A is a syntactic consequence of a first-order theory ${\displaystyle {\mathcal {QS}}}$ if there is a derivation of A using only formulas in ${\displaystyle {\mathcal {QS}}}$ as non-logical axioms. Such a formula A is also called a theorem of ${\displaystyle {\mathcal {QS}}}$. The notation "${\displaystyle {\mathcal {QS}}\vdash A}$" indicates A is a theorem of ${\displaystyle {\mathcal {QS}}}$.

An interpretation of a first-order theory provides a semantics for the formulas of the theory. An interpretation is said to satisfy a formula if the formula is true according to the interpretation. A model of a first-order theory ${\displaystyle {\mathcal {QS}}}$ is an interpretation in which every formula of ${\displaystyle {\mathcal {QS}}}$ is satisfied.

A first-order theory ${\displaystyle {\mathcal {QS}}}$ is a first-order theory with identity if ${\displaystyle {\mathcal {QS}}}$ includes the identity relation symbol "=" and the reflexivity and substitution axiom schemes for this symbol.

• Compactness theorem
• Consistent set
• Deduction theorem
• Enumeration theorem
• Lindenbaum's lemma
• Löwenheim–Skolem theorem