Lab for Automated Reasoning and Analysis LARA

Propositional Logic Syntax

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)
\end{equation*}

We denote the set of all propositional formulas given by the above 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 parentheses:

  • $\land$, $\lor$ associative
  • priorities, from strongest-binding: $(\lnot)\ ;\ (\land, \lor)\ ;\ (\rightarrow, \leftrightarrow)$

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$.

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.

$FV$ denotes the set of free variables in the given propositional formula and can be defined recursively as follows:

\begin{equation*}\begin{array}{l}
  FV(p) = \{ p \}, \mbox{ for } p \in V \\
  FV(\lnot F) = FV(F) \\
  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(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}\end{equation*}

If $FV(F) = \emptyset$, we call $F$ a ground formula.

 
sav08/propositional_logic_syntax.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice