Consequence in dynamic semantics

A dynamic meaning is an update of information states, and a state accepts a sentence when updating it with the sentence changes nothing, that is, when the state is a fixed point of the update. A text updates a state sentence by sentence. [Vel96] distinguishes three consequence relations between the premises of an argument and its conclusion: updating the minimal state with the premises yields a state that accepts the conclusion (his validity₁, EntailsFrom ⊤), updating any state does (validity₂, Entails), or every state that accepts each premise accepts the conclusion (validity₃, PreservesAcceptance), which is the shape of [Yal07]'s informational consequence.

An update is additive when it meets its input with the result of updating the minimal state, so that a static content fixes its dynamic meaning. The additive updates are exactly those satisfying Veltman's four constraints, Strengthening, Monotony, Idempotence and Persistence, which read in the reversed order make the update a principal closure operator. For additive updates the three consequence relations coincide, each saying that the contents of the premises jointly entail the content of the conclusion. In general they come apart: acceptance preservation is monotone in the premises and entailment is monotone on the left, while entailment from a fixed state is neither, but inserting a conclusion that it draws into the premises changes nothing, which gives Sequential Monotony and Sequential Cut.

On sets of possibilities the additive updates are the classical ones of Semantics/Dynamic/Update.lean, the static updates CCP.up, and entailment between static updates is inclusion of their contents. An update with an effect, such as a partial update, is a Kleisli arrow, and its extension along the monad's bind is an update of the kind treated here: a state accepts the arrow exactly when the arrow returns it unchanged.

Main definitions

• DynamicSemantics.text: the update of a state with a list of sentences, from the left.
• DynamicSemantics.EntailsFrom, DynamicSemantics.Entails, DynamicSemantics.PreservesAcceptance: the three consequence relations, with the scoped notation ψs ⊩₁ φ, ψs ⊩₂ φ and ψs ⊩₃ φ.
• DynamicSemantics.IsAdditive: the update meets its input with a fixed content.

Main results

• DynamicSemantics.isAdditive_iff: additivity is Strengthening, Monotony, Idempotence and Persistence together.
• DynamicSemantics.tfae_entails: for additive updates the three consequence relations coincide.
• DynamicSemantics.EntailsFrom.insert_iff: Sequential Monotony and Sequential Cut.
• DynamicSemantics.entailsFrom_append_self: under Idempotence entailment is reflexive.
• DynamicSemantics.isFixedPt_text_iff: along updates that never add possibilities, a state accepts a text exactly when it accepts each of its sentences.
• DynamicSemantics.CCP.isAdditive_iff_isClassical, DynamicSemantics.CCP.entails_up_iff: on sets of possibilities the additive updates are the classical ones, and entailment between static updates is inclusion.
• DynamicSemantics.Update.entails_image_test_iff: a relational update entails a test exactly when its outputs satisfy the test's condition.
• DynamicSemantics.isFixedPt_bind_pure_iff: acceptance of a Kleisli arrow.

Implementation notes

States are ordered by inclusion, as for DynamicSemantics.CCP and DynamicSemantics.ExpState: a more informed state lies lower, the minimal state is ⊤, and Strengthening says that an update never adds possibilities. Veltman orients the order the other way, with the minimal state 0 at the bottom and the sum of two states their join, and the content is the same; on Set the reversed orientation would make ⊥ the absurd state ∅ rather than the minimal one. Acceptance is Function.IsFixedPt, and a sentence is identified with its update.

References

• F. Veltman, Defaults in Update Semantics
• S. Yalcin, Epistemic Modals

Texts

def DynamicSemantics.text {α : Type u_1} (ψs : List (α → α)) (σ : α) : α

The update of σ with a text, σ[ψ₁]⋯[ψₙ], applying the sentences from the left.

Equations

• DynamicSemantics.text ψs σ = List.foldl (fun (σ : α) (ψ : α → α) => ψ σ) σ ψs

@[simp]

theorem DynamicSemantics.text_nil {α : Type u_1} (σ : α) : text [] σ = σ

@[simp]

theorem DynamicSemantics.text_cons {α : Type u_1} (ψ : α → α) (ψs : List (α → α)) (σ : α) : text (ψ :: ψs) σ = text ψs (ψ σ)

@[simp]

theorem DynamicSemantics.text_append {α : Type u_1} (ψs χs : List (α → α)) (σ : α) : text (ψs ++ χs) σ = text χs (text ψs σ)

Consequence

def DynamicSemantics.EntailsFrom {α : Type u_1} (σ : α) (ψs : List (α → α)) (φ : α → α) : Prop

