Veltman (1996): Defaults in Update Semantics

This file formalizes the paper of Veltman, which treats normally φ as an update of an agent's expectations rather than a sentence about them. The framework of section 1, acceptance as a fixed point of the update, the three notions of validity and additivity, with Propositions 1.2 and 1.3, is Semantics/Dynamic/Consequence.lean.

Section 2 studies might on sets of worlds, whose updates of Definition 2.3 are CCP.up, CCP.neg and CCP.might. The test might φ satisfies Strengthening, Idempotence and Monotony, Lemma 2.8, might_le, might_idem and might_monotone, but not Persistence, so the system is not additive, not_isLowerSet_might and not_isAdditive_might. Examples 2.7 show that consistency depends on the order of the text, consistent_might_neg and not_consistent_up_might_neg, and that validity₁ is neither right nor left monotone. On the fragment without might validity is classical, valid₁_up_iff.

A state of section 3 pairs an expectation pattern, a preorder on worlds, with the agent's knowledge of the facts; normally φ refines the pattern in favour of the φ-worlds and presumably φ tests whether φ holds in the optimal worlds. That system is DynamicSemantics.ExpState, and Examples 3.10 are stated here as verdicts of validity₁ on the paper's four worlds, together with the rain-or-snow contrast by which normally (p ∨ q) is stronger than normally p, rain_or_snow and normally_not_normally_or. Rules and facts are additive, so a rule that follows under validity₁ follows under validity₃ as well, ex310_rule_persists_valid₃, while the default inference normally p ⊩ presumably p is valid₁ but neither valid₂ nor valid₃, not_valid₂_presumably and not_valid₃_presumably, which is why Veltman concentrates on validity₁.

Section 4 adds the restricted rules if φ, then normally ψ. An expectation frame assigns a pattern to every domain of worlds, Definition 4.2, Frame; a world is normal in a domain when it is top-ranked in every subdomain containing it, Definition 4.3, Normal; a frame is coherent when every nonempty domain has a normal world, Coherent; accepting a rule refines the pattern at the rule's domain and crashes when the result is incoherent, Definitions 4.5 and 4.6, rule; and a set of defaults applies within the agent's information when every domain extending it has a normal world complying with them, Definition 4.9, Applies. The optimal worlds comply with a maximal applicable set of defaults, Definition 4.13, State.optimal, computed over the accepted rules by Proposition 4.14. Validity is validity₁, Valid. Proved in general are the refinement clause of Definition 4.5, Frame.ofRules_cons_self and Frame.ofRules_cons_of_ne, Proposition 4.7, coherent acceptance being applicability of the new rule within its own domain, coherent_cons_iff, Conditional Identity and Conjunction of Consequents, rule_self and conjConsequents, and the section 5 observation that Weakening the Consequent never crashes a state, weakenConsequent_coherent. Checked on the paper's eight worlds are Examples 4.8 and 4.11, the Nixon diamond, the student who is presumably an unemployed adult, Independence, defeasible Modus Tollens, Modus Ponens over Modus Tollens on a cyclic net, the failure of Hypothetical Syllogism, Contraposition and Strengthening the Antecedent beside their defeasible versions, and the near-validity of Strengthening with a Consequent and Disjunction of Antecedents.

Implementation notes

The update with normally φ of DynamicSemantics.ExpState does not crash, so the second clause of Example 3.10(i) is stated as the failure of the acceptability condition, ex310_conflict.

Every frame an agent reaches from the minimal state is the total frame refined by the rules it has accepted, so a frame of section 4 is presented by its list of rules, Frame.ofRules, which makes coherence, normality, applicability and the optimal worlds decidable and lets each verdict be checked by decide over the atoms p, q and r. Acceptance then compares the facts and the frames of two states rather than their presentations, so Valid is DynamicSemantics.EntailsFrom ⊤ read up to presentation. The comparison with the default logics of Asher and Morreau in section 5 is discussed in the paper and not formalized.

References

• F. Veltman, Defaults in Update Semantics (1996)
• N. Asher and M. Morreau, Commonsense Entailment: A Modal Theory of Nonmonotonic Reasoning (1991)

