Documentation

Linglib.Theories.Semantics.Composition.MaybeMonad

The Maybe Monad: Presupposition as Scope #

@cite{grove-2022}

@cite{grove-2022} argues that presupposition projection is a scope phenomenon. The key insight: presupposition triggers denote values of type α_# (= Option α), and they interact with their semantic context by taking scope via monadic bind (Option.bind), exactly paralleling @cite{charlow-2020}'s treatment of indefinites with the set monad.

The Maybe monad (Option, some, bind) is the presuppositional analog of @cite{charlow-2020}'s set monad (S, η, ⫝̸) for alternatives. Where S gives scope to alternative-denoting expressions, Option gives scope to presupposition triggers. Both derive exceptional scope from ASSOCIATIVITY.

Organization #

§1 Connectives on Option Bool: material conditional (middle Kleene), conjunction/disjunction (weak Kleene)
§2 The intensional-presuppositional monad Iₚ (= ReaderT i Option)
§3 Monad laws for Iₚ
§4 Semantic operations: evaluation (·)^ž, presuppositional universal ∀ₚ
§5 Attitude verb semantics: believe via doxastic accessibility
§6 Bridge: Option Bool ↔ Truth3 ↔ PrProp

The Maybe Monad as Presupposition #

Option is already a LawfulMonad in Lean. Grove's operators are:

Grove notation	Lean	Type
`η_#`	`some`	`α → Option α`
`⋆_#`	`Option.bind`	`Option α → (α → Option β) → Option β`
`#`	`none`	`Option α`

The monad laws (Left Identity, Right Identity, Associativity from Figure 7) hold definitionally.

Parallel with the Set Monad #

	Alternatives (@cite{charlow-2020})	Presupposition (@cite{grove-2022})
Monad	`S α = α → Prop` (sets)	`Option α` (maybe)
Unit	`η_S(x) = {x}`	`η_#(v) = some v`
Bind	`m ⫝̸_S f = ⋃_{x∈m} f(x)`	`v ⋆_# k = k(v); # ⋆_# k = #`
Effect	Indeterminacy	Partiality
Scope	Indefinites escape islands	Presuppositions project past filters

§1 Connectives on `Option Bool` #

Grove uses two distinct gap-propagation policies:

