Inmathematical logic, atheory (also called aformal theory) is a set ofsentences in aformal language. In most scenarios adeductive system is first understood from context, giving rise to aformal system that combines the language with deduction rules. An element${\displaystyle \varphi \in T}$ of adeductively closed theory${\displaystyle T}$ is then called atheorem of the theory. In many deductive systems there is usually a subset${\displaystyle \mathrm{\Sigma }\subseteq T}$ that is called "the set ofaxioms" of the theory${\displaystyle T}$, in which case the deductive system is also called an "axiomatic system". By definition, every axiom is automatically a theorem. Afirst-order theory is a set offirst-order sentences (theorems)recursively obtained by theinference rules of the system applied to the set of axioms.

When defining theories for foundational purposes, additional care must be taken, as normal set-theoretic language may not be appropriate.

The construction of a theory begins by specifying a definite non-emptyconceptual class${\displaystyle \mathcal{E}}$, the elements of which are calledstatements. These initial statements are often called theprimitive elements orelementary statements of the theory—to distinguish them from other statements that may be derived from them.

A theory${\displaystyle \mathcal{T}}$ is a conceptual class consisting of certain of these elementary statements. The elementary statements that belong to${\displaystyle \mathcal{T}}$ are called theelementary theorems of${\displaystyle \mathcal{T}}$ and are said to betrue. In this way, a theory can be seen as a way of designating a subset of${\displaystyle \mathcal{E}}$ that only contain statements that are true.

This general way of designating a theory stipulates that the truth of any of its elementary statements is not known without reference to${\displaystyle \mathcal{T}}$. Thus the same elementary statement may be true with respect to one theory but false with respect to another. This is reminiscent of the case in ordinary language where statements such as "He is an honest person" cannot be judged true or false without interpreting who "he" is, and, for that matter, what an "honest person" is under this theory.^[1]

A theory${\displaystyle \mathcal{S}}$ is asubtheory 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 anextension or asupertheory of${\displaystyle \mathcal{T}}$

A theory is said to be adeductive theory if${\displaystyle \mathcal{T}}$ is aninductive class, which is to say that its content is based on someformal deductive system and that some of its elementary statements are taken asaxioms. In a deductive theory, any sentence that is alogical consequence of one or more of the axioms is also a sentence of that theory.^[1] More formally, if${\displaystyle ⊢}$ is a Tarski-styleconsequence relation, then${\displaystyle \mathcal{T}}$ is closed under${\displaystyle ⊢}$ (and so each of its theorems is a logical consequence of its axioms) if and only if, for all sentences${\displaystyle \varphi }$ in the language of the theory${\displaystyle \mathcal{T}}$, if${\displaystyle \mathcal{T}⊢\varphi }$, then${\displaystyle \varphi \in \mathcal{T}}$; or, equivalently, if${\displaystyle {\mathcal{T}}^{\prime }}$ 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}}^{\prime }⊢\varphi }$, then${\displaystyle \varphi \in {\mathcal{T}}^{\prime }}$, and therefore${\displaystyle \varphi \in \mathcal{T}}$.

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

Asatisfiable theory is a theory that has amodel. This means there is a structureM thatsatisfies 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 φ.

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

Acomplete consistent theory (or just acomplete theory) is aconsistent 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] Anincomplete theory is a consistent theory that is not complete.

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

Aninterpretation of a theory is the relationship between a theory and some subject matter when there is amany-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 afull interpretation, otherwise it is called apartial interpretation.^[4]

Eachstructure has several associated theories. Thecomplete theory of a structureA is the set of allfirst-ordersentences over thesignature ofA that are satisfied byA. It is denoted by Th(A). More generally, thetheory ofK, a class of σ-structures, is the set of all first-orderσ-sentences that are satisfied by all structures inK, and is denoted by Th(K). Clearly Th(A) = Th({A}). These notions can also be defined with respect to other logics.

For each σ-structureA, there are several associated theories in a larger signature σ' that extends σ by adding one new constant symbol for each element of the domain ofA. (If the new constant symbols are identified with the elements ofA 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 ofA.^{[further explanation needed]}

Thediagram ofA consists of all atomic or negated atomic σ'-sentences that are satisfied byA and is denoted by diag_A. Thepositive diagram ofA is the set of all atomic σ'-sentences thatA satisfies. It is denoted by diag⁺_A. Theelementary diagram ofA is the set eldiag_A ofall first-order σ'-sentences that are satisfied byA or, equivalently, the complete (first-order) theory of the naturalexpansion ofA to the signature σ'.

A first-order theory${\displaystyle \mathcal{Q}\mathcal{S}}$ is a set of sentences in a first-orderformal language${\displaystyle \mathcal{Q}}$.

There are many formal derivation ("proof") systems for first-order logic. These includeHilbert-style deductive systems,natural deduction, thesequent calculus, thetableaux method andresolution.

AformulaA is asyntactic consequence of a first-order theory${\displaystyle \mathcal{Q}\mathcal{S}}$ if there is aderivation ofA using only formulas in${\displaystyle \mathcal{Q}\mathcal{S}}$ as non-logical axioms. Such a formulaA is also called a theorem of${\displaystyle \mathcal{Q}\mathcal{S}}$. The notation "${\displaystyle \mathcal{Q}\mathcal{S}⊢A}$" indicatesA is a theorem of${\displaystyle \mathcal{Q}\mathcal{S}}$.

Aninterpretation 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. Amodel of a first-order theory${\displaystyle \mathcal{Q}\mathcal{S}}$ is an interpretation in which every formula of${\displaystyle \mathcal{Q}\mathcal{S}}$ is satisfied.

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

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

One way to specify a theory is to define a set ofaxioms in a particular language. The theory can be taken to include just those axioms, or their logical or provable consequences, as desired. Theories obtained this way includeZFC andPeano arithmetic.

A second way to specify a theory is to begin with astructure, and let the theory be the set of sentences that are satisfied by the structure. This is a method for producing complete theories through the semantic route, with examples including the set of true sentences under the structure (N, +, ×, 0, 1, =), whereN is the set of natural numbers, and the set of true sentences under the structure (R, +, ×, 0, 1, =), whereR is the set of real numbers. The first of these, called the theory oftrue arithmetic, cannot be written as the set of logical consequences of anyenumerable set of axioms.The theory of (R, +, ×, 0, 1, =) was shown by Tarski to bedecidable; it is the theory ofreal closed fields (seeDecidability of first-order theories of the real numbers for more).

• Axiomatic system
• Interpretability
• List of first-order theories
• Mathematical theory

• Hodges, Wilfrid (1997).A shorter model theory.Cambridge University Press.ISBN 0-521-58713-1.

• Formal theories
• Logical expressions

• Articles with short description
• Short description matches Wikidata
• Wikipedia articles needing clarification from June 2021