Differences
This shows you the differences between two versions of the page.
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//. | ||