Middle Kleene for the material conditional ⇒: left-undefined absorbs, but right-undefined does NOT absorb when the left is false (⊥ ⇒ # = ⊤).
Weak Kleene for ∀_#: undefinedness absorbs from either side (⊥ ∧ # = #, unlike Strong Kleene where ⊥ ∧ # = ⊥).

def Semantics.Composition.MaybeMonad.materialCond :

Option Bool → Option Bool → Option Bool

Material conditional ⇒ with middle Kleene semantics (Grove eq. 16).

⊤ ⇒ ψ = ψ, ⊥ ⇒ ψ = ⊤, # ⇒ ψ = #.

The conditional is true when its antecedent is false (regardless of the consequent's definedness), and propagates the consequent when the antecedent is true. Undefinedness in the antecedent absorbs.

Equations

Semantics.Composition.MaybeMonad.materialCond none x✝ = none
Semantics.Composition.MaybeMonad.materialCond (some false) x✝ = some true
Semantics.Composition.MaybeMonad.materialCond (some true) x✝ = x✝

Instances For

def Semantics.Composition.MaybeMonad.meetWK :

Option Bool → Option Bool → Option Bool

Weak Kleene conjunction (used by ∀ₚ).

Undefinedness absorbs from either side, then falsity absorbs. In contrast, Strong Kleene has ⊥ ∧ # = ⊥, while Weak Kleene has ⊥ ∧ # = #.

Equations

Instances For

def Semantics.Composition.MaybeMonad.joinWK :

Option Bool → Option Bool → Option Bool

Weak Kleene disjunction. Dual of meetWK.

Equations

Instances For

def Semantics.Composition.MaybeMonad.negP :

Option Bool → Option Bool

Negation preserves definedness.

Equations

Instances For

theorem Semantics.Composition.MaybeMonad.materialCond_false_absorbs (ψ : Option Bool) :

materialCond (some false) ψ = some true

theorem Semantics.Composition.MaybeMonad.materialCond_true_passes (ψ : Option Bool) :

materialCond (some true) ψ = ψ

theorem Semantics.Composition.MaybeMonad.materialCond_undef_absorbs (ψ : Option Bool) :

materialCond none ψ = none

theorem Semantics.Composition.MaybeMonad.meetWK_comm (a b : Option Bool) :

meetWK a b = meetWK b a

§2 The monad `Iₚ` #

Iₚ I α = I → Option α: the Reader monad transformer applied to the Maybe monad. An expression of type Iₚ I α reads an index (world, world-assignment pair, etc.) and returns a possibly-undefined value.

This monad treats intensionality and presupposition uniformly (Grove §4.1): Iₚ is obtained by replacing t with t_# in standard intensional types (i → t becomes i → t_#).

@[reducible, inline]

abbrev Semantics.Composition.MaybeMonad.Iₚ (I α : Type) :

Iₚ I α: the intensional-presuppositional monad.

An expression of type Iₚ I α reads an index i and returns some v if defined at i, or none if presupposition failure occurs at i.

Equations

Semantics.Composition.MaybeMonad.Iₚ I α = (I → Option α)

Instances For

def Semantics.Composition.MaybeMonad.ηI {I α : Type} (v : α) :

Iₚ I α

ηI: unit for Iₚ. Makes a value trivially index-sensitive (ignores the index, always defined). Grove eq. 19, first line.

Equations

Semantics.Composition.MaybeMonad.ηI v x✝ = some v

Instances For

def Semantics.Composition.MaybeMonad.bindI {I α β : Type} (m : Iₚ I α) (k : α → Iₚ I β) :

Iₚ I β

bindI: bind for Iₚ. Evaluates m at index i; if defined, feeds the result to k at the same index. Grove eq. 19, second line.

Equations

Semantics.Composition.MaybeMonad.bindI m k i = do let v ← m i k v i

Instances For

§3 Monad laws #

The three laws from Figure 7 hold for Iₚ. Left Identity and Associativity are the key properties for scope-taking: Left Identity ensures that η + ⋆ = reconstruction (no scope), and Associativity ensures that cyclic scope-taking (roll-up pied-piping) works.

theorem Semantics.Composition.MaybeMonad.left_identity {I α β : Type} (v : α) (k : α → Iₚ I β) :

bindI (ηI v) k = k v

Left Identity: lifting a value into the monad and immediately binding is the same as applying the continuation directly.

This is why global scope for a presupposition trigger that has been locally η-shifted reconstructs to the local meaning (Grove fn. 13).

theorem Semantics.Composition.MaybeMonad.right_identity {I α : Type} (m : Iₚ I α) :

bindI m ηI = m

Right Identity: binding with ηI is a no-op.

theorem Semantics.Composition.MaybeMonad.assoc {I α β γ : Type} (m : Iₚ I α) (f : α → Iₚ I β) (g : β → Iₚ I γ) :

bindI (bindI m f) g = bindI m fun (x : α) => bindI (f x) g

Associativity: sequential scope-taking = direct wide scope.

This is the presuppositional analog of @cite{charlow-2020}'s ASSOCIATIVITY theorem for the set monad. It guarantees that roll-up pied-piping (taking scope at an island edge, then further) yields the same result as direct scope-taking.

theorem Semantics.Composition.MaybeMonad.backward_compat {I α β : Type} (f : α → β) (v : α) :

(bindI (ηI v) fun (x : α) => ηI (f x)) = ηI (f v)

Backward compatibility: non-presuppositional expressions (those wrapped in some) compose the same way they do without the monad. This means traditional satisfaction-theoretic analyses that use only defined values are preserved inside the monadic setting (Grove §5).

§4 Evaluation and presuppositional universal #

The evaluation function evalI (Grove's (·)^ž) converts an intension that may be undefined into an intensional truth value that may be undefined, by feeding the index to itself. The presuppositional universal forallP (Grove's ∀_#) quantifies over a domain with weak-Kleene semantics.

def Semantics.Composition.MaybeMonad.evalI {I : Type} (φ : Iₚ I (I → Bool)) :

Evaluation function (·)^ž (Grove eq. 20).

Given φ : Iₚ I (I → Bool) (a proposition that reads an index, possibly undefined, to return an intension), evalI φ feeds the index to itself: evalI φ i = (φ i).map (· i).

Equations

Semantics.Composition.MaybeMonad.evalI φ i = Option.map (fun (x : I → Bool) => x i) (φ i)

Instances For

def Semantics.Composition.MaybeMonad.forallP {α : Type} (xs : List α) (φ : α → Option Bool) :

Presuppositional universal ∀_# (Grove eq. 27).

Uses weak Kleene semantics: none absorbs (if the scope is undefined at any value, the whole universal is undefined).

Equations

Semantics.Composition.MaybeMonad.forallP xs φ = List.foldl (fun (acc : Option Bool) (x : α) => Semantics.Composition.MaybeMonad.meetWK acc (φ x)) (some true) xs

Instances For

def Semantics.Composition.MaybeMonad.existsP {α : Type} (xs : List α) (φ : α → Option Bool) :

Presuppositional existential (dual of forallP).

Equations

Semantics.Composition.MaybeMonad.existsP xs φ = List.foldl (fun (acc : Option Bool) (x : α) => Semantics.Composition.MaybeMonad.joinWK acc (φ x)) (some false) xs

Instances For

theorem Semantics.Composition.MaybeMonad.forallP_all_true {α : Type} (xs : List α) (φ : α → Option Bool) (h : ∀ x ∈ xs, φ x = some true) :

forallP xs φ = some true

forallP on an all-true list is some true.

theorem Semantics.Composition.MaybeMonad.forallP_undef {α : Type} (xs : List α) (φ : α → Option Bool) (x : α) (hx : x ∈ xs) (hu : φ x = none) :

forallP xs φ = none

forallP with an undefined element is none.

Since meetWK has none as a zero element, once any φ(x) = none is encountered, the accumulator becomes none and stays none.

§5 `believe` via doxastic accessibility #

Grove §4.2 (eq. 28): believe = λφ,x,i. ∀_# j : dox(x,i,j) ⇒ φ(j). The verb quantifies over doxastically accessible worlds with ∀_# and uses the material conditional ⇒. The ⇒ contributes the key filtering behavior: when dox(x,i,j) = false, ⇒ returns some true regardless of φ(j)'s definedness.

def Semantics.Composition.MaybeMonad.believe {W E : Type} (dox : E → W → W → Bool) (worlds : List W) (φ : Iₚ W Bool) (x : E) :

believe (Grove eq. 28).

Given an accessibility relation dox, a list of worlds, a complement φ : Iₚ W Bool, an agent x, and an evaluation world i: believe dox worlds φ x i = ∀_# j ∈ worlds : dox(x,i,j) ⇒ φ(j)

Equations

Semantics.Composition.MaybeMonad.believe dox worlds φ x i = Semantics.Composition.MaybeMonad.forallP worlds fun (j : W) => Semantics.Composition.MaybeMonad.materialCond (some (dox x i j)) (φ j)

Instances For

§6 Bridges to existing linglib types #

Option Bool, Truth3, and PrProp W are three representations of possibly-undefined truth values. These conversions connect Grove's formalization to the rest of the presupposition infrastructure.

def Semantics.Composition.MaybeMonad.toTruth3 :

Option Bool → Core.Duality.Truth3

Convert Option Bool to Truth3.

Equations

Instances For

def Semantics.Composition.MaybeMonad.ofTruth3 :

Core.Duality.Truth3 → Option Bool

Convert Truth3 to Option Bool.

Equations

Instances For

theorem Semantics.Composition.MaybeMonad.roundtrip_truth3 (v : Core.Duality.Truth3) :

toTruth3 (ofTruth3 v) = v

theorem Semantics.Composition.MaybeMonad.roundtrip_option (v : Option Bool) :

ofTruth3 (toTruth3 v) = v

def Semantics.Composition.MaybeMonad.impMK :

Core.Duality.Truth3 → Core.Duality.Truth3 → Core.Duality.Truth3

Middle Kleene implication on Truth3.

Equations

Instances For

theorem Semantics.Composition.MaybeMonad.materialCond_eq_truth3 (p q : Option Bool) :

toTruth3 (materialCond p q) = impMK (toTruth3 p) (toTruth3 q)

materialCond corresponds to middle Kleene implication on Truth3.

theorem Semantics.Composition.MaybeMonad.meetWK_eq_truth3 (p q : Option Bool) :

toTruth3 (meetWK p q) = (toTruth3 p).meetWeak (toTruth3 q)

meetWK corresponds to Truth3.meetWeak from Core.Duality.

theorem Semantics.Composition.MaybeMonad.joinWK_eq_truth3 (p q : Option Bool) :

toTruth3 (joinWK p q) = (toTruth3 p).joinWeak (toTruth3 q)

joinWK corresponds to Truth3.joinWeak from Core.Duality.

def Semantics.Composition.MaybeMonad.toProp3 {W : Type} (φ : Iₚ W Bool) :

Core.Duality.Prop3 W

Convert Iₚ W Bool to Prop3 W (world-indexed three-valued proposition).

Equations

Semantics.Composition.MaybeMonad.toProp3 φ w = Semantics.Composition.MaybeMonad.toTruth3 (φ w)

Instances For

def Semantics.Composition.MaybeMonad.toPrProp {W : Type} (φ : Iₚ W Bool) :

Core.Presupposition.PrProp W

Convert Iₚ W Bool to PrProp W.

The presupposition field is isSome (defined?), and the assertion is the Bool value (defaulting to false when undefined).

Equations

Semantics.Composition.MaybeMonad.toPrProp φ = { presup := fun (w : W) => (φ w).isSome, assertion := fun (w : W) => (φ w).getD false }

Instances For

theorem Semantics.Composition.MaybeMonad.toPrProp_presup {W : Type} (φ : Iₚ W Bool) (w : W) :

(toPrProp φ).presup w = (φ w).isSome

theorem Semantics.Composition.MaybeMonad.toPrProp_assertion {W : Type} (φ : Iₚ W Bool) (w : W) (v : Bool) (h : φ w = some v) :

(toPrProp φ).assertion w = v