Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:propositional_logic_syntax [2008/03/18 11:10] vkuncak |
sav08:propositional_logic_syntax [2008/03/18 13:56] vkuncak |
||
---|---|---|---|
Line 6: | Line 6: | ||
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) | ||
\] | \] | ||
- | We denote the set of all propositional formulas given by the above grammar by ${\cal F}$. This 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). | + | We denote the set of all propositional formulas given by the above 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 parantheses: | ||
Line 15: | Line 15: | ||
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 Propositional Logic| |
\[ | \[ | ||
\begin{array}{c|c} | \begin{array}{c|c} |