Syntax of propositional logic

An arithmetic expression like \(x + 3 * y\) describes precisely one way to combine arithmetic constants (\(3\) in the example) and arithmetic parameters (\(x\) and \(y\) in the example) using arithmetic operations (\(+\) and \(*\) in the example); a propositional formula does the same with boolean constants (true and false), boolean parameters (variables for true and false), and boolean functions such as and and or.

Introduction

Example \(\bot \vee (X_0 \wedge X_1)\) is a propositional formula, where \(\bot\) stands for false, \(\vee\) stands for or, and \(\wedge\) stands for and.

Example \((X_0 \wedge \neg X_1) \vee (\neg X_0 \wedge X_1)\) is another propositional formula, \(\neg\) stands for not.

Clearly, in both examples a formula is a sequence of symbols (a character string). From a technical point of view, it is, however, more reasonable to imagine and define a formula as a tree, where

• a tree has a root and a finite positive number of nodes,
• each node has a label, and
• the children of a node are linearly ordered.

In this example the left child of the root has two children: one is labelled \(X_0\), the other one \(\neg\). In the order the one labelled \(X_0\) comes first and the one labelled \(\neg\) comes second.

For simplicity, when a tree is drawn there is no particular way of indicating nodes other than showing its label, because every node is labelled (and the empty label is not allowed).

Formal definition

A propositional variable is of the form \(X_i\) where \(i\) stands for a natural number. The set of all propositional variables is denoted \(\text{PVars}\). There are two symbols for boolean constants, \(\bot\) and \(\top\), which stand for false and true, respectively, and are read false and true, respectively.

The definition of the set of all propositional formulas is an inductive definition.

Base elements:

• The one-node trees where the only node is labelled with one of the two constant symbols, \(\bot\) and \(\top\), are propositional formulas.
• The one-node trees where the only node is labelled with one of the propositional variables are propositional formulas.

These formulas are called atomic formulas.

Inductive rule:

• If \(C\) is a connective of arity \(n\) and \(\varphi_0, \dots, \varphi_{n-1}\) are propositional formulas, then the tree with root labelled \(C\) and the \(n\) subtrees \(\varphi_0\), ..., \(\varphi_{n-1}\) is a propositional formula.

Illustration of the inductive step

These formulas are called composite formulas.

The set of all propositional formulas is denoted by \(F_\text{PL}\).

Example The tree is a propositional formula; note that \(\bigvee\) has not only arity two, but also arity three according to our list of connectives.

Example The tree is a propositional formula; note that \(\bigvee\) has even arity zero.

Example The tree is not a propositional formula, because \(\neg\) has arity \(1\), but not arity \(3\), and because \(a\) is neither a symbol for a boolean constant, nor a propositional variable, nor a connective.

Commonly used notation

To simplify notation, formulas are often written as sequences of symbols (strings) using parentheses rather than drawn as trees. There is a general notation, which is used in definitions and proofs, and a more human-readable one.

Prefix notation

The general notation is the commonly used prefix notation, where the connective is prefixed to the sequence of the strings for the subtrees and the elements of the sequence of children are separated by commas. Beginning and end of this sequence are marked by an opening and a closing parenthesis.

Example The formula from the first example above is written as \(\bigvee(X_1, X_0, \neg (X_2))\).

Example The formula is written as \(\bigvee()\).

Example The inductive definition of a formula can also be written as follows.

Base elements:

• The symbols \(\bot\) and \(\top\) are propositional formulas.
• Every propositional variable is a propositional formula.

Inductive rule:

• If \(C\) is a connective of arity \(n\) and \(\varphi_0, \dots, \varphi_{n-1}\) are propositional formulas, then \(C(\varphi_0, \dots, \varphi_{n-1})\) is a propositional formula.

Human-readable notation

The starting point for human-readable notation is the above prefix notation. The difference is that some parentheses are saved to avoid cluttering and connectives are written infix to get rid of commas.

The rules for human-readable notation are:

1. If a connective is used with arity two or more, then it is written in infix notation with parentheses around the string. At the same time, capital connectives become small connectives (which is consistent with the semantics). Example: \(\neg(X_0 \vee X_1 \vee X_2)\) instead of \(\neg(\bigvee(X_0, X_1, X_2))\).
2. These parentheses can be omitted for the connective at the root (in the corresponding tree) and if the connective of the corresponding parent node has lower precedence. For the precedence of the connectives, see list of connectives. Example: \(X_0 \vee X_1 \vee X_2\) instead of \(\bigvee(X_0, X_1, X_2)\). Example: \(X_0 \rightarrow X_1 \vee \neg X_2\) instead of \(X_0 \rightarrow (X_1 \vee \neg X_2)\).
3. Parentheses for a connective with arity \(1\) can be omitted when the child is a constant symbol or a variable or a connective with arity \(1\). Example: \(\neg X_0\) instead of \(\neg(X_0)\).
4. The infix notation is only allowed for the connectives \(\bigwedge\), \(\bigvee\), and \(\bigoplus\). Example: \(X_0 \oplus X_1\oplus X_2\) is allowed in the humand-readable notation while \(X_0 \dot\vee X_1 \dot{\vee} X_2\) is forbidden.

Meta notation

In certain situations, it is useful to work with a symbol like \(\bigwedge\) just as with \(\sum\). This means that \[\bigwedge_{i < n} X_i\] stands for \[\bigwedge(X_0, \dots, X_{n-1}) \enspace,\] which can be written as \[X_0 \wedge \dots \wedge X_{n-1}\enspace.\]