 Prefix-freeness of fully parenthesized formulas

In the grammar $\varphi ::=p_i\mid \neg \varphi \mid (\varphi \to \varphi )$, no logical formula is a proper initial segment of another. A recursive parser reads one variable, or a negation followed by one formula, or a parenthesized pair of formulas separated by implication. Structural induction shows that this parser consumes precisely one whole formula. Its deterministic stopping position proves prefix-freeness. Consequently any formula substring in a valid formula coincides with the formula of a syntax subtree.