Finite-world test fixture for entailment

Thin shim over Set / compl / ∩ / ∪ from mathlib, specialized to a 4-element World enum. Consumers in Linglib.Semantics.Entailment.* use the World type + a handful of test propositions to write by decide test cases for monotonicity, polarity, and presupposition machinery.

The general (polymorphic) monotonicity theorems live in Linglib.Semantics.Quantification.Quantifier (every_scope_up, some_scope_up, no_scope_down, every_restrictor_down). This file provides only the finite-world fixture.

Reference: [vB86], [Lad80], [BC81].

inductive Entailment.World : Type

A small finite set of worlds for decidable reasoning.

• w0 : World
• w1 : World
• w2 : World
• w3 : World

@[implicit_reducible]

instance Entailment.instDecidableEqWorld : DecidableEq World

Equations

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

@[implicit_reducible]

instance Entailment.instReprWorld : Repr World

Equations

• Entailment.instReprWorld = { reprPrec := Entailment.instReprWorld.repr }

def Entailment.instReprWorld.repr : World → ℕ → Std.Format

Equations

• Entailment.instReprWorld.repr Entailment.World.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Entailment.World.w0")).group prec✝
• Entailment.instReprWorld.repr Entailment.World.w1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Entailment.World.w1")).group prec✝
• Entailment.instReprWorld.repr Entailment.World.w2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Entailment.World.w2")).group prec✝
• Entailment.instReprWorld.repr Entailment.World.w3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Entailment.World.w3")).group prec✝

def Entailment.allWorlds : List World

Equations

• Entailment.allWorlds = [Entailment.World.w0, Entailment.World.w1, Entailment.World.w2, Entailment.World.w3]

@[implicit_reducible]

instance Entailment.instFintypeWorld : Fintype World

Equations

• Entailment.instFintypeWorld = { elems := {Entailment.World.w0, Entailment.World.w1, Entailment.World.w2, Entailment.World.w3}, complete := Entailment.instFintypeWorld._proof_1 }

def Entailment.entails : Set World → Set World → Prop

Semantic entailment: thin alias for Set inclusion (p ⊆ q).

Equations

• Entailment.entails x1✝ x2✝ = (x1✝ ⊆ x2✝)

@[implicit_reducible]

instance Entailment.instDecidableEntailsOfDecidablePredWorldMemSet (p q : Set World) [DecidablePred fun (x : World) => x ∈ p] [DecidablePred fun (x : World) => x ∈ q] : Decidable (entails p q)

Equations

• Entailment.instDecidableEntailsOfDecidablePredWorldMemSet p q = Fintype.decidableForallFintype

def Entailment.pnot : Set World → Set World

Negation: thin alias for set complement.

Equations

• Entailment.pnot = compl

def Entailment.pand : Set World → Set World → Set World

Conjunction: thin alias for set intersection.

Equations

• Entailment.pand x1✝ x2✝ = x1✝ ∩ x2✝

def Entailment.por : Set World → Set World → Set World

Disjunction: thin alias for set union.

Equations

• Entailment.por x1✝ x2✝ = x1✝ ∪ x2✝

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetPnot (p : Set World) [DecidablePred fun (x : World) => x ∈ p] : DecidablePred fun (x : World) => x ∈ pnot p

Equations

• Entailment.instDecidablePredWorldMemSetPnot p w = Entailment.instDecidablePredWorldMemSetPnot._aux_1 p w

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetPand (p q : Set World) [DecidablePred fun (x : World) => x ∈ p] [DecidablePred fun (x : World) => x ∈ q] : DecidablePred fun (x : World) => x ∈ pand p q

Equations

• Entailment.instDecidablePredWorldMemSetPand p q w = Entailment.instDecidablePredWorldMemSetPand._aux_1 p q w

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetPor (p q : Set World) [DecidablePred fun (x : World) => x ∈ p] [DecidablePred fun (x : World) => x ∈ q] : DecidablePred fun (x : World) => x ∈ por p q

Equations

• Entailment.instDecidablePredWorldMemSetPor p q w = Entailment.instDecidablePredWorldMemSetPor._aux_1 p q w

def Entailment.p0 : Set World

Proposition true only in w0.

Equations

• Entailment.p0 = {Entailment.World.w0}

def Entailment.p01 : Set World

Proposition true in w0 and w1.

Equations

• Entailment.p01 = {Entailment.World.w0, Entailment.World.w1}

def Entailment.p012 : Set World

Proposition true in w0, w1, w2.

Equations

• Entailment.p012 = {Entailment.World.w0, Entailment.World.w1, Entailment.World.w2}

def Entailment.pAll : Set World

Proposition true everywhere.

Equations

• Entailment.pAll = Set.univ

def Entailment.pNone : Set World

Proposition false everywhere.

Equations

• Entailment.pNone = ∅

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetP0 : DecidablePred fun (x : World) => x ∈ p0

Equations

• Entailment.instDecidablePredWorldMemSetP0 w = id inferInstance

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetP01 : DecidablePred fun (x : World) => x ∈ p01

Equations

• Entailment.instDecidablePredWorldMemSetP01 w = id inferInstance

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetP012 : DecidablePred fun (x : World) => x ∈ p012

Equations

• Entailment.instDecidablePredWorldMemSetP012 w = id inferInstance

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetPAll : DecidablePred fun (x : World) => x ∈ pAll

Equations

• Entailment.instDecidablePredWorldMemSetPAll x✝ = isTrue trivial

@[implicit_reducible]

instance Entailment.instDecidablePredWorldMemSetPNone : DecidablePred fun (x : World) => x ∈ pNone

Equations

• Entailment.instDecidablePredWorldMemSetPNone x✝ = isFalse not_false

theorem Entailment.p0_entails_p01 : entails p0 p01

theorem Entailment.p01_entails_p012 : entails p01 p012