Proposition

Theory-neutral infrastructure for modeling propositions in formal semantics. Prop' W is classical (W → Prop); BProp W is decidable (W → Bool).

@[reducible, inline]

abbrev Core.Proposition.Prop' (W : Type u_1) : Type u_1

Classical propositions: sets of worlds (standard formal semantics).

Equations

• Prop' W = (W → Prop)

@[reducible, inline]

abbrev Core.Proposition.BProp (W : Type u_1) : Type u_1

Decidable propositions: for computation.

Equations

• BProp W = (W → Bool)

instance Core.Proposition.bpropToProp' (W : Type u_1) : Coe (BProp W) (Prop' W)

Coercion from decidable to classical propositions.

Equations

• Core.Proposition.bpropToProp' W = { coe := fun (p : BProp W) (w : W) => p w = true }

def Core.Proposition.Classical.pnot (W : Type u_1) (p : Prop' W) : Prop' W

Propositional negation.

Equations

• Core.Proposition.Classical.pnot W p w = ¬p w

def Core.Proposition.Classical.pand (W : Type u_1) (p q : Prop' W) : Prop' W

Propositional conjunction.

Equations

• Core.Proposition.Classical.pand W p q w = (p w ∧ q w)

def Core.Proposition.Classical.por (W : Type u_1) (p q : Prop' W) : Prop' W

Propositional disjunction.

Equations

• Core.Proposition.Classical.por W p q w = (p w ∨ q w)

def Core.Proposition.Classical.pimp (W : Type u_1) (p q : Prop' W) : Prop' W

Propositional implication.

Equations

• Core.Proposition.Classical.pimp W p q w = (p w → q w)

def Core.Proposition.Classical.entails (W : Type u_1) (p q : Prop' W) : Prop

Semantic entailment: p entails q iff q is true whenever p is true.

Equations

• Core.Proposition.Classical.entails W p q = ∀ (w : W), p w → q w

def Core.Proposition.Classical.equiv (W : Type u_1) (p q : Prop' W) : Prop

Propositional equivalence.

Equations

• Core.Proposition.Classical.equiv W p q = (Core.Proposition.Classical.entails W p q ∧ Core.Proposition.Classical.entails W q p)

def Core.Proposition.Classical.bigConj (W : Type u_1) (X : Set (Prop' W)) : Prop' W

Grand conjunction: true at w iff all propositions in X are true at w.

Equations

• Core.Proposition.Classical.bigConj W X w = ∀ φ ∈ X, φ w

def Core.Proposition.Classical.bigDisj (W : Type u_1) (X : Set (Prop' W)) : Prop' W

Grand disjunction: true at w iff some proposition in X is true at w.

Equations

• Core.Proposition.Classical.bigDisj W X w = ∃ φ ∈ X, φ w

def Core.Proposition.Classical.consistent (W : Type u_1) (X : Set (Prop' W)) : Prop

Consistency: some world satisfies all propositions in X.

Equations

• Core.Proposition.Classical.consistent W X = ∃ (w : W), ∀ φ ∈ X, φ w

def Core.Proposition.Classical.top (W : Type u_1) : Prop' W

The always-true proposition.

Equations

• Core.Proposition.Classical.top W x✝ = True

def Core.Proposition.Classical.bot (W : Type u_1) : Prop' W

The always-false proposition.

Equations

• Core.Proposition.Classical.bot W x✝ = False

theorem Core.Proposition.Classical.entails_refl (W : Type u_1) (p : Prop' W) : entails W p p

theorem Core.Proposition.Classical.entails_trans (W : Type u_1) (p q r : Prop' W) (hpq : entails W p q) (hqr : entails W q r) : entails W p r

theorem Core.Proposition.Classical.equiv_refl (W : Type u_1) (p : Prop' W) : equiv W p p

theorem Core.Proposition.Classical.equiv_symm (W : Type u_1) (p q : Prop' W) (h : equiv W p q) : equiv W q p

theorem Core.Proposition.Classical.pnot_pnot (W : Type u_1) (p : Prop' W) : entails W p (pnot W (pnot W p))

theorem Core.Proposition.Classical.pand_eq_inf (W : Type u_1) (p q : Prop' W) : pand W p q = p ⊓ q

Conjunction equals infimum in the lattice.

theorem Core.Proposition.Classical.por_eq_sup (W : Type u_1) (p q : Prop' W) : por W p q = p ⊔ q

Disjunction equals supremum in the lattice.

theorem Core.Proposition.Classical.pnot_eq_compl (W : Type u_1) (p : Prop' W) : pnot W p = pᶜ

Negation equals complement in the Boolean algebra.

theorem Core.Proposition.Classical.entails_eq_le (W : Type u_1) (p q : Prop' W) : entails W p q ↔ p ≤ q

Entailment equals the lattice ordering.

theorem Core.Proposition.Classical.top_eq_latticeTop (W : Type u_1) : top W = ⊤

Top equals lattice top.

theorem Core.Proposition.Classical.bot_eq_latticeBot (W : Type u_1) : bot W = ⊥

Bot equals lattice bot.

def Core.Proposition.Decidable.pnot (W : Type u_1) (p : BProp W) : BProp W

Propositional negation.

Equations

• Core.Proposition.Decidable.pnot W p w = !p w

def Core.Proposition.Decidable.pand (W : Type u_1) (p q : BProp W) : BProp W

Propositional conjunction.

Equations

• Core.Proposition.Decidable.pand W p q w = (p w && q w)

def Core.Proposition.Decidable.por (W : Type u_1) (p q : BProp W) : BProp W

Propositional disjunction.

Equations

• Core.Proposition.Decidable.por W p q w = (p w || q w)

def Core.Proposition.Decidable.top (W : Type u_1) : BProp W

The always-true proposition.

Equations

• Core.Proposition.Decidable.top W x✝ = true

def Core.Proposition.Decidable.bot (W : Type u_1) : BProp W

The always-false proposition.

Equations

• Core.Proposition.Decidable.bot W x✝ = false

def Core.Proposition.Decidable.entails (W : Type u_1) (worlds : List W) (p q : BProp W) : Bool

Decidable entailment given explicit world enumeration.

Equations

• Core.Proposition.Decidable.entails W worlds p q = worlds.all fun (w : W) => !p w || q w

def Core.Proposition.Decidable.equiv (W : Type u_1) (worlds : List W) (p q : BProp W) : Bool

Decidable equivalence given explicit world enumeration.

Equations

• Core.Proposition.Decidable.equiv W worlds p q = (Core.Proposition.Decidable.entails W worlds p q && Core.Proposition.Decidable.entails W worlds q p)

def Core.Proposition.Decidable.consistent (W : Type u_1) (worlds : List W) (ps : List (BProp W)) : Bool

Decidable consistency: is there a world satisfying all propositions?

Equations

• Core.Proposition.Decidable.consistent W worlds ps = worlds.any fun (w : W) => ps.all fun (p : BProp W) => p w

def Core.Proposition.Decidable.count (W : Type u_1) (worlds : List W) (p : BProp W) : ℕ

Count worlds satisfying a proposition.

Equations

• Core.Proposition.Decidable.count W worlds p = (List.filter p worlds).length

def Core.Proposition.Decidable.filter (W : Type u_1) (worlds : List W) (p : BProp W) : List W

Get all worlds satisfying a proposition.

Equations

• Core.Proposition.Decidable.filter W worlds p = List.filter p worlds

theorem Core.Proposition.Decidable.pand_eq_inf (W : Type u_1) (p q : BProp W) : pand W p q = p ⊓ q

Conjunction equals infimum in the Bool lattice.

theorem Core.Proposition.Decidable.por_eq_sup (W : Type u_1) (p q : BProp W) : por W p q = p ⊔ q

Disjunction equals supremum in the Bool lattice.

theorem Core.Proposition.Decidable.pnot_eq_compl (W : Type u_1) (p : BProp W) : pnot W p = pᶜ

Negation equals complement in the Bool Boolean algebra.

theorem Core.Proposition.Decidable.top_eq_latticeTop (W : Type u_1) : top W = ⊤

Top equals lattice top.

theorem Core.Proposition.Decidable.bot_eq_latticeBot (W : Type u_1) : bot W = ⊥

Bot equals lattice bot.

theorem Core.Proposition.Decidable.pnot_reverses_entailment {W : Type u_1} (p q : BProp W) (h : ∀ (w : W), p w = true → q w = true) (w : W) : pnot W q w = true → pnot W p w = true

Negation reverses entailment (DE property).

theorem Core.Proposition.Decidable.pnot_pnot {W : Type u_1} (p : BProp W) : pnot W (pnot W p) = p

Double negation elimination for decidable propositions.

theorem Core.Proposition.Decidable.pnot_antitone {W : Type u_1} : Antitone (pnot W)

Negation is antitone (DE): if p ≤ q pointwise, then ¬q ≤ ¬p pointwise.

theorem Core.Proposition.decidable_pnot_eq_classical {W : Type u_1} (p : BProp W) : (fun (w : W) => Decidable.pnot W p w = true) = Classical.pnot W fun (w : W) => p w = true

Decidable negation corresponds to Classical negation under coercion.

theorem Core.Proposition.decidable_pand_eq_classical {W : Type u_1} (p q : BProp W) : (fun (w : W) => Decidable.pand W p q w = true) = Classical.pand W (fun (w : W) => p w = true) fun (w : W) => q w = true

Decidable conjunction corresponds to Classical conjunction.

theorem Core.Proposition.decidable_por_eq_classical {W : Type u_1} (p q : BProp W) : (fun (w : W) => Decidable.por W p q w = true) = Classical.por W (fun (w : W) => p w = true) fun (w : W) => q w = true

Decidable disjunction corresponds to Classical disjunction.

theorem Core.Proposition.classical_pnot_is_de {W : Type u_1} (p q : BProp W) : (∀ (w : W), (fun (w : W) => p w = true) w → (fun (w : W) => q w = true) w) → ∀ (w : W), Classical.pnot W (fun (w : W) => q w = true) w → Classical.pnot W (fun (w : W) => p w = true) w

Transfer theorem: DE property of Decidable.pnot implies DE for Classical.pnot.

def Core.Proposition.ClassicalNotation.«term∼_» : Lean.ParserDescr

Equations

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

def Core.Proposition.ClassicalNotation.«term_∧ₚ_» : Lean.TrailingParserDescr

Equations

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

def Core.Proposition.ClassicalNotation.«term_∨ₚ_» : Lean.TrailingParserDescr

Equations

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

def Core.Proposition.ClassicalNotation.«term_→ₚ_» : Lean.TrailingParserDescr

Equations

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

def Core.Proposition.ClassicalNotation.«term_⊆ₚ_» : Lean.TrailingParserDescr

Equations

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

def Core.Proposition.ClassicalNotation.«term_≡ₚ_» : Lean.TrailingParserDescr

Equations

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

def Core.Proposition.ClassicalNotation.«term⋀» : Lean.ParserDescr

Equations

• Core.Proposition.ClassicalNotation.«term⋀» = Lean.ParserDescr.node `Core.Proposition.ClassicalNotation.«term⋀» 1024 (Lean.ParserDescr.symbol "⋀")

def Core.Proposition.ClassicalNotation.«term⋁» : Lean.ParserDescr

Equations

• Core.Proposition.ClassicalNotation.«term⋁» = Lean.ParserDescr.node `Core.Proposition.ClassicalNotation.«term⋁» 1024 (Lean.ParserDescr.symbol "⋁")

def Core.Proposition.DecidableNotation.«term∼ᵇ_» : Lean.ParserDescr

Equations

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

def Core.Proposition.DecidableNotation.«term_∧ᵇ_» : Lean.TrailingParserDescr

Equations

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

def Core.Proposition.DecidableNotation.«term_∨ᵇ_» : Lean.TrailingParserDescr

Equations

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

class Core.Proposition.FiniteWorlds (W : Type u_1) : Type u_1

Typeclass for types with a complete enumeration of all elements.

• worlds : List W

  List of all worlds

• complete (w : W) : w ∈ worlds

  The list is complete

def Core.Proposition.FiniteWorlds.entails (W : Type u_1) [FiniteWorlds W] (p q : BProp W) : Bool

Decidable entailment using the FiniteWorlds instance.

Equations

• Core.Proposition.FiniteWorlds.entails W p q = Core.Proposition.Decidable.entails W Core.Proposition.FiniteWorlds.worlds p q

def Core.Proposition.FiniteWorlds.equiv (W : Type u_1) [FiniteWorlds W] (p q : BProp W) : Bool

Decidable equivalence using the FiniteWorlds instance.

Equations

• Core.Proposition.FiniteWorlds.equiv W p q = Core.Proposition.Decidable.equiv W Core.Proposition.FiniteWorlds.worlds p q

def Core.Proposition.FiniteWorlds.consistent (W : Type u_1) [FiniteWorlds W] (ps : List (BProp W)) : Bool

Decidable consistency using the FiniteWorlds instance.

Equations

• Core.Proposition.FiniteWorlds.consistent W ps = Core.Proposition.Decidable.consistent W Core.Proposition.FiniteWorlds.worlds ps

def Core.Proposition.FiniteWorlds.count (W : Type u_1) [FiniteWorlds W] (p : BProp W) : ℕ

Count satisfying worlds.

Equations

• Core.Proposition.FiniteWorlds.count W p = Core.Proposition.Decidable.count W Core.Proposition.FiniteWorlds.worlds p

def Core.Proposition.FiniteWorlds.filter (W : Type u_1) [FiniteWorlds W] (p : BProp W) : List W

Filter satisfying worlds.

Equations

• Core.Proposition.FiniteWorlds.filter W p = Core.Proposition.Decidable.filter W Core.Proposition.FiniteWorlds.worlds p

noncomputable def Core.Proposition.FiniteWorlds.ofFintype {W : Type u_1} [Fintype W] [DecidableEq W] : FiniteWorlds W

Build a FiniteWorlds instance from Fintype + DecidableEq. Bridges the Mathlib Fintype convention (used by 26+ RSA files) to the linglib FiniteWorlds convention (used by 47+ files).

Equations

• Core.Proposition.FiniteWorlds.ofFintype = { worlds := Fintype.elems.val.toList.dedup, complete := ⋯ }

noncomputable def Core.Proposition.FiniteWorlds.toFintype {W : Type u_1} [fw : FiniteWorlds W] : Fintype W

Convert a FiniteWorlds instance to Fintype. Bridges in the other direction: linglib FiniteWorlds → Mathlib Fintype. Uses classical for DecidableEq needed by List.toFinset.

Equations

• Core.Proposition.FiniteWorlds.toFintype = { elems := Core.Proposition.FiniteWorlds.worlds.toFinset, complete := ⋯ }

theorem Core.Proposition.entails_sound (W : Type u_1) [FiniteWorlds W] (p q : BProp W) : FiniteWorlds.entails W p q = true → Classical.entails W (fun (w : W) => p w = true) fun (w : W) => q w = true

Decidable entailment is sound w.r.t. classical entailment.

inductive Core.Proposition.World4 : Type

A simple 4-world type for basic examples.

• w0 : World4
• w1 : World4
• w2 : World4
• w3 : World4

instance Core.Proposition.instDecidableEqWorld4 : DecidableEq World4

Equations

• Core.Proposition.instDecidableEqWorld4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Proposition.instBEqWorld4 : BEq World4

Equations

• Core.Proposition.instBEqWorld4 = { beq := Core.Proposition.instBEqWorld4.beq }

def Core.Proposition.instBEqWorld4.beq : World4 → World4 → Bool

Equations

• Core.Proposition.instBEqWorld4.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Proposition.instReprWorld4 : Repr World4

Equations

• Core.Proposition.instReprWorld4 = { reprPrec := Core.Proposition.instReprWorld4.repr }

def Core.Proposition.instReprWorld4.repr : World4 → ℕ → Std.Format

Equations

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

instance Core.Proposition.instInhabitedWorld4 : Inhabited World4

Equations

• Core.Proposition.instInhabitedWorld4 = { default := Core.Proposition.instInhabitedWorld4.default }

def Core.Proposition.instInhabitedWorld4.default : World4

Equations

• Core.Proposition.instInhabitedWorld4.default = Core.Proposition.World4.w0

instance Core.Proposition.instFiniteWorldsWorld4 : FiniteWorlds World4

Equations

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

inductive Core.Proposition.World2 : Type

A simple 2-world type (true/false worlds).

• wT : World2
• wF : World2

instance Core.Proposition.instDecidableEqWorld2 : DecidableEq World2

Equations

• Core.Proposition.instDecidableEqWorld2 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Proposition.instBEqWorld2.beq : World2 → World2 → Bool

Equations

• Core.Proposition.instBEqWorld2.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Proposition.instBEqWorld2 : BEq World2

Equations

• Core.Proposition.instBEqWorld2 = { beq := Core.Proposition.instBEqWorld2.beq }

instance Core.Proposition.instReprWorld2 : Repr World2

Equations

• Core.Proposition.instReprWorld2 = { reprPrec := Core.Proposition.instReprWorld2.repr }

def Core.Proposition.instReprWorld2.repr : World2 → ℕ → Std.Format

Equations

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

instance Core.Proposition.instInhabitedWorld2 : Inhabited World2

Equations

• Core.Proposition.instInhabitedWorld2 = { default := Core.Proposition.instInhabitedWorld2.default }

def Core.Proposition.instInhabitedWorld2.default : World2

Equations

• Core.Proposition.instInhabitedWorld2.default = Core.Proposition.World2.wT

instance Core.Proposition.instFiniteWorldsWorld2 : FiniteWorlds World2

Equations

• Core.Proposition.instFiniteWorldsWorld2 = { worlds := [Core.Proposition.World2.wT, Core.Proposition.World2.wF], complete := Core.Proposition.instFiniteWorldsWorld2._proof_1 }

def Core.Proposition.GaloisConnection.extension {W : Type u_1} (props : Set (Prop' W)) : Set W

Extension (Set-based): compute the worlds where all propositions hold.

Equations

• Core.Proposition.GaloisConnection.extension props = {w : W | ∀ p ∈ props, p w}

def Core.Proposition.GaloisConnection.intension {W : Type u_1} (worlds : Set W) : Set (Prop' W)

Intension (Set-based): compute propositions true at all given worlds.

Equations

• Core.Proposition.GaloisConnection.intension worlds = {p : Prop' W | ∀ w ∈ worlds, p w}

theorem Core.Proposition.GaloisConnection.extension_antitone {W : Type u_1} : Antitone extension

Extension is antitone: more propositions → fewer worlds.

theorem Core.Proposition.GaloisConnection.intension_antitone {W : Type u_1} : Antitone intension

Intension is antitone: fewer worlds → more propositions.

theorem Core.Proposition.GaloisConnection.galois_connection {W : Type u_1} (A : Set (Prop' W)) (Ws : Set W) : Ws ⊆ extension A ↔ A ⊆ intension Ws

Galois connection: W ⊆ ext(A) ↔ A ⊆ int(W).

theorem Core.Proposition.GaloisConnection.galois_right {W : Type u_1} (A : Set (Prop' W)) (Ws : Set W) (h : A ⊆ intension Ws) : Ws ⊆ extension A

Galois connection (← direction): A ⊆ int(W) implies W ⊆ ext(A).

theorem Core.Proposition.GaloisConnection.galois_left {W : Type u_1} (A : Set (Prop' W)) (Ws : Set W) (h : Ws ⊆ extension A) : A ⊆ intension Ws

Galois connection (→ direction): W ⊆ ext(A) implies A ⊆ int(W).

theorem Core.Proposition.GaloisConnection.closure_expanding {W : Type u_1} (Ws : Set W) : Ws ⊆ extension (intension Ws)

Closure property: ext(int(W)) ⊇ W.

theorem Core.Proposition.GaloisConnection.closure_expanding' {W : Type u_1} (A : Set (Prop' W)) : A ⊆ intension (extension A)

Closure property: int(ext(A)) ⊇ A.

def Core.Proposition.GaloisConnection.gc {W : Type u_1} : GaloisConnection (⇑OrderDual.toDual ∘ extension) (intension ∘ ⇑OrderDual.ofDual)

Mathlib Galois connection between Set (Prop' W) and (Set W)ᵒᵈ.

Since extension and intension are both antitone, the adjunction lives between Set (Prop' W) and the order dual of Set W: l = toDual ∘ extension, u = intension ∘ ofDual.

The GC condition l A ≤ᵒᵈ b ↔ A ≤ u b unfolds to exactly the hand-proved galois_connection: Ws ⊆ ext(A) ↔ A ⊆ int(Ws).

Equations

• ⋯ = ⋯

def Core.Proposition.GaloisConnection.extensionL {W : Type u_1} (worlds : List W) (props : List (BProp W)) : List W

Extension (List-based): compute worlds where all propositions hold.

Equations

• Core.Proposition.GaloisConnection.extensionL worlds props = List.filter (fun (w : W) => props.all fun (p : BProp W) => p w) worlds

def Core.Proposition.GaloisConnection.intensionL {W : Type u_1} (worlds : List W) (props : List (BProp W)) : List (BProp W)

Intension (List-based): filter propositions true at all given worlds.

Equations

• Core.Proposition.GaloisConnection.intensionL worlds props = List.filter (fun (p : BProp W) => worlds.all p) props

theorem Core.Proposition.GaloisConnection.extensionL_antitone {W : Type u_1} (worlds : List W) (A B : List (BProp W)) (w : W) (hSub : ∀ p ∈ A, p ∈ B) (hw : w ∈ extensionL worlds B) : w ∈ extensionL worlds A

Extension is antitone (List version).

theorem Core.Proposition.GaloisConnection.intensionL_antitone {W : Type u_1} (props : List (BProp W)) (W1 W2 : List W) (p : BProp W) (hSub : ∀ w ∈ W1, w ∈ W2) (hp : p ∈ intensionL W2 props) : p ∈ intensionL W1 props

Intension is antitone (List version).

theorem Core.Proposition.GaloisConnection.closureL_expanding {W : Type u_1} (allWorlds : List W) (props : List (BProp W)) (Ws : List W) (hWs : ∀ w ∈ Ws, w ∈ allWorlds) (w : W) (hw : w ∈ Ws) : w ∈ extensionL allWorlds (intensionL Ws props)

Closure expanding (List version).

def Core.Proposition.GaloisConnection.extensionFW (W : Type u_1) [FiniteWorlds W] (props : List (BProp W)) : List W

FiniteWorlds version of extension.

Equations

• Core.Proposition.GaloisConnection.extensionFW W props = Core.Proposition.GaloisConnection.extensionL Core.Proposition.FiniteWorlds.worlds props

def Core.Proposition.GaloisConnection.intensionFW (W : Type u_1) [FiniteWorlds W] (worlds : List W) (props : List (BProp W)) : List (BProp W)

FiniteWorlds version of intension.

Equations

• Core.Proposition.GaloisConnection.intensionFW W worlds props = Core.Proposition.GaloisConnection.intensionL worlds props