Theorem·T35
Unique readability of formulas
No formula is a proper initial segment of another formula, and every formula decomposes as an equality, a relation application, a negation, a binary connective, or a quantification, in exactly one way.
For a language
: (i)
: if
,
, and
for all
, then
. (ii)
: every
is exactly one of
for unique
and unique
;
for unique
and unique
with
;
for unique
;
for unique
and unique
and unique
; or
for unique
, unique
, and unique
- never two of these at once.
In words
No formula is a proper initial segment of another formula, and every formula decomposes in exactly one way: it is either an equality of two terms, a relation symbol applied to a tuple of terms, a negation of a formula, a binary connective joining two formulas, or a quantifier over a variable applied to a formula - the leading symbol, and the pieces it is built from, are uniquely determined by the formula itself.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1(i). Suppose with and for . By induction on , exactly as in the Locality step of L66's proof (using that and agree below ): for every such . In particular, by T34 applied to : . Suppose toward a contradiction that . Then T34 applied to (positivity, at ) gives , i.e. . But in (L15 (vi)), so by order-preservation of the embedding, contradicting via totality and L15 (i) (irreflexivity, ruling out both). So , and with the agreement hypothesis, as sets of pairs (Extensionality).
- 2(ii), existence. By structural induction: each of the five clauses of D083 directly produces a formula of the matching shape (taking its own witnesses), so every formula is of at least one of the five forms.
- 3(ii), mutual exclusivity. The five forms' possible values of are pairwise disjoint: always has first coordinate , while every has first coordinate , and (distinct naturals, (P3)), so L01 rules out the relation form coinciding with any of the other four. Among the forms, the index sets (eq), (neg), (bin), (quant) are pairwise disjoint subsets of the eight indices (pairwise distinct natural numbers, (P3)), so , i.e. , forces (L01), which is impossible when are drawn from two different (disjoint) families. As is a single fixed value, is of at most one of the five forms.
- 4(ii), uniqueness for eq. Suppose with . Comparing entries from position on (T29), ; call this common sequence . By trichotomy, say without loss of generality ; since and are both initial segments of the same (comparing entries via T29) and , is an initial segment of . Since , T32 (i) gives outright. Then comparing entries of from position on (T29) gives .
- 5(ii), uniqueness for rel. Suppose with , . Comparing position (T29), , i.e. , so (L01); hence , so have the same length . Comparing entries from position on, . Exactly as in the "uniqueness of " step of the proof of T32 (ii) - induction on , using trichotomy and T32 (i) at each step - for every , i.e. .
- 6(ii), uniqueness for neg. Suppose with . By trichotomy, say without loss of generality . For (hence also ): comparing entries from position on (T29), applicable to both decompositions, . So is an initial segment of ; since , part (i) gives outright.
- 7(ii), uniqueness for bin. Suppose with , . Comparing position , so (L01). With , exactly as in the uniqueness argument for eq - comparing entries from position on, applying trichotomy and part (i) (for formulas, in place of T32 (i) for terms) to , then comparing the remainder - and .
- 8(ii), uniqueness for quant. Suppose with , , . Comparing position : (L01). Comparing position : , i.e. , so (L01). Comparing entries from position on (T29), and arguing exactly as in the uniqueness step for neg - trichotomy plus part (i) applied to - .
∎
Remarks
The formula-level payoff of the formula parse-balance machinery, mirroring the term case one level up: a formula genuinely has one and only one syntactic shape, so "the leading symbol of a formula" and "the pieces it is built from" are well-defined notions, not merely one possible reading among several. Together with unique readability of terms, this is what will license defining the satisfaction relation between a structure and a formula by genuine recursion on formula structure - the recursive clauses, one for equality, relation application, negation, each connective, and each quantifier, pin down a unique answer because the case they apply to is itself unique. Every standard treatment of first-order logic proves exactly this before allowing any function or relation to be defined by recursion on formulas.