This is an old revision of the document!
Propositional Logic Syntax
Let be the set of propositional variables, denoted by non-terminal V. The context-free grammar of propositional logic formulas is the following:
\[
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 .
Omitting parantheses:
- , commutative
- priorities, from strongest-binding:
When in doubt, use parenthesis.
Notation: when we write this means that and are identical formulas (with identical syntax trees). For example, , but it is not the case that .
In Isabelle theorem prover we use this
ASCII notation for Propositional Logic
Usually we work with syntax trees, as in Problem 3 in Homework 1.
denotes the set of free variables in the given propositional formula and can be defined recursively as follows: \[\begin{array}{l}
FV(p) = \{ p \}, \mbox{ for } p \in V \\ 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(\lnot F) = FV(F) \\ 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) \\
\end{array}\]