Editing Consistency (section)

== First-order logic ==

===Notation===
In the following context of [[mathematical logic]], the [[turnstile symbol]] <math>\vdash</math> means "provable from". That is, <math>a\vdash b</math> reads: ''b'' is provable from ''a'' (in some specified formal system).

===Definition===
*A set of [[Well-formed formula|formulas]] <math>\Phi</math> in first-order logic is '''consistent''' (written <math>\operatorname{Con} \Phi</math>) if there is no formula <math>\varphi</math> such that <math>\Phi \vdash \varphi</math> and <math>\Phi \vdash \lnot\varphi</math>.  Otherwise <math>\Phi</math> is '''inconsistent''' (written <math>\operatorname{Inc}\Phi</math>).
*<math>\Phi</math> is said to be '''simply consistent''' if for no formula <math>\varphi</math> of <math>\Phi</math>, both <math>\varphi</math> and the [[negation]] of <math>\varphi</math> are theorems of <math>\Phi</math>.{{clarify|reason=Assuming that 'provable from' and 'theorem of' is equivalent, there seems to be no difference between 'consistent' and 'simply consistent'. If that is true, both definitions should be joined into a single one. If not, the difference should be made clear.|date=September 2018}}
*<math>\Phi</math> is said to be '''absolutely consistent''' or '''Post consistent''' if at least one formula in the language of <math>\Phi</math> is not a theorem of <math>\Phi</math>.
*<math>\Phi</math> is said to be '''maximally consistent''' if <math>\Phi</math> is consistent and for every formula <math>\varphi</math>, <math>\operatorname{Con} (\Phi \cup \{\varphi\})</math> implies <math>\varphi \in \Phi</math>.
*<math>\Phi</math> is said to '''contain witnesses''' if for every formula of the form <math>\exists x \,\varphi</math> there exists a [[Term (logic)|term]] <math>t</math> such that <math>(\exists x \, \varphi \to \varphi {t \over x}) \in \Phi</math>, where <math>\varphi {t \over x}</math> denotes the [[substitution (logic)|substitution]] of each <math>x</math> in <math>\varphi</math> by a <math>t</math>; see also [[First-order logic]].{{citation needed|date=September 2018}}

===Basic results===
# The following are equivalent:
## <math>\operatorname{Inc}\Phi</math>
## For all <math>\varphi,\; \Phi \vdash \varphi.</math>
# Every satisfiable set of formulas is consistent, where a set of formulas <math>\Phi</math> is satisfiable if and only if there exists a model <math>\mathfrak{I}</math> such that <math>\mathfrak{I} \vDash \Phi </math>.
# For all <math>\Phi</math> and <math>\varphi</math>:
## if not <math> \Phi \vdash \varphi</math>, then <math>\operatorname{Con}\left( \Phi \cup \{\lnot\varphi\}\right)</math>;
## if <math>\operatorname{Con}\Phi</math> and <math>\Phi \vdash \varphi</math>, then <math> \operatorname{Con} \left(\Phi \cup \{\varphi\}\right)</math>;
## if <math>\operatorname{Con}\Phi</math>, then <math>\operatorname{Con}\left( \Phi \cup \{\varphi\}\right)</math> or <math>\operatorname{Con}\left( \Phi \cup \{\lnot \varphi\}\right)</math>.
# Let <math>\Phi</math> be a maximally consistent set of formulas and suppose it contains [[Witness (mathematics)|witnesses]].  For all <math>\varphi</math> and <math> \psi </math>:
## if <math> \Phi \vdash \varphi</math>, then <math>\varphi \in \Phi</math>,
## either <math>\varphi \in \Phi</math> or <math>\lnot \varphi \in \Phi</math>,
## <math>(\varphi \lor \psi) \in \Phi</math> if and only if <math>\varphi \in \Phi</math> or <math>\psi \in \Phi</math>,
## if <math>(\varphi\to\psi) \in \Phi</math> and <math>\varphi \in \Phi </math>, then <math>\psi \in \Phi</math>,
## <math>\exists x \, \varphi \in \Phi</math> if and only if there is a term <math>t</math> such that <math>\varphi{t \over x}\in\Phi</math>.{{citation needed|date=September 2018}}

===Henkin's theorem===
Let <math>S</math> be a [[signature (logic)|set of symbols]]. Let <math>\Phi</math> be a maximally consistent set of <math>S</math>-formulas containing [[Witness (mathematics)#Henkin witnesses|witnesses]].

Define an [[equivalence relation]] <math>\sim</math> on the set of <math>S</math>-terms by <math>t_0 \sim t_1</math> if <math>\; t_0 \equiv t_1 \in \Phi</math>, where <math>\equiv</math> denotes [[First-order logic#Equality and its axioms|equality]]. Let <math>\overline t</math> denote the [[equivalence class]] of terms containing <math>t </math>; and let <math>T_\Phi := \{ \; \overline t \mid t \in T^S \} </math> where <math>T^S </math> is the set of terms based on the set of symbols <math>S</math>.

Define the <math>S</math>-[[Structure (mathematical logic)|structure]] <math>\mathfrak T_\Phi </math> over <math> T_\Phi </math>, also called the '''term-structure''' corresponding to <math>\Phi</math>, by:

# for each <math>n</math>-ary relation symbol <math>R \in S</math>, define <math>R^{\mathfrak T_\Phi} \overline {t_0} \ldots \overline {t_{n-1}}</math> if <math>\; R t_0 \ldots t_{n-1} \in \Phi;</math><ref>This definition is independent of the choice of <math>t_i</math> due to the substitutivity properties of <math>\equiv</math> and the maximal consistency of <math>\Phi</math>.</ref>
# for each <math>n</math>-ary function symbol <math>f \in S</math>, define <math>f^{\mathfrak T_\Phi} (\overline {t_0} \ldots \overline {t_{n-1}}) := \overline {f t_0 \ldots t_{n-1}};</math>
# for each constant symbol <math>c \in S</math>, define <math>c^{\mathfrak T_\Phi}:= \overline c.</math>

Define a variable assignment <math>\beta_\Phi</math> by <math>\beta_\Phi (x) := \bar x</math> for each variable <math>x</math>. Let <math>\mathfrak I_\Phi := (\mathfrak T_\Phi,\beta_\Phi)</math> be the '''term [[Interpretation (logic)#First-order logic|interpretation]]''' associated with <math>\Phi</math>.

Then for each <math>S</math>-formula <math>\varphi</math>:

{{center|1=
<math>\mathfrak I_\Phi \vDash \varphi</math> if and only if <math> \; \varphi \in \Phi.</math>{{citation needed|date=September 2018}}
}}

===Sketch of proof===
There are several things to verify. First, that <math>\sim</math> 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 <math>\sim</math> is an equivalence relation and also requires a proof that (1) and (2) are independent of the choice of <math> t_0, \ldots ,t_{n-1} </math> class representatives.  Finally, <math> \mathfrak I_\Phi \vDash \varphi </math> can be verified by induction on formulas.