Formula Position (Propositional Logic)

logic

Definition

Propositional Formula Position

A propositional formula position is a finite sequence of positive integers that specifies one occurrence of a subformula inside a propositional formula.

If , we also say that occurs in at the position .

Recursive Definition

The following clauses state which sequences are valid positions and what subformula each position denotes. They are read as inductive rules: every valid position is obtained by finitely many applications of the clauses below.

Root Position

For every propositional formula , the empty sequence is a position in , and

Further:

Conjunction and Disjunction

Let . If has the form:

then for all the position is a position in , and:

Further:

Negation

Let . If has the form:

then is a position in , and:

Further:

Implication

Let . If has the form:

then and are positions in , and:

Further:

Equivalence

Let . If has the form:

then and are positions in , and:

Further:

Occurrence

If we say that occurs in at position . Different positions may determine different occurrences of the same subformula.

Examples

Let

Then the following are positions in :

The corresponding subformulas are:

Let

Then

So the same subformula occurs in at two different positions. This is why positions are useful when one wants to talk about one fixed occurrence.