Definition·D091
Satisfaction of a formula in a structure
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
by:
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 left side failing or the right side holding, 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
. The meta-level
used on the right of each clause are the ordinary logical words of this wiki's own reasoning, not further formulas of
; 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.