Boolean Interpretation is Well-Defined/Proof 1

From ProofWiki
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$