Theorem·T36
Satisfaction is well-defined
The nine clauses of def-satisfaction never leave a formula undetermined and never force two conflicting verdicts on it.
For an L-structure
, assignment
, and
:
(D091) is a well-defined proposition - D091's clauses determine, uniquely, whether it holds.
In words
For any formula of the language, whether the structure under the assignment satisfies it is settled outright, never left open or contradictorily double-determined.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A09 (computed from the citation graph, not asserted).
Proof
- 1Setup, generalizing over assignments. Fix the L-structure . We show, by strong induction on , the stronger claim: for every assignment into and every with : is a well-defined proposition, determined solely by D091's clauses together with the (already-determined, by the induction hypothesis) truth of for every assignment and every formula of length . Taking gives the theorem. Generalizing over the assignment is essential: the quantifier clauses below need satisfaction of a *shorter* formula, but under a *different*, updated assignment - not under itself.
- 2
- 3eq, rel. If ( ): T33 gives and exist uniquely - unconditionally, independent of this induction - so whether they are equal is a determinate fact (Extensionality); by the eq clause of D091, this determines . Similarly if : is a determinate tuple, and whether it lies in is determinate; the rel clause of D091 determines .
- 4neg. If ( ): . Indeed every formula has length : were , its balance would need to equal both (the base clause of D090, which holds at position regardless of the sequence) and (T34, the end clause, which applies at position ) - impossible, as is injective and . By the induction hypothesis (at , ), is well-defined; by the neg clause of D091, so is .
- 5and, or, implies, iff. If ( , ): as in the neg case, , so and likewise . By the induction hypothesis (at , and at , ), and are both well-defined; by the matching clause of D091 ( , or according to ), so is .
- 6forall, exists. If ( , , ): . For every , is an assignment into (D087), so by the induction hypothesis (at the assignment and , of length ): is well-defined. As this holds for every , both "for all , ..." and "for some , ..." are well-defined (meta-level) propositions; by the forall/exists clause of D091 (according to ), so is .
- 7Conclude. Every form determines from the induction hypothesis alone, so T08 gives the stronger claim for every , hence for every assignment and every . Taking : is well-defined for every .
∎
Remarks
Confirms the satisfaction relation
is well posed for every formula, not just an informally plausible recursive scheme. As in the term case, the proof is strong induction on length, with the case split at each length genuinely justified by unique readability - but the quantifier clauses additionally force the induction hypothesis to be generalized over every assignment, not just the one fixed at the outset, since a quantifier reaches into a shorter formula under a *different* assignment. With this in hand, a structure can be said to model a formula or a theory, and one formula can be said to semantically entail another, setting up soundness and, with a deduction system, Gödel's completeness theorem.