Definition·D082
Term of a language
A term is a sequence belonging to every term-admissible set: the smallest one, built from variables and function symbols alone.
For a language
:
In words
A sequence w is a term of L exactly when, for every set C, if C is term-admissible for L then w belongs to C: the terms are the smallest term-admissible set.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Existence:
is itself term-admissible, so Separation carves
out of it, exactly mirroring the construction of ω as the intersection of all inductive sets. The result does not depend on which term-admissible set was used to start, by Extensionality, since the displayed condition already forces membership in every term-admissible set. That
is itself term-admissible, and is contained in every term-admissible set, is L62, mirroring L04; this is what will license structural induction on terms.