 Balanced parentheses in propositional syntax

Every propositional formula generated by a parenthesized grammar has equally many opening and closing parentheses. By structural induction, atomic formulas begin with equal zero counts; negation preserves them; and a parenthesized binary logical connective adds its two subformula counts and one parenthesis of each kind. An optional paired-parenthesis construction also adds one to both counts. This necessary syntactic invariant is useful for checking generated expressions, though equal counts alone do not guarantee correctly nested syntax.