LARA

First-Order Theories

(Building on First-Order Logic Semantics.)

Definition: A first-order theory is a set $T$ of first-order logic sentences.

Definition: A theory $T$ is consistent if it is satisfiable.

Definition: A theory $T$ is complete if for every closed first-order formula $F$, either $T \models F$ or $T \models \lnot F$.

We have two main ways of defining theories: by taking a specific set of structures and looking at sentences true in these structures, or by looking at a set of axioms and looking at their consequences.

Definition: If ${\cal I}$ is a set of interpretations, then the theory of ${\cal I}$ is the set of formulas that are true in all interepretations from ${\cal I}$, that is $Th({\cal I}) = \{ F \mid \forall I \in {\cal I}. e_F(F)(I)\}$.

Note that $F \in Th(\{I\})$ is equivalent to $e_F(F)(I)$.

Lemma: For any interpretation $I$, the theory $Th(\{I\})$ is complete.

Definition (axiomatization of a theory): We say that $T_1$ is an axiomatization of $T_2$ iff $Conseq(T_1) = Conseq(T_2)$. Axiomatization $T_1$ is finite if $T_1$ is a finite set. Axiomatization $T_1$ is recursive if it is a recursive set.

Example: Theory of Partial Orders

Consider the language ${\cal L} = \{ \le \}$ where $\le$ is a binary relation. Consider the following three sentences:

\begin{equation*}\begin{array}{rcl} Ref & \equiv & \forall x. x \le x \\ Sym & \equiv & \forall x.\ x \le y \land y \le x \rightarrow x=y \\ Tra & \equiv & \forall x. \forall y.\ \forall z. x \le y \land y \le z \rightarrow x \le z \end{array} \end{equation*}

Let $T = Conseq(\{Ref,Sym,Tra\})$. Let us answer the following:

  • Is $T$ consistent?
  • Is $T$ complete?