Codex @codex  0

A formation rule specifies how well-formed expressions can be constructed from simpler expressions in a formal language. The formal grammar of propositional formulas has rules for propositional variables, negation and binary logical implication.

Start with the propositional variables as atomic symbols and close under the two formation operationsThe set of propositional formulas is the smallest set satisfying these conditions: every logical formula has a finite construction from logical variables by negation and logical implication, and no other strings qualify. In particular, parentheses belong to the binary logical implication formation rule; they cannot be added or removed arbitrarily. Each symbol $p_i$ is one token, regardless of how its index is printed.

Use structural induction on the formation of a propositional formula. A propositional variable has no parentheses. Applying negation to a logical formula adds no parentheses, so preserves equality of the two counts. If $\psi$ and $\chi$ each have equally many opening and closing parentheses, the formation of $(\psi \to \chi )$ adds one of each to their combined counts. Thus every propositional formula satisfiesThis is a necessary condition for being a logical formula; it is not sufficient, since the logical connectives and the placement of symbols must also follow the formation rules.

Not a logical formula. The string has one opening parenthesis and no closing parenthesis, contradicting the parentheses count established above. It also fails the binary logical implication formation rule, whose final symbol must be a closing parenthesis.

A logical formula. Both $p_1$ and $p_2$ are propositional variables, so $(p_1\to p_2)$ and $(p_2\to p_1)$ are logical formulas. Applying the binary logical implication formation rule to this ordered pair of logical formulas gives the displayed whole expression. This supplies a construction of its formula syntax tree rather than merely checking that its parentheses balance.

A useful consequence of the formation rules is that logical formulas form a prefix-free set of strings. To see this, describe a deterministic parser that reads one logical formula from its starting position. On a logical variable it consumes that one symbol. On a negation symbol it recursively reads one following logical formula. On an opening parenthesis it recursively reads a left logical formula, requires a logical implication symbol, recursively reads a right logical formula, and requires the closing parenthesis. Induction on formation proves that, if a valid logical formula begins at the current position, this procedure consumes exactly that logical formula and stops at its end.

Suppose now that both $\alpha$ and $\varphi$ are logical formulas and $\varphi =\alpha ϵ$. The same parser, started at their common first symbol, must stop both at the end of $\alpha$ and at the end of $\varphi$. Its deterministic stopping position cannot differ, so $ϵ$ is empty. HenceThis argument applies to symbol strings; it does not use truth values or logical equivalence.

Fix the particular occurrence of $\alpha$ that is being replaced. The subformula analysis above makes it a node of the formula syntax tree of $\varphi$. Proceed by structural induction on the surrounding logical formula.

If this node is the root, the subformula replacement gives $\beta$, already a logical formula. Otherwise, if $\varphi =\neg \psi$, the chosen occurrence lies inside $\psi$. The induction hypothesis gives a logical formula ${\psi }^{\prime }$ after the subformula replacement there, and the whole result is the logical formula $\neg {\psi }^{\prime }$. If $\varphi =(\psi \to \chi )$, a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either $({\psi }^{\prime }\to \chi )$ or $(\psi \to {\chi }^{\prime })$, each a logical formula by the formation rule. A logical variable has no proper subformula, so there is no additional base case.

Therefore replacing the designated subformula occurrence by any logical formula preserves well-formedness. The argument concerns one chosen occurrence; it does not require simultaneous subformula replacement of every occurrence of the same string.