LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav08:first-order_logic_syntax [2008/03/19 10:24]
vkuncak 		sav08:first-order_logic_syntax [2015/04/21 17:30] (current)
Line 7: Line 7:
 The set $V$ denotes countably infinite set of first-order variables, which is independent of the language. The set $V$ denotes countably infinite set of first-order variables, which is independent of the language.
  
-\[+\begin{equation*}
 \begin{array}{rcl} \begin{array}{rcl}
     F &::​=&​ A \mid \lnot F \mid (F \land F) \mid (F \lor F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\     F &::​=&​ A \mid \lnot F \mid (F \land F) \mid (F \lor F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\
Line 14: Line 14:
     T & ::= & V \mid f(T,​\ldots,​T)  ​     T & ::= & V \mid f(T,​\ldots,​T)  ​
 \end{array} \end{array}
-\]+\end{equation*}
  
 Terminology summary: Terminology summary:
Line 31: Line 31:
  
 Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$, $ar(Q) = 1$, $ar(R) = 2$, $ar(f) = 2$. Then Example: Consider language ${\cal L} = \{ P, Q, R, f \}$ with $ar(P) = 1$, $ar(Q) = 1$, $ar(R) = 2$, $ar(f) = 2$. Then
-\[+\begin{equation*}
     \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x)     \lnot \forall x.\, \forall y. R(x,y) \land Q(x) \rightarrow Q(f(y,x)) \lor P(x)
-\]+\end{equation*}
 denotes denotes
-\[+\begin{equation*}
     \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x)))))     \lnot (\forall x.\ (\forall y. ((R(x,y) \land Q(x)) \rightarrow (Q(f(y,x)) \lor P(x)))))
-\]+\end{equation*}
  
 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 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
-\[+\begin{equation*}
     \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x)     \lnot \forall x.\, \forall y. x \mathop{R} y \land Q(x) \rightarrow Q(y \mathop{f} x) \lor P(x)
-\]+\end{equation*}
  
 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$. 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| In [[Isabelle theorem prover]] we use this ++++ASCII notation for First-Order Logic|
-\[+\begin{equation*}
 \begin{array}{c|c} ​ \begin{array}{c|c} ​
 \mbox{math} & \mbox{Isabelle} \\ \hline \mbox{math} & \mbox{Isabelle} \\ \hline
Line 60: Line 60:
 \exists ​ & \verb!EX! \exists ​ & \verb!EX!
 \end{array} \end{array}
-\]+\end{equation*}
 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. 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.
  
Line 69: Line 69:
  
 $FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows: $FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows:
-\[\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl}
   FV(x) &=& \{ x \}, \mbox{ for } x \in V \\   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(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(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(t_1 = t_2) &=& F(t_1) \cup F(t_2) \\
   FV(\lnot F) &=& FV(F) \\   FV(\lnot F) &=& FV(F) \\
Line 81: Line 81:
   FV(\forall x.F) &=& FV(F) \setminus \{x\} \\   FV(\forall x.F) &=& FV(F) \setminus \{x\} \\
   FV(\exists x.F) &=& FV(F) \setminus \{x\}    FV(\exists x.F) &=& FV(F) \setminus \{x\} 
-\end{array}\]+\end{array}\end{equation*}
  
 If $FV(F) = \emptyset$, we call $F$ a //closed first-order logic formula//, or //​sentence//​. If $FV(F) = \emptyset$, we call $F$ a //closed first-order logic formula//, or //​sentence//​.