Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:propositional_logic_syntax [2008/03/10 16:21] vkuncak |
sav08:propositional_logic_syntax [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 3: | Line 3: | ||
Let $V$ be a [[countable set]] of //propositional variables//, denoted by non-terminal //V//. The context-free grammar of propositional logic formulas ${\cal F}$ is the following: | Let $V$ be a [[countable set]] of //propositional variables//, denoted by non-terminal //V//. The context-free grammar of propositional logic formulas ${\cal F}$ is the following: | ||
- | \[ | + | \begin{equation*} |
F ::= V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) | F ::= V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) | ||
- | \] | + | \end{equation*} |
- | We denote the set of all propositional formulas given by the above grammar by ${\cal F}$. | + | We denote the set of all propositional formulas given by the above [[:Notes on Context-Free Grammars|context-free grammar]] by ${\cal F}$. Each propositional formula is a finite sequence of symbols, given by the above context-free grammar. The set ${\cal F}$ is a countable set: we can order all formulas in this set in a sequence (for example, by writing them down in binary alphabet and sorting the resulting strings alphabetically). |
- | Omitting parantheses: | + | Omitting parentheses: |
- | * $\land$, $\lor$ commutative | + | * $\land$, $\lor$ associative |
* priorities, from strongest-binding: $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow, \leftrightarrow)$ | * priorities, from strongest-binding: $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow, \leftrightarrow)$ | ||
- | When in doubt, use parenthesis. | + | When in doubt, use parentheses. |
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 Propositional Logic| | In [[Isabelle theorem prover]] we use this ++++ASCII notation for Propositional Logic| | ||
- | \[ | + | \begin{equation*} |
\begin{array}{c|c} | \begin{array}{c|c} | ||
\mbox{math} & \mbox{Isabelle} \\ \hline | \mbox{math} & \mbox{Isabelle} \\ \hline | ||
Line 27: | Line 27: | ||
{\it false} & \verb!False! \\ | {\it false} & \verb!False! \\ | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
Rendering and input in math notation is also possible using ProofGeneral or Eclipse. | Rendering and input in math notation is also possible using ProofGeneral or Eclipse. | ||
Line 36: | Line 36: | ||
$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}{l} | + | \begin{equation*}\begin{array}{l} |
FV(p) = \{ p \}, \mbox{ for } p \in V \\ | FV(p) = \{ p \}, \mbox{ for } p \in V \\ | ||
+ | FV(\lnot F) = FV(F) \\ | ||
FV(F_1 \land F_2) = FV(F_1) \cup FV(F_2) \\ | 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 \lor F_2) = FV(F_1) \cup FV(F_2) \\ | ||
- | FV(\lnot F) = FV(F) \\ | ||
FV(F_1 \rightarrow 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(F_1 \leftrightarrow F_2) = FV(F_1) \cup FV(F_2) \\ | ||
- | \end{array}\] | + | \end{array}\end{equation*} |
+ | If $FV(F) = \emptyset$, we call $F$ a //ground formula//. |