Theorem·T32
Unique readability of terms
No term is a proper initial segment of another term, and every term decomposes as a variable or a function application in exactly one way.
For a language
: (i)
: if
,
, and
for all
, then
. (ii)
: every
is either
for a unique
, or
for a unique
and unique
with
- never both.
In words
No term is a proper initial segment of another term, and every term is either a bare variable or a function symbol applied to a tuple of shorter terms, in exactly one way: the symbol, and the terms it is applied to, are uniquely determined by the term itself.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1(i). Suppose with and for . By induction on , exactly as in the Locality step of L65's proof (using that and agree below ): for every such . In particular, by T31 applied to : . Suppose toward a contradiction that . Then T31 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 and mutual exclusivity. By structural induction: every is trivially of the first form, and every is trivially of the second (taking its own ), so every term is of at least one form. The two forms exclude each other: if , comparing position gives , i.e. , forcing (L01) - impossible, as in the base case of T31.
- 3(ii), uniqueness of . If , comparing position gives , i.e. , so by L01.
- 4
- 5(ii), uniqueness of . With and as above, comparing entries from position on (T29) gives . We show for every by induction on : assume for all , so and hence (concatAll is a function); call this common sequence . As in the construction of in the proof of T31 (there prefixed by , here not), and are both initial segments of the common sequence . By trichotomy, say without loss of generality ; then , having the smaller domain, is itself an initial segment of (both are initial segments of the same sequence, so they agree wherever both are defined). Comparing entries from position on (T29), is an initial segment of . Since , prefix-freeness (i) gives outright. By induction, for every , i.e. .
∎
Remarks
This is the payoff of the parse-balance machinery: a term genuinely has one and only one syntactic shape, so "the function symbol at the head of
" and "the
-th argument of
" are well-defined notions, not merely one possible reading among several. This is exactly what licenses defining a value, a free-variable set, or (for formulas, by the same technique) a satisfaction clause by genuine recursion on syntax: the recursive equations pin down a unique answer because the case they apply to is itself unique. Every standard treatment of first-order logic (Enderton's "Unique Readability Theorem", Mendelson's analogous lemma) proves exactly this before allowing any function to be defined by recursion on terms or formulas.