@cite{veltman-1996} — Full Study #
@cite{veltman-1996}
Regression tests for @cite{veltman-1996}'s update semantics with defaults.
§3 Examples (Examples 3.10) #
Finite verification of the key properties of "normally" and "presumably" over a 4-world type with atoms p, q.
§4 Specificity (Tweety Triangle & Nixon Diamond) #
Expectation frames resolve specificity (Tweety) and conflicting defaults (Nixon) using the subdomain-based normality check.
§5 Inference Patterns #
Conjunction of Consequents (CC) is valid for the default conditional ⇝. Contraposition and Strengthening the Antecedent fail (counterexamples).
§5–6 Generics Bridge #
The normality ordering in update semantics plays the same role as the normalcy predicate in the GEN operator for generic sentences.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
Instances For
After "normally p", learning ¬p doesn't crash — the info state still has ¬p-worlds. Rules can have exceptions.
After "normally p", the globally optimal worlds are exactly the p-worlds. So "normally ¬p" is unacceptable: no optimal world satisfies ¬p. This is @cite{veltman-1996}'s coherence check (Definition 3.9).
After "normally p" then learning ¬p, "presumably p" fails. The optimal worlds in {w | ¬p w} are all ¬p-worlds (mutually equivalent under the p-biased ordering).
@cite{veltman-1996}, Examples 3.10(ii): normally p, ¬p ⊬ presumably p.
But exceptions don't destroy the rule: "normally p" still holds.
@cite{veltman-1996}, Examples 3.10(ii): normally p, ¬p ⊩ normally p.
Irrelevant information doesn't block presumptions: after "normally p" and learning q, "presumably p" still succeeds.
@cite{veltman-1996}, Examples 3.10(iii): normally p, q ⊩ presumably p.
One default being defeated doesn't affect unrelated defaults.
@cite{veltman-1996}, Examples 3.10(iv): normally p, normally q, ¬p ⊩ presumably q.
When two defaults conflict with the facts, neither presumption goes through. w₂ (¬p, q) is optimal but ¬p, so "presumably p" fails.
@cite{veltman-1996}, Examples 3.10(v): normally p, normally q, ¬(p ∧ q) ⊬ presumably p.
Symmetric: w₁ (p, ¬q) is optimal but ¬q, so "presumably q" fails.
@cite{veltman-1996}, Examples 3.10(v): normally p, normally q, ¬(p ∧ q) ⊬ presumably q.
Equations
Instances For
birdFlies is normal among birds.
penguinFlies is NOT normal among birds — specificity.
penguinNoFly is normal among penguins.
quakerPacifist is normal among Quakers.
repNotPacifist is normal among Republicans.
quakerPacifist is NOT normal among Republicans (disjoint domains).
Conjunction of Consequents (CC): after processing "if φ then normally ψ" and "if φ then normally χ", the ordering at the φ-domain already respects (ψ ∧ χ).
This is the mathematical core of CC: sequential refinement by ψ and χ produces an ordering that promotes (ψ ∧ χ)-worlds.
@cite{veltman-1996}, §5 (p.256): CC is valid.
CC at the frame level: after two refinements at the same domain, further refinement by the conjunction is a no-op.
Contraposition fails: after "if p then normally q", w₁ (p, ¬q) is still normal among ¬q-worlds — the frame at d_¬q is untouched.
If contraposition held, all normal ¬q-worlds would satisfy ¬p. But w₁ is a normal ¬q-world that satisfies p.
@cite{veltman-1996}, §5 (p.255).
Strengthening the Antecedent fails: after "if p then normally q", the frame at d_{p∧q} is untouched (since d_{p∧q} ≠ d_p).
@cite{veltman-1996}, §5 (p.256).
Defeasible Modus Tollens fails for ExpFrame.normal:
after "if p then normally q" and learning ¬q, w₁ (a p-world)
is still normal among ¬q-worlds. No subdomain of d_nq = {w₀, w₁}
equals d_p = {w₁, w₃}, so the refined ordering is never consulted.
This shows that DMT requires the full dynamic derivation
(processing the conditional, then asserting ¬q, then testing
presumably ¬p) rather than a single ExpFrame.normal check.
Generics as defaults (@cite{veltman-1996}, §5–6).
The truth conditions of the GEN operator ("P's are normally Q"): ∀w ∈ optimal(d). scope(w) are exactly the conditions for the "presumably" test to pass in update semantics.
This theorem witnesses the structural identity: "all optimal worlds
in a domain satisfy the scope" is just the definition of optimality
restated. The substantive bridge is that NormalityOrder.optimal
provides the normalcy predicate for GEN, and NormalityOrder.refine
provides the dynamic mechanism for learning new generic rules.