LARA

Differences

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

Link to this comparison view

sav08:first-order_theories [2008/04/15 13:45]
vkuncak
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|first-order logic formulas]]. 
- 
-**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{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}$.++