LARA

Differences

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

Link to this comparison view

sav08:first-order_logic_syntax [2008/03/19 10:24]
vkuncak
sav08:first-order_logic_syntax [2015/04/21 17:30]
Line 1: Line 1:
-====== First-Order Logic Syntax ====== 
- 
-(Compare to [[Propositional Logic Syntax]].) 
- 
-First order language ${\cal L}$ is a set of //relation symbols// $R$ and //function symbols// $f$, each of which comes with arity $ar(R)$, $ar(f)$, which are $\ge 0$.  Function symbols of arity 0 are constants. ​ Relation symbols of arity 0 are propositional variables.  ​ 
- 
-The set $V$ denotes countably infinite set of first-order variables, which is independent of the language. 
- 
-\[ 
-\begin{array}{rcl} 
-    F &::​=&​ A \mid \lnot F \mid (F \land F) \mid (F \lor F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ 
-      & \mid & \forall x.F \mid \exists x.F \\ 
-    A & ::= & R(T,​\ldots,​T) \mid (T = T) \\ 
-    T & ::= & V \mid f(T,​\ldots,​T)  ​ 
-\end{array} 
-\] 
- 
-Terminology summary: 
-  * $F$ - first-order logic formula (in language ${\cal L}$) 
-  * $A$ - atomic formula 
-  * $A, \lnot A$ - literals 
-  * $T$ - term 
-  * $f$ - function symbol 
-  * $R$ - relation symbol 
-  * $V$ - first-order variables 
- 
-Omitting parentheses:​ 
-  * $\land$, $\lor$ are associative 
-  * priorities, from strongest-binding:​ $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow,​ \leftrightarrow)\ ;\ (\forall, \exists)$ 
-When in doubt, use parentheses. 
- 
-Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$, $ar(Q) = 1$, $ar(R) = 2$, $ar(f) = 2$. Then 
-\[ 
-    \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x) 
-\] 
-denotes 
-\[ 
-    \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x))))) 
-\] 
- 
-Often we use infix notation for relation and function symbols. ​ In the example above, if we write $R$ and $f$ in infix notation, the formula becomes 
-\[ 
-    \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x) 
-\] 
- 
-Notation: when we write $F_1 \equiv F_2$ this means that $F_1$ and $F_2$ are identical formulas (with identical syntax trees). ​ For example, $p \land q \equiv p \land q$, but it is not the case that $p \land q \equiv q \land p$. 
- 
-In [[Isabelle theorem prover]] we use this ++++ASCII notation for First-Order Logic| 
-\[ 
-\begin{array}{c|c} ​ 
-\mbox{math} & \mbox{Isabelle} \\ \hline 
-\land & \verb!&​! \\ 
-\lor  & \verb!|! \\ 
-\lnot & \verb!~! \\ 
-\rightarrow & \verb!-->​! \\ 
-\leftrightarrow & \verb!=! \\ 
-{\it true} & \verb!True! \\ 
-{\it false} & \verb!False! \\ 
-\forall ​ & \verb!ALL! \\ 
-\exists ​ & \verb!EX! 
-\end{array} 
-\] 
-Rendering and input in math notation is also possible using [[http://​proofgeneral.inf.ed.ac.uk/​|ProofGeneral]]. Note: the equality symbol (even if used on '​bool'​ types) binds more strongly than propositional operators, unlike the usual equivalence. 
- 
-Type of first-order formulas is //bool//. 
-++++ 
- 
-Usually we treat formulas as syntax trees and not strings. 
- 
-$FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows: 
-\[\begin{array}{rcl} 
-  FV(x) &=& \{ x \}, \mbox{ for } x \in V \\ 
-  FV(f(t_1,​\ldots,​t_n) &=& F(t_1) \cup \ldots \cup F(t_n) \\ 
-  FV(R(t_1,​\ldots,​t_n) &=& F(t_1) \cup \ldots \cup F(t_n) \\ 
-  FV(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\ 
-  FV(\lnot F) &=& FV(F) \\ 
-  FV(F_1 \land F_2) &=& FV(F_1) \cup FV(F_2) \\ 
-  FV(F_1 \lor F_2) &=& FV(F_1) \cup FV(F_2) \\ 
-  FV(F_1 \rightarrow F_2) &=& FV(F_1) \cup FV(F_2) \\ 
-  FV(F_1 \leftrightarrow F_2) &=& FV(F_1) \cup FV(F_2) \\ 
-  FV(\forall x.F) &=& FV(F) \setminus \{x\} \\ 
-  FV(\exists x.F) &=& FV(F) \setminus \{x\}  
-\end{array}\] 
- 
-If $FV(F) = \emptyset$, we call $F$ a //closed first-order logic formula//, or //​sentence//​.