Differences
This shows you the differences between two versions of the page.
sav08:first-order_theories [2008/03/19 22:02] damien |
sav08:first-order_theories [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== First-Order Theories ====== | ||
- | (Building on [[First-Order Logic Semantics]].) | ||
- | |||
- | **Definition:** A //first-order theory// is a set $T$ of [[First-Order Logic Syntax|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 sentences that are true in all interepretations of ${\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{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} | ||
- | \] | ||
- | Let $T = Conseq(\{Ref,Sym,Tra\})$. Let us answer the following: | ||
- | * 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}$.++ |