Definition·D092
Variables occurring in a term
A bare variable contributes itself; a function application contributes everything occurring in any of its arguments.
For a language
, the set of variables occurring in a term
, written
, is characterized by:
In words
For a term of the language: a bare variable contributes exactly itself, and a function symbol applied to a tuple of terms contributes the union of whatever occurs in each of those terms.
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 · A09 (computed from the citation graph, not asserted).
Remarks
Existence and uniqueness of
, for every term, is T37, exactly as for term values.
(D018, D007) is the family
;
of it (D004) collects everything occurring in any argument. Deliberately named
, distinct from "Var" (the fixed set of *all* variables,
):
is the much smaller, finite set actually occurring in the one term
. For formulas, the analogous notion of *free* variables (D093) differs from this one exactly at a quantifier, which strips its bound variable out.