# Differences

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

 sav08:propositional_logic_syntax [2009/04/08 18:34]philippe.suter sav08:propositional_logic_syntax [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/04/08 18:34 philippe.suter 2009/04/08 18:34 philippe.suter 2008/03/18 14:00 vkuncak 2008/03/18 13:56 vkuncak 2008/03/18 13:54 vkuncak 2008/03/18 11:16 vkuncak fixed accidental edit2008/03/18 11:10 vkuncak 2008/03/11 14:36 vkuncak 2008/03/10 19:33 vkuncak 2008/03/10 16:32 vkuncak 2008/03/10 16:30 vkuncak 2008/03/10 16:21 vkuncak 2008/03/10 11:17 vkuncak 2008/03/10 10:58 vkuncak 2008/03/10 10:43 vkuncak 2008/03/06 10:59 vkuncak 2008/03/05 21:02 vkuncak 2008/03/05 21:02 vkuncak 2008/03/05 20:46 vkuncak created Next revision Previous revision 2009/04/08 18:34 philippe.suter 2009/04/08 18:34 philippe.suter 2008/03/18 14:00 vkuncak 2008/03/18 13:56 vkuncak 2008/03/18 13:54 vkuncak 2008/03/18 11:16 vkuncak fixed accidental edit2008/03/18 11:10 vkuncak 2008/03/11 14:36 vkuncak 2008/03/10 19:33 vkuncak 2008/03/10 16:32 vkuncak 2008/03/10 16:30 vkuncak 2008/03/10 16:21 vkuncak 2008/03/10 11:17 vkuncak 2008/03/10 10:58 vkuncak 2008/03/10 10:43 vkuncak 2008/03/06 10:59 vkuncak 2008/03/05 21:02 vkuncak 2008/03/05 21:02 vkuncak 2008/03/05 20:46 vkuncak created 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 [[: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). 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). Line 11: Line 11: * $\land$, $\lor$ associative * $\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(\lnot F) = FV(F) \\ Line 43: Line 43: 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//. If $FV(F) = \emptyset$, we call $F$ a //ground formula//.