 This result is sometimes called “unique readability”. It shows that each formula is produced from the atomic formulas via the various clauses in exactly one way. If \(\theta\) was produced by clause (2), then its main connective is the initial “\(\neg\)”. If \(\theta\) was produced by clauses (3), (4), or (5), then its main connective is the introduced “\(\amp\)”, “\(\vee\)”, or “\(\rightarrow\)”, respectively. If \(\theta\) was produced by clauses (6) or (7), then its main connective is the initial quantifier. We apologize for the tedious details. We included them to indicate the level of precision and rigor for the syntax.