The canonical some/all world model

The minimal scenario type for evaluating the some/all scalar contrast ([Hor72]): three worlds covering "no entity has the property" / "at least one but not all do" / "all do", with the literal some/all meanings and the canonical implicature as decidable predicates.

Consumed as a model input by the implicature study files ([GP09], [CS11]) and as a component of richer scenario types (belief worlds, picture cells).

Main declarations

• SomeAllWorld — the 3-world scenario type.
• SomeAllWorld.atLeastOne / SomeAllWorld.universal — literal some and all meanings.
• SomeAllWorld.notUniversal — the canonical scalar implicature of some, defined as the negation of universal.

inductive SomeAllWorld : Type

The minimal scenario type for evaluating the some/all scalar contrast. Three worlds, parameterized by an implicit entity-set whose property-holders are being counted: zero (none), at least one but not all (someNotAll), or all (all).

• none : SomeAllWorld
• someNotAll : SomeAllWorld
• all : SomeAllWorld

@[implicit_reducible]

instance instDecidableEqSomeAllWorld : DecidableEq SomeAllWorld

Equations

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

def instReprSomeAllWorld.repr : SomeAllWorld → ℕ → Std.Format

Equations

• instReprSomeAllWorld.repr SomeAllWorld.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SomeAllWorld.none")).group prec✝
• instReprSomeAllWorld.repr SomeAllWorld.someNotAll prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SomeAllWorld.someNotAll")).group prec✝
• instReprSomeAllWorld.repr SomeAllWorld.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SomeAllWorld.all")).group prec✝

@[implicit_reducible]

instance instReprSomeAllWorld : Repr SomeAllWorld

Equations

• instReprSomeAllWorld = { reprPrec := instReprSomeAllWorld.repr }

@[implicit_reducible]

instance instInhabitedSomeAllWorld : Inhabited SomeAllWorld

Equations

• instInhabitedSomeAllWorld = { default := instInhabitedSomeAllWorld.default }

@[implicit_reducible]

instance instFintypeSomeAllWorld : Fintype SomeAllWorld

Equations

• instFintypeSomeAllWorld = { elems := { val := ↑SomeAllWorld.enumList, nodup := SomeAllWorld.enumList_nodup }, complete := instFintypeSomeAllWorld._proof_1 }

def SomeAllWorld.atLeastOne : SomeAllWorld → Prop

Literal some meaning: at least one entity has the property.

Equations

• SomeAllWorld.none.atLeastOne = False
• x✝.atLeastOne = True

def SomeAllWorld.universal : SomeAllWorld → Prop

Literal all meaning: every entity has the property.

Equations

• SomeAllWorld.all.universal = True
• x✝.universal = False

def SomeAllWorld.notUniversal (w : SomeAllWorld) : Prop

The canonical scalar implicature of some: not all. Defined as the negation of universal.

Equations

• w.notUniversal = ¬w.universal

@[implicit_reducible]

instance SomeAllWorld.instDecidablePredAtLeastOne : DecidablePred atLeastOne

Equations

• SomeAllWorld.none.instDecidablePredAtLeastOne = isFalse not_false
• SomeAllWorld.someNotAll.instDecidablePredAtLeastOne = isTrue trivial
• SomeAllWorld.all.instDecidablePredAtLeastOne = isTrue trivial

@[implicit_reducible]

instance SomeAllWorld.instDecidablePredUniversal : DecidablePred universal

Equations

• SomeAllWorld.none.instDecidablePredUniversal = isFalse not_false
• SomeAllWorld.someNotAll.instDecidablePredUniversal = isFalse not_false
• SomeAllWorld.all.instDecidablePredUniversal = isTrue trivial

@[implicit_reducible]

instance SomeAllWorld.instDecidableNotUniversal (w : SomeAllWorld) : Decidable w.notUniversal

Equations

• w.instDecidableNotUniversal = SomeAllWorld.instDecidableNotUniversal._aux_1 w

theorem SomeAllWorld.universal_imp_atLeastOne {w : SomeAllWorld} (h : w.universal) : w.atLeastOne

all asymmetrically entails some: this is the structural source of the some/all scalar contrast.

theorem SomeAllWorld.notUniversal_iff_not_universal {w : SomeAllWorld} : w.notUniversal ↔ ¬w.universal

The SI of some is exactly the complement of all.