Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
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}$.++ |