# 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) Both sides previous revision Previous revision 2008/04/15 13:46 vkuncak 2008/04/15 13:45 vkuncak 2008/03/19 22:02 damien 2008/03/19 15:13 vkuncak 2008/03/19 15:13 vkuncak created Next revision Previous revision 2008/04/15 13:46 vkuncak 2008/04/15 13:45 vkuncak 2008/03/19 22:02 damien 2008/03/19 15:13 vkuncak 2008/03/19 15:13 vkuncak created 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}$.++