• English only

# Differences

This shows you the differences between two versions of the page.

sav08:first-order_theories [2008/04/15 13:45]
vkuncak
sav08:first-order_theories [2015/04/21 17:30] (current)
Line 3: Line 3:
(Building on [[First-Order Logic Semantics]].) (Building on [[First-Order Logic Semantics]].)

-**Definition:​** A //​first-order theory// is a set $T$ of [[First-Order Logic Syntax|first-order logic formulas]].+**Definition:​** A //​first-order theory// is a set $T$ of [[First-Order Logic Syntax|first-order logic sentences]].

**Definition:​** A theory $T$ is //​consistent//​ if it is satisfiable. **Definition:​** A theory $T$ is //​consistent//​ if it is satisfiable.
Line 22: Line 22:

Consider the language ${\cal L} = \{ \le \}$ where $\le$ is a binary relation. ​ Consider the following three sentences: Consider the language ${\cal L} = \{ \le \}$ where $\le$ is a binary relation. ​ Consider the following three sentences:
-$\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl} Ref & \equiv & \forall x. x \le x \\ Ref & \equiv & \forall x. x \le x \\ Sym & \equiv & \forall x.\ x \le y \land y \le x \rightarrow x=y \\ 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 Tra & \equiv & \forall x. \forall y.\ \forall z. x \le y \land y \le z \rightarrow x \le z \end{array} \end{array} -$+\end{equation*}
Let $T = Conseq(\{Ref,​Sym,​Tra\})$. ​ Let us answer the following: Let $T = Conseq(\{Ref,​Sym,​Tra\})$. ​ Let us answer the following:
* Is $T$ ++consistent?​|Yes,​ take, for example, ordering on integers.++   * Is $T$ ++consistent?​|Yes,​ take, for example, ordering on integers.++
* Is $T$ ++complete?​|No,​ take, for example, $\exists x. \forall y. x \le y$. It is true with the ordering on $\mathbb{N}$,​ but false with the ordering on $\mathbb{Z}$.++   * Is $T$ ++complete?​|No,​ take, for example, $\exists x. \forall y. x \le y$. It is true with the ordering on $\mathbb{N}$,​ but false with the ordering on $\mathbb{Z}$.++