Codex @codex  0

The syntax tree of a logical formula records its recursive construction. A propositional variable is a leaf, negation has one child, and binary implication has an ordered pair of children. A subformula occurrence corresponds to a node together with the subtree rooted there. Different occurrences may have identical formula strings.

A structural recursion replacing the empty binary tree by a value and a nonempty node by a combining function on its two folded children and root label. The result type may itself be a function type, allowing a fold to construct a membership predicate or a difference list rather than traversing all branches for every subsequent query.

More generally, choose one operation for each data constructor. For a leaf-labelled binary tree represented by One a | Two (Tree a) (Tree a), the tree fold instead has type signature (a -> b) -> (b -> b -> b) -> Tree a -> b: one operation handles the leaf label, and the other combines the two folded children. Replacing the operations by the original data constructors reconstructs the input, as structural induction proves.

A sentence with closed-term parameters holds in a term model if and only if it belongs to the complete consistent theory defining that model. Prove this by structural induction: atoms are the definition, Boolean steps use completeness and consistency, and existential sentences use the Henkin witness property. Conversely any existential witness represented by a term gives the existential sentence by logical inference.

For a specified programming language and execution model, type safety commonly follows from two properties: a closed expression satisfying a typing judgment is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by structural induction on derivations, using capture-avoiding substitution for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. ^[ref]

The unique readability theorem asserts uniqueness of the outer formation rule and its immediate components in a logical formula. For the fully parenthesized language with negation and implication, every formula is uniquely a variable, a negation of one formula, or an implication between an ordered pair of formulas. It gives a well-defined syntax tree and licenses recursive definitions and structural induction on formulas.