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:

   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 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:

  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) \\

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