Notation

In the following context of mathematical logic, the turnstile symbol ${\displaystyle \vdash }$ means "provable from". That is, ${\displaystyle a\vdash b}$ reads: b is provable from a (in some specified formal system).

Definition

• A set of formulas ${\displaystyle \Phi }$ in first-order logic is consistent (written ${\displaystyle \operatorname {Con} \Phi }$) if there is no formula ${\displaystyle \varphi }$ such that ${\displaystyle \Phi \vdash \varphi }$ and ${\displaystyle \Phi \vdash \lnot \varphi }$. Otherwise ${\displaystyle \Phi }$ is inconsistent (written ${\displaystyle \operatorname {Inc} \Phi }$).
• ${\displaystyle \Phi }$ is said to be simply consistent if for no formula ${\displaystyle \varphi }$ of ${\displaystyle \Phi }$, both ${\displaystyle \varphi }$ and the negation of ${\displaystyle \varphi }$ are theorems of ${\displaystyle \Phi }$.
• ${\displaystyle \Phi }$ is said to be absolutely consistent or Post consistent if at least one formula in the language of ${\displaystyle \Phi }$ is not a theorem of ${\displaystyle \Phi }$.
• ${\displaystyle \Phi }$ is said to be maximally consistent if ${\displaystyle \Phi }$ is consistent and for every formula ${\displaystyle \varphi }$, ${\displaystyle \operatorname {Con} (\Phi \cup \{\varphi \})}$ implies ${\displaystyle \varphi \in \Phi }$.
• ${\displaystyle \Phi }$ is said to contain witnesses if for every formula of the form ${\displaystyle \exists x\,\varphi }$ there exists a term ${\displaystyle t}$ such that ${\displaystyle (\exists x\,\varphi \to \varphi {t \over x})\in \Phi }$, where ${\displaystyle \varphi {t \over x}}$ denotes the substitution of each ${\displaystyle x}$ in ${\displaystyle \varphi }$ by a ${\displaystyle t}$; see also First-order logic.

Basic results

1. The following are equivalent:
   1. ${\displaystyle \operatorname {Inc} \Phi }$
   2. For all ${\displaystyle \varphi ,\;\Phi \vdash \varphi .}$
2. Every satisfiable set of formulas is consistent, where a set of formulas ${\displaystyle \Phi }$ is satisfiable if and only if there exists a model ${\displaystyle {\mathfrak {I}}}$ such that ${\displaystyle {\mathfrak {I}}\vDash \Phi }$.
3. For all ${\displaystyle \Phi }$ and ${\displaystyle \varphi }$:
   1. if not ${\displaystyle \Phi \vdash \varphi }$, then ${\displaystyle \operatorname {Con} \left(\Phi \cup \{\lnot \varphi \}\right)}$;
   2. if ${\displaystyle \operatorname {Con} \Phi }$ and ${\displaystyle \Phi \vdash \varphi }$, then ${\displaystyle \operatorname {Con} \left(\Phi \cup \{\varphi \}\right)}$;
   3. if ${\displaystyle \operatorname {Con} \Phi }$, then ${\displaystyle \operatorname {Con} \left(\Phi \cup \{\varphi \}\right)}$ or ${\displaystyle \operatorname {Con} \left(\Phi \cup \{\lnot \varphi \}\right)}$.
4. Let ${\displaystyle \Phi }$ be a maximally consistent set of formulas and suppose it contains witnesses. For all ${\displaystyle \varphi }$ and ${\displaystyle \psi }$:
   1. if ${\displaystyle \Phi \vdash \varphi }$, then ${\displaystyle \varphi \in \Phi }$,
   2. either ${\displaystyle \varphi \in \Phi }$ or ${\displaystyle \lnot \varphi \in \Phi }$,
   3. ${\displaystyle (\varphi \lor \psi )\in \Phi }$ if and only if ${\displaystyle \varphi \in \Phi }$ or ${\displaystyle \psi \in \Phi }$,
   4. if ${\displaystyle (\varphi \to \psi )\in \Phi }$ and ${\displaystyle \varphi \in \Phi }$, then ${\displaystyle \psi \in \Phi }$,
   5. ${\displaystyle \exists x\,\varphi \in \Phi }$ if and only if there is a term ${\displaystyle t}$ such that ${\displaystyle \varphi {t \over x}\in \Phi }$.

Henkin's theorem

Let ${\displaystyle S}$ be a set of symbols. Let ${\displaystyle \Phi }$ be a maximally consistent set of ${\displaystyle S}$-formulas containing witnesses.

Define an equivalence relation ${\displaystyle \sim }$ on the set of ${\displaystyle S}$-terms by ${\displaystyle t_{0}\sim t_{1}}$ if ${\displaystyle \;t_{0}\equiv t_{1}\in \Phi }$, where ${\displaystyle \equiv }$ denotes equality. Let ${\displaystyle {\overline {t}}}$ denote the equivalence class of terms containing ${\displaystyle t}$; and let ${\displaystyle T_{\Phi }:=\{\;{\overline {t}}\mid t\in T^{S}\}}$ where ${\displaystyle T^{S}}$ is the set of terms based on the set of symbols ${\displaystyle S}$.

Define the ${\displaystyle S}$-structure ${\displaystyle {\mathfrak {T}}_{\Phi }}$ over ${\displaystyle T_{\Phi }}$, also called the term-structure corresponding to ${\displaystyle \Phi }$, by:

1. for each ${\displaystyle n}$-ary relation symbol ${\displaystyle R\in S}$, define ${\displaystyle R^{{\mathfrak {T}}_{\Phi }}{\overline {t_{0}}}\ldots {\overline {t_{n-1}}}}$ if ${\displaystyle \;Rt_{0}\ldots t_{n-1}\in \Phi$ ;} ^[8]
2. for each ${\displaystyle n}$-ary function symbol ${\displaystyle f\in S}$, define ${\displaystyle f^{{\mathfrak {T}}_{\Phi }}({\overline {t_{0}}}\ldots {\overline {t_{n-1}}}):={\overline {ft_{0}\ldots t_{n-1}}};}$
3. for each constant symbol ${\displaystyle c\in S}$, define ${\displaystyle c^{{\mathfrak {T}}_{\Phi }}:={\overline {c}}.}$

Define a variable assignment ${\displaystyle \beta _{\Phi }}$ by ${\displaystyle \beta _{\Phi }(x):={\bar {x}}}$ for each variable ${\displaystyle x}$. Let ${\displaystyle {\mathfrak {I}}_{\Phi }:=({\mathfrak {T}}_{\Phi },\beta _{\Phi })}$ be the term interpretation associated with ${\displaystyle \Phi }$.

Then for each ${\displaystyle S}$-formula ${\displaystyle \varphi }$:

${\displaystyle {\mathfrak {I}}_{\Phi }\vDash \varphi }$ if and only if ${\displaystyle \;\varphi \in \Phi .}$

Sketch of proof

There are several things to verify. First, that ${\displaystyle \sim }$ is in fact an equivalence relation. Then, it needs to be verified that (1), (2), and (3) are well defined. This falls out of the fact that ${\displaystyle \sim }$ is an equivalence relation and also requires a proof that (1) and (2) are independent of the choice of ${\displaystyle t_{0},\ldots ,t_{n-1}}$ class representatives. Finally, ${\displaystyle {\mathfrak {I}}_{\Phi }\vDash \varphi }$ can be verified by induction on formulas.