Axiomatic WikiWWikiDDefinitionsSatisfaction of a formula in a structure
Definition·D091
When a structure, under an assignment, makes a formula true - characterized by recursion on the formula's five formation rules.
For an L-structure
and assignment
into
, that
satisfies
under
, written
, is characterized for
, using the notation for formulas and terms of
, as follows. For
:
For
and
with
:
For
:
For
:
For
and
:
In words
Two terms are equal exactly when they have the same value. A relation symbol applied to a tuple of terms holds exactly when the tuple of values lies in the relation's interpretation. A negation holds exactly when the negated formula does not. A conjunction holds exactly when both sides do, a disjunction when at least one side does, an implication when the right side holds whenever the left side does, and a biconditional when both sides agree. A universal quantification holds exactly when the body holds under every way of reassigning the bound variable, and an existential quantification when it holds under at least one such reassignment.
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 relation, for every formula, is T36 (by strong induction on the length of
, using unique readability to know the five-way case split is genuinely exhaustive and non-overlapping). The logical symbol indices
match D083's five formation rules exactly:
is equality,
is negation,
are
, and
are
. Both the object-level formulas on the left of
and the meta-level claims on the right are written with these same symbols (D109); only context, which side of
something sits on, distinguishes the two levels, exactly as in any informal treatment of semantics.
is the updated assignment sending
to
and agreeing with
elsewhere. Nonemptiness of
(D086) is what keeps the universal and existential clauses from being vacuously true and false respectively for every formula.