Might (§2)

theorem Veltman1996.might_le {W : Type u_1} (φ : DynamicSemantics.CCP W) (σ : Set W) : φ.might σ ⊆ σ

The test might φ never adds possibilities (Lemma 2.8(i)).

theorem Veltman1996.might_idem {W : Type u_1} (φ : DynamicSemantics.CCP W) (σ : Set W) : Function.IsFixedPt φ.might (φ.might σ)

The test might φ is idempotent (Lemma 2.8(ii)).

theorem Veltman1996.might_monotone {W : Type u_1} {φ : DynamicSemantics.CCP W} (hφ : Monotone φ) : Monotone φ.might

The test might φ is monotone when φ is (Lemma 2.8(iii)).

def Veltman1996.Consistent {W : Type u_1} (ψs : List (DynamicSemantics.CCP W)) : Prop

A text is consistent when updating some state with it does not yield the absurd state (Definition 2.4).

Equations

• Veltman1996.Consistent ψs = ∃ (σ : Set W), (List.foldl (fun (σ : Set W) (ψ : DynamicSemantics.CCP W) => ψ σ) σ ψs).Nonempty

theorem Veltman1996.consistent_might_neg {W : Type u_1} {c : Set W} (hc : c.Nonempty) (hc' : cᶜ.Nonempty) : Consistent [(DynamicSemantics.CCP.up c).neg.might, DynamicSemantics.CCP.up c]

Might ¬p, p is consistent, but p, might ¬p is not (Example 2.7(i)).

theorem Veltman1996.not_consistent_up_might_neg {W : Type u_1} {c : Set W} : ¬Consistent [DynamicSemantics.CCP.up c, (DynamicSemantics.CCP.up c).neg.might]

theorem Veltman1996.valid₁_might_neg {W : Type u_1} {c : Set W} : DynamicSemantics.EntailsFrom ⊤ [(DynamicSemantics.CCP.up c).neg.might] (DynamicSemantics.CCP.up c).neg.might

Right monotonicity fails: might ¬p ⊩ might ¬p, but might ¬p, p ⊮ might ¬p (Example 2.7(ii)).

theorem Veltman1996.not_valid₁_might_neg_up {W : Type u_1} {c : Set W} (hc : c.Nonempty) (hc' : cᶜ.Nonempty) : ¬DynamicSemantics.EntailsFrom ⊤ [(DynamicSemantics.CCP.up c).neg.might, DynamicSemantics.CCP.up c] (DynamicSemantics.CCP.up c).neg.might

theorem Veltman1996.valid₁_might {W : Type u_1} {c : Set W} (hc : c.Nonempty) : DynamicSemantics.EntailsFrom ⊤ [] (DynamicSemantics.CCP.up c).might

Left monotonicity fails: ⊩ might p, but ¬p ⊮ might p (Example 2.7(iii)).

theorem Veltman1996.not_valid₁_neg_might {W : Type u_1} {c : Set W} (hc : cᶜ.Nonempty) : ¬DynamicSemantics.EntailsFrom ⊤ [(DynamicSemantics.CCP.up c).neg] (DynamicSemantics.CCP.up c).might

theorem Veltman1996.not_isLowerSet_might {W : Type u_1} {c : Set W} (hc : c.Nonempty) (hc' : cᶜ.Nonempty) : ¬IsLowerSet (Function.fixedPoints (DynamicSemantics.CCP.up c).might)

Might p is not persistent: the minimal state accepts it, but the more informed state that has learnt ¬p does not (§2).

theorem Veltman1996.not_isAdditive_might {W : Type u_1} {c : Set W} (hc : c.Nonempty) (hc' : cᶜ.Nonempty) : ¬DynamicSemantics.IsAdditive (DynamicSemantics.CCP.up c).might

So might p is not additive, although it satisfies Strengthening, Idempotence and Monotony (§2).

theorem Veltman1996.valid₁_up_iff {W : Type u_1} {d : Set W} {cs : List (Set W)} : DynamicSemantics.EntailsFrom ⊤ (List.map DynamicSemantics.CCP.up cs) (DynamicSemantics.CCP.up d) ↔ ∀ (w : W), (∀ c ∈ cs, w ∈ c) → w ∈ d

On the fragment without might validity is classical: the conclusion holds at every world at which all the premises hold (§2).

Rules with exceptions (§3)

inductive Veltman1996.PQWorld : Type

The four worlds over the atoms p and q are w₀ = ∅, w₁ = {p}, w₂ = {q} and 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

def Veltman1996.σ₀ : DynamicSemantics.ExpState PQWorld

The minimal state 0.

Equations

• Veltman1996.σ₀ = DynamicSemantics.ExpState.init

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

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

theorem Veltman1996.ex310_conflict : ¬∃ w ∈ (σ₀.promote atomP).order.minimals Set.univ, ¬atomP w

The opposite rule is then unacceptable, since no normal world of 0[normally p] is a ¬p-world (3.10(i)). The update with normally does not crash here, so this is the acceptability condition rather than the crash.

theorem Veltman1996.ex310_presumably : DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP] (DynamicSemantics.ExpState.presumablyTest atomP)

Normally p ⊩ presumably p (3.10(ii)).

theorem Veltman1996.not_valid₂_presumably : ¬DynamicSemantics.Entails [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP] (DynamicSemantics.ExpState.presumablyTest atomP)

The default inference normally p ⊩ presumably p is not valid₂, since a state may already know that p fails, and Veltman concentrates on validity₁ for this reason (§1.3).

theorem Veltman1996.not_valid₃_presumably : ¬DynamicSemantics.PreservesAcceptance [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP] (DynamicSemantics.ExpState.presumablyTest atomP)

Nor is it valid₃: a state that knows ¬p accepts normally p without presuming p.

theorem Veltman1996.ex310_defeat : ¬DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] (DynamicSemantics.ExpState.presumablyTest atomP)

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

theorem Veltman1996.ex310_rule_persists : DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP

Exceptions do not defeat the rule, normally p, ¬p ⊩ normally p (3.10(ii)).

theorem Veltman1996.ex310_rule_persists_valid₃ : DynamicSemantics.PreservesAcceptance [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP

Rules and facts are additive, so the persistence of the rule holds under every notion of validity (Proposition 1.3), unlike the presumption.

theorem Veltman1996.ex310_irrelevant : DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert atomQ] (DynamicSemantics.ExpState.presumablyTest atomP)

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

theorem Veltman1996.ex310_contrary : ¬DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert atomQ, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] (DynamicSemantics.ExpState.presumablyTest atomP)

Information to the contrary does, normally p, q, ¬p ⊮ presumably p (3.10(iii)).

theorem Veltman1996.ex310_two_rules : DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomQ] (DynamicSemantics.ExpState.presumablyTest atomP)

