inductive Semantics.Entailment.World : Type

A small finite set of worlds for decidable reasoning.

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

@[implicit_reducible]

instance Semantics.Entailment.instDecidableEqWorld : DecidableEq World

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Entailment.instReprWorld : Repr World

Equations

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

def Semantics.Entailment.allWorlds : List World

Equations

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

@[implicit_reducible]

instance Semantics.Entailment.instFintypeWorld : Fintype World

Equations

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

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

Semantic entailment: thin alias for Set inclusion (p ⊆ q). The discourse-meaningful name is kept; the body is mathlib's subset relation.

Equations

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

@[implicit_reducible]

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

Equations

• Semantics.Entailment.instDecidableEntailsOfDecidablePredWorldMemSet p q = Fintype.decidableForallFintype

def Semantics.Entailment.pnot : Set World → Set World

Negation: thin alias for set complement.

Equations

• Semantics.Entailment.pnot = compl

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

Conjunction: thin alias for set intersection.

Equations

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

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

Disjunction: thin alias for set union.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Semantics.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

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

@[implicit_reducible]

instance Semantics.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

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

theorem Semantics.Entailment.pnot_reverses_entailment {p q : Set World} (h : entails p q) : entails (pnot q) (pnot p)

Negation reverses entailment.

def Semantics.Entailment.p0 : Set World

Proposition true only in w0.

Equations

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

def Semantics.Entailment.p01 : Set World

Proposition true in w0 and w1.

Equations

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

def Semantics.Entailment.p012 : Set World

Proposition true in w0, w1, w2.

Equations

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

def Semantics.Entailment.pAll : Set World

Proposition true everywhere.

Equations

• Semantics.Entailment.pAll = Set.univ

def Semantics.Entailment.pNone : Set World

Proposition false everywhere.

Equations

• Semantics.Entailment.pNone = ∅

@[implicit_reducible]

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

Equations

• Semantics.Entailment.instDecidablePredWorldMemSetP0 w = id inferInstance

@[implicit_reducible]

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

Equations

• Semantics.Entailment.instDecidablePredWorldMemSetP01 w = id inferInstance

@[implicit_reducible]

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

Equations

• Semantics.Entailment.instDecidablePredWorldMemSetP012 w = id inferInstance

@[implicit_reducible]

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

Equations

• Semantics.Entailment.instDecidablePredWorldMemSetPAll x✝ = isTrue trivial

@[implicit_reducible]

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

Equations

• Semantics.Entailment.instDecidablePredWorldMemSetPNone x✝ = isFalse not_false

def Semantics.Entailment.testCases : List (Set World × Set World)

Test cases for monotonicity: pairs where first entails second.

Equations

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

theorem Semantics.Entailment.p0_entails_p01 : entails p0 p01

p0 entails p01.

theorem Semantics.Entailment.p01_entails_p012 : entails p01 p012

p01 entails p012.