# Boolean Interpretation is Well-Defined/Proof 1

Jump to navigation
Jump to search

## Theorem

Let $\mathcal L_0$ be the language of propositional logic.

Let $v: \mathcal L_0 \to \{T, F\}$ be a boolean interpretation.

Then $v$ is well-defined.

## Proof

By Language of Propositional Logic has Unique Parsability, $\mathcal L_0$ is uniquely parsable.

Therefore, the Principle of Definition by Structural Induction can be applied to $\mathcal L_0$.

By inspection, we see that the definition of the boolean interpretation $v$ follows the bottom-up specification of propositional logic.

Hence the Principle of Definition by Structural Induction implies that $v$ is well-defined.

$\blacksquare$