• English only

# Differences

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

 sav08:first-order_logic_syntax [2008/03/19 10:24]vkuncak sav08:first-order_logic_syntax [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/24 11:36 vkuncak 2008/03/19 10:24 vkuncak 2008/03/18 12:17 vkuncak 2008/03/18 12:17 vkuncak 2008/03/18 12:12 vkuncak 2008/03/18 11:44 vkuncak 2008/03/18 11:31 vkuncak 2008/03/18 11:31 vkuncak 2008/03/18 11:18 vkuncak 2008/03/18 11:17 vkuncak 2008/03/18 11:15 vkuncak 2008/03/18 11:09 vkuncak 2008/03/18 11:07 vkuncak 2008/03/18 11:07 vkuncak 2008/03/18 11:05 vkuncak 2008/03/18 11:04 vkuncak 2008/03/18 11:03 vkuncak 2008/03/18 11:03 vkuncak 2008/03/17 21:35 vkuncak 2008/03/13 15:54 vkuncak 2008/03/13 13:08 vkuncak 2008/03/13 12:35 vkuncak 2008/03/13 12:11 vkuncak 2008/03/13 12:11 vkuncak 2008/03/13 12:10 vkuncak 2008/03/13 12:08 vkuncak 2008/03/13 12:08 vkuncak created Next revision Previous revision 2008/03/24 11:36 vkuncak 2008/03/19 10:24 vkuncak 2008/03/18 12:17 vkuncak 2008/03/18 12:17 vkuncak 2008/03/18 12:12 vkuncak 2008/03/18 11:44 vkuncak 2008/03/18 11:31 vkuncak 2008/03/18 11:31 vkuncak 2008/03/18 11:18 vkuncak 2008/03/18 11:17 vkuncak 2008/03/18 11:15 vkuncak 2008/03/18 11:09 vkuncak 2008/03/18 11:07 vkuncak 2008/03/18 11:07 vkuncak 2008/03/18 11:05 vkuncak 2008/03/18 11:04 vkuncak 2008/03/18 11:03 vkuncak 2008/03/18 11:03 vkuncak 2008/03/17 21:35 vkuncak 2008/03/13 15:54 vkuncak 2008/03/13 13:08 vkuncak 2008/03/13 12:35 vkuncak 2008/03/13 12:11 vkuncak 2008/03/13 12:11 vkuncak 2008/03/13 12:10 vkuncak 2008/03/13 12:08 vkuncak 2008/03/13 12:08 vkuncak created 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//​.

sav08/first-order_logic_syntax.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice