LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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 14:00]
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 [[: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 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} ​