Two rules each yield their presumption, normally p, normally q ⊩ presumably p (3.10(iv)).

theorem Veltman1996.ex310_two_rules_defeat : ¬DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomQ, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] (DynamicSemantics.ExpState.presumablyTest atomP)

An exception to one rule defeats its presumption, normally p, normally q, ¬p ⊮ presumably p (3.10(iv)).

theorem Veltman1996.ex310_independence : DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomQ, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] (DynamicSemantics.ExpState.presumablyTest atomQ)

But not the other rule's, since two rules are independent, normally p, normally q, ¬p ⊩ presumably q (3.10(iv)).

theorem Veltman1996.ex310_ambiguity : have ψs := [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomQ, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (w : PQWorld) => ¬(atomP w ∧ atomQ w)]; ¬DynamicSemantics.EntailsFrom ⊤ ψs (DynamicSemantics.ExpState.presumablyTest atomP) ∧ ¬DynamicSemantics.EntailsFrom ⊤ ψs (DynamicSemantics.ExpState.presumablyTest atomQ)

The state normally p, normally q, ¬(p ∧ q) is ambiguous and presumes neither p nor q (3.10(v)).

theorem Veltman1996.rain_or_snow : ¬DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] (DynamicSemantics.ExpState.presumablyTest atomQ) ∧ DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote fun (w : PQWorld) => atomP w ∨ atomQ w, fun (x : DynamicSemantics.ExpState PQWorld) => x.assert fun (x : PQWorld) => ¬atomP x] (DynamicSemantics.ExpState.presumablyTest atomQ)

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), because a rule normally (p ∨ q) says what to expect when p fails.

