Axiomatic WikiWWikiDDefinitionsValue of a term in a structure
Definition·D089
Evaluate a term by looking up bare variables in the assignment and applying a function symbol's interpretation to the already-evaluated arguments.
For an L-structure
and assignment
into
, the value
of a term
is the element of
characterized by, writing terms in the notation of D109: for
,
and for
and
with
,
In words
A bare variable evaluates to whatever the assignment gives it, and a function symbol applied to a matching-arity tuple of terms evaluates by first evaluating each of those terms, then applying the function's interpretation to the resulting tuple of values.
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 this value, for every term, is T33 (by strong induction on the length of
, using unique readability to know the case split is genuinely exhaustive and non-overlapping - without it, these two clauses would only pin down a value if a term could not be read two different ways).
(D018) is the tuple
, a member of
(D085) matching the arity
expects (D086).