Axiomatic WikiWWikiTTheoremsSatisfaction is well-defined
Theorem·T36
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.
- 2By T35 (ii), (of length ) is exactly one of the nine forms of D083, written via the notation introduced there as , , , one of , , , , or one of , ; we check each determines .
- 3eq, rel. If is ( ): 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 (for and with ): is a determinate tuple, and whether it lies in is determinate; the rel clause of D091 determines .
- 4neg. If is ( ): by D109, , so . 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 .
- 5
- 6forall, exists. If is or for some and (D109): in either case , so . 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 matching clause of D091 (forall or exists, respectively), 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. The nine-way case split in the proof is written with the ordinary connective, quantifier, equality, and application notation for formulas and terms, rather than spelled out as raw constructor sequences. 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.