theorem Veltman1996.normally_not_normally_or : ¬DynamicSemantics.EntailsFrom ⊤ [fun (x : DynamicSemantics.ExpState PQWorld) => x.promote atomP] fun (x : DynamicSemantics.ExpState PQWorld) => x.promote fun (w : PQWorld) => atomP w ∨ atomQ w

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

Rules for exceptions (§4)

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

A restricted rule φ ⇝ ψ makes default 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 assigns to d 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 = DynamicSemantics.ExpState.refine (ofRules R r.domain) fun (w : ↥r.domain) => ↑w ∈ r.default

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

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)).

theorem Veltman1996.Frame.ofRules_perm {W : Type u_1} {R R' : List (Rule W)} (h : R.Perm R') : ofRules R = ofRules R'

The presented frame depends only on which rules have been accepted, not on their order.

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

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

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_studies {W : Type u_1} [DecidableEq W] (R : List (Rule W)) (d : Finset W) : DecidableRel LE.le

Equations

• Veltman1996.instDecidableRelSubtypeMemFinsetLe_studies 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

A proposition e is a default in πd when d ∩ e ≠ ∅ and πd ∘ e = πd, that is, when πd already respects e (Definition 4.2(ii)).

Equations

• Veltman1996.IsDefault π d e = ((d ∩ e).Nonempty ∧ DynamicSemantics.ExpState.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 holds, since 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 when every domain extending s has a normal world complying with them (Definition 4.9(ii)).

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

A coherent frame stays coherent under a new rule r with r.domain ∩ r.default ≠ ∅ iff r applies within its own domain, which means that no domain extending r.domain has all its normal worlds in r.domain \ r.default (Proposition 4.7).

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 π = { decide := decide (∀ a ∈ Finset.univ, (fun (d : Finset W) => d.Nonempty → (Veltman1996.normal π d).Nonempty) a), reflects_decide := ⋯ }

@[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

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

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

A state (π, s) consists of 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 has the total frame and 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

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

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

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

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

The state σ accepts φ, written σ ⊩ φ, when σ[φ] has the same facts and the same frame as σ.

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

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

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

The update σ[φ ⇝ ψ] refines the frame at ⟦φ⟧ with ⟦ψ⟧, and crashes if ⟦φ⟧ ∩ ⟦ψ⟧ = ∅ or the refined frame is incoherent (Definition 4.6).

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

The update σ[φ] for a factual φ eliminates the ¬φ-worlds, and crashes 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

The update σ[presumably φ] is a test that passes iff φ holds in every optimal world (Definition 4.13(iii)).

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

An argument is valid₁ when the minimal state updated with the premises in order accepts the conclusion (§1.2).

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

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

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

Conditional Identity holds, since φ ⇝ φ refines nothing and is accepted in the minimal state for nonempty φ.

Veltman's eight worlds

@[reducible, inline]

abbrev Veltman1996.World : Type

The world wᵢ is the set of atoms whose bits are set in i, so 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

An exception to normally p for q is acceptable, but a further exception for ¬q is not, being one exception too many, and neither is normally q on top of it (Examples 4.8(i)–(iii)).

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)

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

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

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

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ᶜ)

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

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

The defeasible Hypothetical Syllogism holds, q ⇝ p, p ⇝ r, q ⊩ presumably r (Example 4.11(vi), the (*) of §5).

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), and adults are normally employed (p ⇝ r). John, a student, is presumably an unemployed adult, since 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)

An exception in one respect is not an exception in others, so 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, since (*) 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, since 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, since the derived rule never crashes the state, though it is not accepted.