Differences
This shows you the differences between two versions of the page.
sav08:first-order_logic_syntax [2008/03/18 12:12] 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}{l} | ||
- | FV(x) = \{ x \}, \mbox{ for } x \in V \\ | ||
- | 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 formula//. | ||