ψs entails φ from σ when updating σ with ψs yields a state that accepts φ. Entailment from the minimal state is Veltman's validity₁.

Equations

• DynamicSemantics.EntailsFrom σ ψs φ = Function.IsFixedPt φ (DynamicSemantics.text ψs σ)

def DynamicSemantics.Entails {α : Type u_1} (ψs : List (α → α)) (φ : α → α) : Prop

ψs entails φ when updating any state with ψs yields a state that accepts φ, Veltman's validity₂.

Equations

• DynamicSemantics.Entails ψs φ = ∀ (σ : α), DynamicSemantics.EntailsFrom σ ψs φ

def DynamicSemantics.PreservesAcceptance {α : Type u_1} (ψs : List (α → α)) (φ : α → α) : Prop

Every state that accepts each of ψs accepts φ, Veltman's validity₃.

Equations

• DynamicSemantics.PreservesAcceptance ψs φ = ∀ (σ : α), (∀ ψ ∈ ψs, Function.IsFixedPt ψ σ) → Function.IsFixedPt φ σ

def DynamicSemantics.«term_⊩₁_» : Lean.TrailingParserDescr

ψs entails φ from σ when updating σ with ψs yields a state that accepts φ. Entailment from the minimal state is Veltman's validity₁.

Equations

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

def DynamicSemantics.«term_⊩₂_» : Lean.TrailingParserDescr

ψs entails φ when updating any state with ψs yields a state that accepts φ, Veltman's validity₂.

Equations

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

def DynamicSemantics.«term_⊩₃_» : Lean.TrailingParserDescr

Every state that accepts each of ψs accepts φ, Veltman's validity₃.

Equations

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

theorem DynamicSemantics.Entails.entailsFrom {α : Type u_1} {ψs : List (α → α)} {φ : α → α} (h : Entails ψs φ) (σ : α) : EntailsFrom σ ψs φ

theorem DynamicSemantics.entails_singleton_iff {α : Type u_1} {φ f : α → α} : Entails [f] φ ↔ φ ∘ f = f

A single premise entails φ exactly when φ absorbs it.

theorem DynamicSemantics.Entails.trans {α : Type u_1} {φ f g : α → α} (h₁ : Entails [f] g) (h₂ : Entails [g] φ) : Entails [f] φ

Entailment between single premises is transitive.

theorem DynamicSemantics.preservesAcceptance_iff {α : Type u_1} {ψs : List (α → α)} {φ : α → α} : PreservesAcceptance ψs φ ↔ ⋂ ψ ∈ ψs, Function.fixedPoints ψ ⊆ Function.fixedPoints φ

theorem DynamicSemantics.PreservesAcceptance.mono {α : Type u_1} {ψs χs : List (α → α)} {φ : α → α} (h : PreservesAcceptance ψs φ) (hsub : ψs ⊆ χs) : PreservesAcceptance χs φ

Acceptance preservation is monotone: adding premises preserves it.

theorem DynamicSemantics.Entails.append_left {α : Type u_1} {ψs : List (α → α)} {φ : α → α} (h : Entails ψs φ) (χs : List (α → α)) : Entails (χs ++ ψs) φ

Entailment is left monotone: adding premises in front preserves it.

theorem DynamicSemantics.EntailsFrom.insert_iff {α : Type u_1} {σ : α} {ψs : List (α → α)} {φ : α → α} (h : EntailsFrom σ ψs φ) {θs : List (α → α)} {χ : α → α} : EntailsFrom σ (ψs ++ φ :: θs) χ ↔ EntailsFrom σ (ψs ++ θs) χ

Inserting a conclusion drawn from σ right after its premises changes nothing. From right to left this is Sequential Monotony, and from left to right Sequential Cut.

theorem DynamicSemantics.entailsFrom_append_self {α : Type u_1} {σ : α} {ψs : List (α → α)} {φ : α → α} (hφ : ∀ (σ : α), Function.IsFixedPt φ (φ σ)) : EntailsFrom σ (ψs ++ [φ]) φ

Under Idempotence entailment is reflexive: a sentence follows from any premises ending in it.

Texts of eliminative updates

theorem DynamicSemantics.text_le {α : Type u_1} [PartialOrder α] {ψs : List (α → α)} (h : ∀ ψ ∈ ψs, ∀ (σ : α), ψ σ ≤ σ) (σ : α) : text ψs σ ≤ σ

theorem DynamicSemantics.isFixedPt_text_iff {α : Type u_1} [PartialOrder α] {ψs : List (α → α)} (h : ∀ ψ ∈ ψs, ∀ (σ : α), ψ σ ≤ σ) {σ : α} : Function.IsFixedPt (text ψs) σ ↔ ∀ ψ ∈ ψs, Function.IsFixedPt ψ σ

