Veltman (1996): defaults in update semantics

[Vel96] treats normally φ as an update of an agent's expectations rather than a sentence about them: a state is a pair of an expectation pattern (a preorder on worlds) and the agent's knowledge of the facts, normally φ refines the pattern in favour of φ-worlds, and presumably φ tests whether φ holds in the optimal worlds of the state. That §3 system is Semantics/Dynamic/UpdateSemantics/Default.lean; the first section checks its Examples 3.10 on the paper's four worlds, the rain-or-snow contrast that shows normally (p ∨ q) to be stronger than normally p, and normally_not_normally_or.

The heart of the paper (§4) adds restricted rules if φ, then normally ψ (φ ⇝ ψ): an expectation frame assigns a pattern to every domain d of worlds (Definition 4.2), a world is normal in d when it is top-ranked in every subdomain containing it (Definition 4.3), a frame is coherent when every nonempty domain has a normal world, accepting φ ⇝ ψ refines the pattern at ⟦φ⟧ and crashes when the result is incoherent (Definitions 4.5–4.6), and a set of defaults applies within s when every domain extending s has a normal world complying with them (Definition 4.9). The optimal worlds of a state comply with a maximal applicable set of defaults (Definition 4.13), which Proposition 4.14 lets one compute over the explicitly accepted rules. Since every frame an agent reaches from the minimal state is the refinement of the total frame by the rules it has accepted, a frame is presented here by its list of rules (Frame.ofRules): that makes coherence, normality, applicability and the optimal worlds decidable, so each verdict of the paper is checked by decide on Veltman's eight worlds over the atoms p, q, r. Validity is his validity₁ (§1.2): the minimal state updated with the premises in order accepts the conclusion (Valid).

Proved in general: Definition 4.5's refinement clause as theorems about the presentation (ofRules_cons_self, ofRules_cons_of_ne), Proposition 4.7 as the equivalence of coherent acceptance with the new rule's applicability within its own domain (coherent_cons_iff), Conditional Identity and Conjunction of Consequents (rule_self, conjConsequents), and the §5 observation that Weakening the Consequent never crashes a state (weakenConsequent_coherent). Checked on the model: Examples 4.8 and 4.11, the §5 benchmarks (the Nixon diamond, the student–adult–employment argument, Independence), the validity of defeasible Modus Tollens and of Modus Ponens over Modus Tollens on a cyclic net, the failure of Hypothetical Syllogism, Contraposition and Strengthening the Antecedent together with their defeasible versions, and the near-validity of Strengthening with a Consequent and Disjunction of Antecedents.

Rules with exceptions (§3)

inductive Veltman1996.PQWorld : Type

Veltman's four worlds over the atoms p, q: w₀ = ∅, w₁ = {p}, w₂ = {q}, w₃ = {p, q}.

• w₀ : PQWorld
• w₁ : PQWorld
• w₂ : PQWorld
• w₃ : PQWorld

@[instance_reducible]

instance Veltman1996.instDecidableEqPQWorld : DecidableEq PQWorld

Equations

• Veltman1996.instDecidableEqPQWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Veltman1996.atomP : PQWorld → Prop

Equations

• Veltman1996.atomP Veltman1996.PQWorld.w₁ = True
• Veltman1996.atomP Veltman1996.PQWorld.w₃ = True
• Veltman1996.atomP x✝ = False

def Veltman1996.atomQ : PQWorld → Prop

Equations

• Veltman1996.atomQ Veltman1996.PQWorld.w₂ = True
• Veltman1996.atomQ Veltman1996.PQWorld.w₃ = True
• Veltman1996.atomQ x✝ = False

theorem Veltman1996.ex310_exception : ((Veltman1996.σ₀✝.promote atomP).assert fun (x : PQWorld) => ¬atomP x).info.Nonempty

Rules can have exceptions: after normally p, learning ¬p does not crash (3.10(i)).

theorem Veltman1996.ex310_conflict : ¬∃ w ∈ Core.Order.Normality.optimal (Veltman1996.σ₀✝.promote atomP).order Set.univ, ¬atomP w

But the opposite rule is then unacceptable: no optimal world of 0[normally p] is a ¬p-world (3.10(i)).

