Unique readability theorem (source code)

= Unique readability theorem

The <unique readability theorem> asserts uniqueness of the outer <formal grammar>[formation rule] and its immediate components in a <logical formula>. For the fully parenthesized language with <negation> and <logical implication>[implication], every <logical formula>[formula] is uniquely a <logical variable>[variable], a <negation> of one <logical formula>[formula], or an <logical implication>[implication] between an <ordered pair> of <logical formula>[formulas]. It gives a well-defined <syntax tree of a formula>[syntax tree] and licenses recursive definitions and <structural induction> on <logical formula>[formulas].