Along updates that never add possibilities, a state accepts a text exactly when it accepts each of its sentences.

Additive updates

def DynamicSemantics.IsAdditive {α : Type u_1} [SemilatticeInf α] [OrderTop α] (f : α → α) : Prop

An update is additive when it meets its input with the update of the minimal state, so that a static content determines it.

Equations

• DynamicSemantics.IsAdditive f = ∀ (σ : α), f σ = σ ⊓ f ⊤

theorem DynamicSemantics.IsAdditive.le {α : Type u_1} [SemilatticeInf α] [OrderTop α] {f : α → α} (hf : IsAdditive f) (σ : α) : f σ ≤ σ

theorem DynamicSemantics.IsAdditive.isFixedPt_iff {α : Type u_1} [SemilatticeInf α] [OrderTop α] {f : α → α} {σ : α} (hf : IsAdditive f) : Function.IsFixedPt f σ ↔ σ ≤ f ⊤

A state accepts an additive update exactly when it lies below the update's content.

theorem DynamicSemantics.isAdditive_id {α : Type u_1} [SemilatticeInf α] [OrderTop α] : IsAdditive id

theorem DynamicSemantics.isAdditive_inf_right {α : Type u_1} [SemilatticeInf α] [OrderTop α] (a : α) : IsAdditive fun (x : α) => x ⊓ a

Meeting with a fixed content is additive.

theorem DynamicSemantics.IsAdditive.comp {α : Type u_1} [SemilatticeInf α] [OrderTop α] {f g : α → α} (hg : IsAdditive g) (hf : IsAdditive f) : IsAdditive (g ∘ f)

theorem DynamicSemantics.isAdditive_text {α : Type u_1} [SemilatticeInf α] [OrderTop α] {ψs : List (α → α)} (h : ∀ ψ ∈ ψs, IsAdditive ψ) : IsAdditive (text ψs)

A text of additive updates is additive.

theorem DynamicSemantics.isAdditive_iff {α : Type u_1} [SemilatticeInf α] [OrderTop α] {f : α → α} : IsAdditive f ↔ (∀ (σ : α), f σ ≤ σ) ∧ Monotone f ∧ (∀ (σ : α), Function.IsFixedPt f (f σ)) ∧ IsLowerSet (Function.fixedPoints f)

An update is additive exactly when it satisfies Strengthening, never adding possibilities, Monotony, Idempotence, and Persistence, the states that accept it being closed downward. The four constraints make the update a closure operator on the reversed order whose closed elements form an upper set, and such an operator is principal.

theorem DynamicSemantics.tfae_entails {α : Type u_1} [SemilatticeInf α] [OrderTop α] {φ : α → α} {ψs : List (α → α)} (hψs : ∀ ψ ∈ ψs, IsAdditive ψ) (hφ : IsAdditive φ) : [EntailsFrom ⊤ ψs φ, Entails ψs φ, PreservesAcceptance ψs φ].TFAE

For additive updates the three consequence relations coincide.

Updates with effects

theorem DynamicSemantics.isFixedPt_bind_pure_iff {α : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {φ : α → m α} {σ : α} : Function.IsFixedPt (fun (x : m α) => x >>= φ) (pure σ) ↔ φ σ = pure σ

A state accepts a Kleisli arrow, read as an update through the monad's bind, exactly when the arrow returns it unchanged.

Sets of possibilities

theorem DynamicSemantics.CCP.isAdditive_up {S : Type u_2} (c : Set S) : IsAdditive (up c)

The static update with a content is additive.

theorem DynamicSemantics.CCP.isFixedPt_up_iff {S : Type u_2} {c s : Set S} : Function.IsFixedPt (up c) s ↔ s ⊆ c

A state accepts a static update exactly when it lies inside the content.

theorem DynamicSemantics.CCP.isAdditive_iff_isClassical {S : Type u_2} {u : CCP S} : IsAdditive u ↔ u.IsClassical

On sets of possibilities the additive updates are the classical ones, eliminative and distributive.

theorem DynamicSemantics.CCP.entails_up_iff {S : Type u_2} {c d : Set S} : Entails [up c] (up d) ↔ c ⊆ d

Entailment between static updates is inclusion of their contents.

theorem DynamicSemantics.Update.entails_image_test_iff {S : Type u_2} (R : Update S) (C : Condition S) : Entails [SetRel.image R] (SetRel.image (test C)) ↔ SetRel.cod R ⊆ C

A relational update entails a test exactly when its outputs satisfy the test's condition.