theorem Veltman1996.ex310_defeat : ¬∀ w ∈ ((Veltman1996.σ₀✝.promote atomP).assert fun (x : PQWorld) => ¬atomP x).optimal, atomP w

Exceptions defeat presumptions: normally p, ¬p ⊮ presumably p (3.10(ii)).

theorem Veltman1996.ex310_rule_persists : Core.Order.Normality.respects ((Veltman1996.σ₀✝.promote atomP).assert fun (x : PQWorld) => ¬atomP x).order atomP

But not the rule: normally p, ¬p ⊩ normally p (3.10(ii)).

theorem Veltman1996.ex310_irrelevant (w : PQWorld) : w ∈ ((Veltman1996.σ₀✝.promote atomP).assert atomQ).optimal → atomP w

Irrelevant information does not block a presumption: normally p, q ⊩ presumably p (3.10(iii)).

theorem Veltman1996.ex310_independence (w : PQWorld) : w ∈ (((Veltman1996.σ₀✝.promote atomP).promote atomQ).assert fun (x : PQWorld) => ¬atomP x).optimal → atomQ w

Independence: normally p, normally q, ¬p ⊩ presumably q (3.10(iv)).

theorem Veltman1996.ex310_ambiguity : have σ := ((Veltman1996.σ₀✝.promote atomP).promote atomQ).assert fun (w : PQWorld) => ¬(atomP w ∧ atomQ w); (¬∀ w ∈ σ.optimal, atomP w) ∧ ¬∀ w ∈ σ.optimal, atomQ w

Ambiguity: normally p, normally q, ¬(p ∧ q) presumes neither p nor q (3.10(v)).

theorem Veltman1996.rain_or_snow : (¬∀ w ∈ ((Veltman1996.σ₀✝.promote atomP).assert fun (x : PQWorld) => ¬atomP x).optimal, atomQ w) ∧ ∀ w ∈ ((Veltman1996.σ₀✝.promote fun (w : PQWorld) => atomP w ∨ atomQ w).assert fun (x : PQWorld) => ¬atomP x).optimal, atomQ w

Normally it rains; it is not raining; so presumably it snows is invalid, but normally it rains or snows; it is not raining; so presumably it snows is valid (§3): a rule normally (p ∨ q) says what to expect when p fails.

theorem Veltman1996.normally_not_normally_or : ((Veltman1996.σ₀✝.promote atomP).promote fun (w : PQWorld) => atomP w ∨ atomQ w) ≠ Veltman1996.σ₀✝.promote atomP

Hence normally p ⊮ normally (p ∨ q): the second rule further refines the pattern.

Rules for exceptions (§4)

structure Veltman1996.Rule (W : Type u_2) : Type u_2

A restricted rule φ ⇝ ψ: default is a default in the domain domain.

• domain : Finset W
• default : Finset W

@[instance_reducible]

instance Veltman1996.instDecidableEqRule {W✝ : Type u_2} [DecidableEq W✝] : DecidableEq (Rule W✝)

Equations

• Veltman1996.instDecidableEqRule = Veltman1996.instDecidableEqRule.decEq

def Veltman1996.instDecidableEqRule.decEq {W✝ : Type u_2} [DecidableEq W✝] (x✝ x✝¹ : Rule W✝) : Decidable (x✝ = x✝¹)

Equations

