# Language of Propositional Logic has Unique Parsability

## Theorem

The language of propositional logic $\mathcal L_0$ has unique parsability.

## Proof

It is to be demonstrated that each WFF arises by a unique rule of formation from the bottom-up specification of propositional logic.

The rules $\mathbf W : TF$ and $\mathbf W : \mathcal P_0$ need no further treatment.

From inspection of the first character it is clear that the remaining $\mathbf W : \neg$ and $\mathbf W : Op$ cannot yield the same WFF.

What remains is to establish uniqueness in applying $\mathbf W : \neg$ and $\mathbf W : Op$.

For $\mathbf W : \neg$, this means to consider:

- $\mathbf A = \neg \mathbf B = \neg \mathbf C$

from which it is immediate that $\mathbf B = \mathbf C$.

Lastly, for $\mathbf W : Op$, we have the following lemma:

### Lemma

Let $\mathbf A$ be a WFF.

Suppose that $\mathbf A = \left({B \circ C}\right) = \left({D * E}\right)$.

Then $\mathbf B = \mathbf D$, ${\circ} = {*}$, and $\mathbf C = \mathbf E$.

$\Box$

Having examined all possible combinations of rules of formation, we conclude that $\mathcal L_0$ has unique parsability.

$\blacksquare$

## Comment

Some sources only prove a subset of this result, deeming the rest of the cases a triviality not worth devoting precious space to.