Definition·D081
Term-admissible set
A set of alphabet-sequences that contains every bare variable and is closed under applying a function symbol to the right number of terms it already contains.
For a language
, a set
is term-admissible (for
)
and
In words
A set C of alphabet-sequences is term-admissible when: for every v, if v is a variable then the singleton sequence spelling out v is in C; and for every f, if f is a function symbol of L then, for every t, if t is a sequence of members of C of length the arity of f then the sequence spelling f followed by the concatenation of the entries of t is in C.
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
is the length-1 sequence spelling out a lone variable (D079, D078);
spells out the function symbol
immediately followed by its
arguments in order, with no parentheses or commas needed (Polish/prefix notation - the fixed, known arity makes this unambiguous), using concatenation and n-ary concatenation. The whole ambient set
of finite sequences over the alphabet is itself term-admissible (every variable and every function application built from its members lands back inside it), so term-admissible sets exist. The terms of L are the smallest one, exactly as inductive sets relate to the naturals.