• 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)
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//​.