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:
\[
{\cal 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)
\]
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}\]