= Prefix-freeness of fully parenthesized formulas
{title2=$\alpha,\phi\in\operatorname{Form},\quad\phi=\alpha\epsilon\ \Longrightarrow\ |\epsilon|=0$}
In the grammar $\phi::=p_i\mid\neg\phi\mid(\phi\to\phi)$, no <logical formula> is a proper initial segment of another. A recursive <parser> reads one <logical variable>[variable], or a <negation> followed by one <logical formula>[formula], or a parenthesized pair of <logical formula>[formulas] separated by <logical implication>[implication]. <Structural induction> shows that this <parser> consumes precisely one whole <logical formula>[formula]. Its deterministic stopping position proves <prefix-freeness of fully parenthesized formulas>[prefix-freeness]. Consequently any <logical formula>[formula] substring in a valid <logical formula>[formula] coincides with the <logical formula>[formula] of a syntax subtree.
Back to article page