• Veltman1996.instDecidableEqRule.decEq { domain := a, default := a_1 } { domain := b, default := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Veltman1996.Frame (W : Type u_2) : Type u_2

An expectation frame assigns to every domain d a pattern on d (Definition 4.2).

Equations

• Veltman1996.Frame W = ((d : Finset W) → Preorder ↥d)

@[reducible]

def Veltman1996.Frame.ofRules {W : Type u_1} (R : List (Rule W)) : Frame W

The frame presented by a list of rules: the pattern at d is the total pattern refined by the defaults of the rules with domain d (Proposition 4.14).

Equations

• Veltman1996.Frame.ofRules R d = Preorder.ofCriteria (fun (w : ↥d) (r : Veltman1996.Rule W) => ↑w ∈ r.default) {r : Veltman1996.Rule W | r ∈ R ∧ r.domain = d}

theorem Veltman1996.Frame.ofRules_cons_self {W : Type u_1} (r : Rule W) (R : List (Rule W)) : ofRules (r :: R) r.domain = Core.Order.Normality.refine (ofRules R r.domain) fun (w : ↥r.domain) => ↑w ∈ r.default

Refinement at the rule's own domain (Definition 4.5(ii)(b)): the pattern at r.domain is the old one refined with r.default.

theorem Veltman1996.Frame.ofRules_cons_of_ne {W : Type u_1} (r : Rule W) (R : List (Rule W)) {d : Finset W} (h : d ≠ r.domain) : ofRules (r :: R) d = ofRules R d

Other domains are untouched (Definition 4.5(ii)(a)).

def Veltman1996.Normal {W : Type u_1} (π : Frame W) (d : Finset W) (w : W) : Prop

w is normal in πd (Definition 4.3(i)): w ∈ d and w is at least as normal as every world of every subdomain of d containing it, under that subdomain's pattern.

Equations

• Veltman1996.Normal π d w = (w ∈ d ∧ ∀ d' ⊆ d, ∀ (hw : w ∈ d') (v : W) (hv : v ∈ d'), ⟨w, hw⟩ ≤ ⟨v, hv⟩)

theorem Veltman1996.normal_ofRules_iff {W : Type u_1} (R : List (Rule W)) (d : Finset W) (w : W) : Normal (Frame.ofRules R) d w ↔ w ∈ d ∧ ∀ r ∈ R, r.domain ⊆ d → w ∈ r.domain → ∀ v ∈ r.domain, v ∈ r.default → w ∈ r.default

In a presented frame, only the rules' own domains can disqualify a world.

theorem Veltman1996.Normal.mono {W : Type u_1} {π : Frame W} {d d' : Finset W} {w : W} (h : Normal π d w) (hw : w ∈ d') (hd : d' ⊆ d) : Normal π d' w

A world normal in a domain is normal in every subdomain containing it.

theorem Veltman1996.Normal.of_cons {W : Type u_1} {r : Rule W} {R : List (Rule W)} {d : Finset W} {w : W} (h : Normal (Frame.ofRules (r :: R)) d w) : Normal (Frame.ofRules R) d w

Accepting a rule can only remove normal worlds.

@[instance_reducible]

instance Veltman1996.instDecidableRelSubtypeMemFinsetLe_linglib {W : Type u_1} [DecidableEq W] (R : List (Rule W)) (d : Finset W) : DecidableRel LE.le

Equations

• Veltman1996.instDecidableRelSubtypeMemFinsetLe_linglib R d w v = decidable_of_iff (∀ r ∈ R, r.domain = d → ↑v ∈ r.default → ↑w ∈ r.default) ⋯

@[instance_reducible]

instance Veltman1996.instDecidablePredNormalOfRules {W : Type u_1} [DecidableEq W] (R : List (Rule W)) (d : Finset W) : DecidablePred (Normal (Frame.ofRules R) d)

Equations

• Veltman1996.instDecidablePredNormalOfRules R d w = decidable_of_iff (w ∈ d ∧ ∀ r ∈ R, r.domain ⊆ d → w ∈ r.domain → ∀ v ∈ r.domain, v ∈ r.default → w ∈ r.default) ⋯

def Veltman1996.normal {W : Type u_1} (π : Frame W) (d : Finset W) [DecidablePred (Normal π d)] : Finset W

The normal worlds nπd (Definition 4.3(ii)).

Equations

• Veltman1996.normal π d = Finset.filter (Veltman1996.Normal π d) d

def Veltman1996.Complies {W : Type u_1} (w : W) (D : List (Rule W)) : Prop

w complies with the defaults D (Definition 4.9(i)).

Equations

• Veltman1996.Complies w D = ∀ r ∈ D, w ∈ r.domain → w ∈ r.default

@[instance_reducible]

instance Veltman1996.instDecidableComplies {W : Type u_1} [DecidableEq W] (w : W) (D : List (Rule W)) : Decidable (Complies w D)

Equations

• Veltman1996.instDecidableComplies w D = Veltman1996.instDecidableComplies._aux_1 w D

def Veltman1996.IsDefault {W : Type u_1} [DecidableEq W] (π : Frame W) (d e : Finset W) : Prop

e is a default in πd (Definition 4.2(ii)): d ∩ e ≠ ∅ and πd ∘ e = πd, i.e. πd already respects e (Normality.refine_of_respects).

Equations

• Veltman1996.IsDefault π d e = ((d ∩ e).Nonempty ∧ Core.Order.Normality.respects (π d) fun (w : ↥d) => ↑w ∈ e)

theorem Veltman1996.isDefault_of_mem {W : Type u_1} [DecidableEq W] {R : List (Rule W)} {r : Rule W} (hr : r ∈ R) (hne : (r.domain ∩ r.default).Nonempty) : IsDefault (Frame.ofRules R) r.domain r.default

Every accepted rule with a nonempty domain-default intersection is a default of the presented frame.

theorem Veltman1996.conjConsequents {W : Type u_1} [DecidableEq W] {R : List (Rule W)} {φ ψ χ : Finset W} (hψ : { domain := φ, default := ψ } ∈ R) (hχ : { domain := φ, default := χ } ∈ R) : Frame.ofRules ({ domain := φ, default := ψ ∩ χ } :: R) = Frame.ofRules R

Conjunction of Consequents: once φ ⇝ ψ and φ ⇝ χ have been accepted, the pattern at ⟦φ⟧ respects ψ ∧ χ, so φ ⇝ (ψ ∧ χ) refines nothing.

def Veltman1996.Coherent {W : Type u_1} (π : Frame W) [(d : Finset W) → DecidablePred (Normal π d)] : Prop

A frame is coherent when every nonempty domain has a normal world (Definition 4.3(iii)).

Equations

• Veltman1996.Coherent π = ∀ (d : Finset W), d.Nonempty → (Veltman1996.normal π d).Nonempty

def Veltman1996.Applies {W : Type u_1} (π : Frame W) [(d : Finset W) → DecidablePred (Normal π d)] (D : List (Rule W)) (s : Finset W) : Prop

The defaults D jointly apply within s (Definition 4.9(ii)): every domain extending s has a normal world complying with them.

Equations

• Veltman1996.Applies π D s = ∀ (d : Finset W), s ⊆ d → ∃ w ∈ Veltman1996.normal π d, Veltman1996.Complies w D

theorem Veltman1996.coherent_cons_iff {W : Type u_1} [DecidableEq W] {R : List (Rule W)} (hR : Coherent (Frame.ofRules R)) {r : Rule W} (hne : (r.domain ∩ r.default).Nonempty) : Coherent (Frame.ofRules (r :: R)) ↔ Applies (Frame.ofRules R) [r] r.domain

Proposition 4.7: a coherent frame stays coherent under a new rule r with r.domain ∩ r.default ≠ ∅ iff r applies within its own domain — no domain extending r.domain has all its normal worlds in r.domain \ r.default.

theorem Veltman1996.weakenConsequent_applies {W : Type u_1} [DecidableEq W] {R : List (Rule W)} (hR : Coherent (Frame.ofRules R)) {φ ψ χ : Finset W} (hψ : { domain := φ, default := ψ } ∈ R) (hne : (φ ∩ ψ).Nonempty) : Applies (Frame.ofRules R) [{ domain := φ, default := ψ ∪ χ }] φ

Weakening the Consequent is "almost valid" (§5): a state that has accepted φ ⇝ ψ never crashes on φ ⇝ (ψ ∨ χ), since any normal world of a domain extending ⟦φ⟧ that lies in ⟦φ⟧ already satisfies ψ.

theorem Veltman1996.weakenConsequent_coherent {W : Type u_1} [DecidableEq W] {R : List (Rule W)} (hR : Coherent (Frame.ofRules R)) {φ ψ χ : Finset W} (hψ : { domain := φ, default := ψ } ∈ R) (hne : (φ ∩ ψ).Nonempty) : Coherent (Frame.ofRules ({ domain := φ, default := ψ ∪ χ } :: R))

@[instance_reducible]

instance Veltman1996.instDecidableEqFrameOfRules {W : Type u_1} [DecidableEq W] [Fintype W] (R R' : List (Rule W)) : Decidable (Frame.ofRules R = Frame.ofRules R')

Equations

• Veltman1996.instDecidableEqFrameOfRules R R' = decidable_of_iff (∀ (d : Finset W) (w v : ↥d), w ≤ v ↔ w ≤ v) ⋯

@[instance_reducible]

instance Veltman1996.instDecidableCoherent {W : Type u_1} [Fintype W] (π : Frame W) [(d : Finset W) → DecidablePred (Normal π d)] : Decidable (Coherent π)

Equations

• Veltman1996.instDecidableCoherent π = Veltman1996.instDecidableCoherent._aux_1 π

@[instance_reducible]

instance Veltman1996.instDecidableApplies {W : Type u_1} [DecidableEq W] [Fintype W] (π : Frame W) [(d : Finset W) → DecidablePred (Normal π d)] (D : List (Rule W)) (s : Finset W) : Decidable (Applies π D s)

Equations

• Veltman1996.instDecidableApplies π D s = Veltman1996.instDecidableApplies._aux_1 π D s

structure Veltman1996.State (W : Type u_2) : Type u_2

A state (π, s): the frame, presented by the accepted rules, and the agent's knowledge of the facts (Definition 4.4).

• rules : List (Rule W)
• info : Finset W

@[instance_reducible]

instance Veltman1996.instDecidableEqState {W✝ : Type u_2} [DecidableEq W✝] : DecidableEq (State W✝)

Equations

• Veltman1996.instDecidableEqState = Veltman1996.instDecidableEqState.decEq

def Veltman1996.instDecidableEqState.decEq {W✝ : Type u_2} [DecidableEq W✝] (x✝ x✝¹ : State W✝) : Decidable (x✝ = x✝¹)

Equations

• Veltman1996.instDecidableEqState.decEq { rules := a, info := a_1 } { rules := b, info := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Veltman1996.State.init {W : Type u_1} [Fintype W] : State W

The minimal state 0: the total frame, every world possible.

Equations

• Veltman1996.State.init = { rules := [], info := Finset.univ }

def Veltman1996.State.absurd {W : Type u_1} : State W

The absurd state 1.

Equations

• Veltman1996.State.absurd = { rules := [], info := ∅ }

@[reducible, inline]

abbrev Veltman1996.State.frame {W : Type u_1} (σ : State W) : Frame W

The frame of a state.

Equations

• σ.frame = Veltman1996.Frame.ofRules σ.rules

def Veltman1996.State.MaximalApplicable {W : Type u_1} [DecidableEq W] (σ : State W) (D : List (Rule W)) : Prop

D is a maximal applicable set of defaults in σ (Definition 4.13(i)), over the accepted rules (Proposition 4.14).

Equations

• σ.MaximalApplicable D = (Veltman1996.Applies σ.frame D σ.info ∧ ∀ r ∈ σ.rules, Veltman1996.Applies σ.frame (r :: D) σ.info → r ∈ D)

@[instance_reducible]

instance Veltman1996.State.instDecidableMaximalApplicable {W : Type u_1} [DecidableEq W] [Fintype W] (σ : State W) (D : List (Rule W)) : Decidable (σ.MaximalApplicable D)

Equations

• σ.instDecidableMaximalApplicable D = Veltman1996.State.instDecidableMaximalApplicable._aux_1 σ D

def Veltman1996.State.optimal {W : Type u_1} [DecidableEq W] [Fintype W] (σ : State W) : Finset W

The optimal worlds mσ (Definition 4.13(ii)): the worlds of s complying with a maximal applicable set of defaults.

Equations

• σ.optimal = {w ∈ σ.info | ∃ D ∈ σ.rules.sublists, σ.MaximalApplicable D ∧ Veltman1996.Complies w D}

def Veltman1996.State.Accepts {W : Type u_1} (σ : State W) (φ : State W → State W) : Prop

σ ⊩ φ: σ[φ] is σ — the same facts and the same frame.

Equations

• σ.Accepts φ = ((φ σ).info = σ.info ∧ (φ σ).frame = σ.frame)

@[instance_reducible]

instance Veltman1996.State.instDecidableAccepts {W : Type u_1} [DecidableEq W] [Fintype W] (σ : State W) (φ : State W → State W) : Decidable (σ.Accepts φ)

Equations

• σ.instDecidableAccepts φ = Veltman1996.State.instDecidableAccepts._aux_1 σ φ

def Veltman1996.rule {W : Type u_1} [DecidableEq W] [Fintype W] (φ ψ : Finset W) (σ : State W) : State W

σ[φ ⇝ ψ] (Definition 4.6): refine the frame at ⟦φ⟧ with ⟦ψ⟧, crashing if ⟦φ⟧ ∩ ⟦ψ⟧ = ∅ or the refined frame is incoherent.

Equations

• One or more equations did not get rendered due to their size.

def Veltman1996.normally {W : Type u_1} [DecidableEq W] [Fintype W] (ψ : Finset W) : State W → State W

Normally ψ is (ψ ∨ ¬ψ) ⇝ ψ (Definition 4.1).

Equations

• Veltman1996.normally ψ = Veltman1996.rule (ψ ∪ ψᶜ) ψ

def Veltman1996.fact {W : Type u_1} [DecidableEq W] (φ : Finset W) (σ : State W) : State W

σ[φ] for a factual φ: eliminate the ¬φ-worlds, crashing if none remain.

Equations

• Veltman1996.fact φ σ = if (σ.info ∩ φ).Nonempty then { rules := σ.rules, info := σ.info ∩ φ } else Veltman1996.State.absurd

def Veltman1996.presumably {W : Type u_1} [DecidableEq W] [Fintype W] (φ : Finset W) (σ : State W) : State W

σ[presumably φ] (Definition 4.13(iii)): a test passing iff φ holds in every optimal world.

Equations

• Veltman1996.presumably φ σ = if σ.optimal ⊆ φ then σ else Veltman1996.State.absurd

def Veltman1996.Valid {W : Type u_1} [Fintype W] (prems : List (State W → State W)) (concl : State W → State W) : Prop

Validity₁ (§1.2): the minimal state updated with the premises in order accepts the conclusion.

Equations

• Veltman1996.Valid prems concl = (List.foldl (fun (σ : Veltman1996.State W) (φ : Veltman1996.State W → Veltman1996.State W) => φ σ) Veltman1996.State.init prems).Accepts concl

@[instance_reducible]

instance Veltman1996.instDecidableValid {W : Type u_1} [DecidableEq W] [Fintype W] (prems : List (State W → State W)) (concl : State W → State W) : Decidable (Valid prems concl)

Equations

• Veltman1996.instDecidableValid prems concl = Veltman1996.instDecidableValid._aux_1 prems concl

theorem Veltman1996.rule_self {W : Type u_1} [DecidableEq W] [Fintype W] {φ : Finset W} (hφ : φ.Nonempty) : Valid [] (rule φ φ)

Conditional Identity: φ ⇝ φ is accepted in the minimal state for nonempty φ — the rule refines nothing.

Veltman's eight worlds

@[reducible, inline]

abbrev Veltman1996.World : Type

wᵢ is the set of atoms whose bits are set in i: w₀ = ∅, w₁ = {p}, w₂ = {q}, w₃ = {p, q}, w₄ = {r}, …, w₇ = {p, q, r}.

Equations

• Veltman1996.World = Fin 8

def Veltman1996.p : Finset World

Equations

• Veltman1996.p = {x : Veltman1996.World | ↑x % 2 = 1}

def Veltman1996.q : Finset World

Equations

• Veltman1996.q = {x : Veltman1996.World | ↑x / 2 % 2 = 1}

def Veltman1996.r : Finset World

Equations

• Veltman1996.r = {x : Veltman1996.World | ↑x / 4 % 2 = 1}

theorem Veltman1996.ex48 : rule q pᶜ (normally p State.init) ≠ State.absurd ∧ rule qᶜ pᶜ (rule q pᶜ (normally p State.init)) = State.absurd ∧ normally q (rule q pᶜ (normally p State.init)) = State.absurd

Examples 4.8(i)–(iii): an exception to normally p for q is acceptable, but not a further exception for ¬q (too many exceptions), nor normally q on top of it.

theorem Veltman1996.ex411_specificity : Valid [normally p, rule q pᶜ, fact q] (presumably pᶜ) ∧ Valid [normally p, rule q pᶜ, fact (q ∩ r)] (presumably pᶜ) ∧ Valid [normally p, rule q pᶜ, rule (q ∩ r) p, fact (q ∩ r)] (presumably p)

Examples 4.11(i)–(iii), the verdicts of §4: the more specific rule takes precedence, and an exception to an exception restores the general verdict.

theorem Veltman1996.ex411_iv : Valid [rule p r, rule q (p ∩ rᶜ), fact (p ∩ q)] (presumably rᶜ)

Example 4.11(iv): neither rule is more specific, yet in the context p ∧ q only q ⇝ (p ∧ ¬r) applies.

theorem Veltman1996.nixon : ¬Valid [rule p r, rule q rᶜ, fact (p ∩ q)] (presumably r) ∧ ¬Valid [rule p r, rule q rᶜ, fact (p ∩ q)] (presumably rᶜ)

Example 4.11(v), the Nixon diamond (§5): p ⇝ r, q ⇝ ¬r, p ∧ q presume neither r nor ¬r — the two defaults apply separately but not jointly.

theorem Veltman1996.ex411_vi : Valid [rule q p, rule p r, fact q] (presumably r)

Example 4.11(vi): q ⇝ p, p ⇝ r, q ⊩ presumably r — the defeasible Hypothetical Syllogism (§5's (*)).

Comparisons (§5)

theorem Veltman1996.students : Valid [rule p r, rule q rᶜ, rule q p, fact q] (presumably (p ∩ rᶜ))

Students are normally adults (q ⇝ p), students are normally not employed (q ⇝ ¬r), adults are normally employed (p ⇝ r): John, a student, is presumably an unemployed adult — q ⇝ ¬r overrides p ⇝ r in the presence of q ⇝ p.

theorem Veltman1996.independence : Valid [rule q p, rule q rᶜ, fact q, fact r] (presumably p)

Independence: an exception in one respect is not an exception in others — a student who is employed is still presumably an adult.

theorem Veltman1996.defeasibleModusTollens : Valid [rule p q, fact qᶜ] (presumably pᶜ)

Defeasible Modus Tollens is valid: p ⇝ q, ¬q ⊩ presumably ¬p.

theorem Veltman1996.modusPonens_over_modusTollens : Valid [rule p q, rule q pᶜ, fact p] (presumably q)

On the cyclic net p ⇝ q, q ⇝ ¬p, Modus Ponens takes precedence over Modus Tollens: p ⊩ presumably q.

theorem Veltman1996.substitution_fails : ¬Valid [rule q p, rule p qᶜ, fact q] (presumably qᶜ)

Validity₁ is not closed under substitution: (*) holds for independent predicates, but substituting ¬q for r defeats it.

theorem Veltman1996.hypotheticalSyllogism_fails : ¬Valid [rule q p, rule p r] (rule q r)

Hypothetical Syllogism fails although its defeasible version (*) holds: the rule q ⇝ r is not accepted.

theorem Veltman1996.contraposition_fails : ¬Valid [rule p q] (rule qᶜ pᶜ)

Defeasible Modus Tollens holds but Contraposition fails.

theorem Veltman1996.strengthening : Valid [rule p q, fact (p ∩ r)] (presumably q) ∧ ¬Valid [rule p q] (rule (p ∩ r) q)

p ⇝ q, p ∧ r ⊩ presumably q, but Strengthening the Antecedent fails.

theorem Veltman1996.nearValid : rule (p ∩ q) r (rule p r (rule p q State.init)) ≠ State.absurd ∧ ¬Valid [rule p q, rule p r] (rule (p ∩ q) r) ∧ rule (p ∪ q) r (rule q r (rule p r State.init)) ≠ State.absurd ∧ ¬Valid [rule p r, rule q r] (rule (p ∪ q) r)

Strengthening with a Consequent and Disjunction of Antecedents are almost valid: the derived rule never crashes the state, though it is not accepted.