diff --git a/Linglib.lean b/Linglib.lean index d39ad9d7b..bec650168 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -46,13 +46,12 @@ import Linglib.Core.Logic.Quantification.Lattice import Linglib.Core.Logic.Quantification.Logicality import Linglib.Core.Logic.Quantification.Polyadic import Linglib.Core.Logic.Quantification.Exclusive -import Linglib.Core.Logic.Opposition.Aristotelian -import Linglib.Core.Logic.Opposition.Atoms -import Linglib.Core.Logic.Opposition.Bitstring -import Linglib.Core.Logic.Opposition.Diagram -import Linglib.Core.Logic.Opposition.Partition -import Linglib.Core.Logic.Opposition.Probabilistic -import Linglib.Core.Logic.Opposition.Square +import Linglib.Core.Logic.Aristotelian.Basic +import Linglib.Core.Logic.Aristotelian.Bitstring +import Linglib.Core.Logic.Aristotelian.Diagram +import Linglib.Core.Logic.Aristotelian.Partition +import Linglib.Core.Logic.Aristotelian.Probabilistic +import Linglib.Core.Logic.Aristotelian.Square import Linglib.Core.Logic.PolarizedIndividuals import Linglib.Core.Scales.Extent import Linglib.Semantics.Alternatives.Lexical diff --git a/Linglib/Core/Logic/Aristotelian/Basic.lean b/Linglib/Core/Logic/Aristotelian/Basic.lean new file mode 100644 index 000000000..3ae95f8fb --- /dev/null +++ b/Linglib/Core/Logic/Aristotelian/Basic.lean @@ -0,0 +1,227 @@ +import Mathlib.Logic.Basic +import Mathlib.Order.BooleanAlgebra.Basic +import Mathlib.Order.Hom.Basic + +/-! +# The four Aristotelian relations @cite{demey-smessaert-2018} + +Two elements φ, ψ of a Boolean algebra stand in one of four *Aristotelian +relations* (@cite{demey-smessaert-2024}, Definition 1): + +| Relation | Condition | mathlib | +|----------------|-----------------------------|----------------------------| +| Contradictory | `φ ⊓ ψ = ⊥` and `φ ⊔ ψ = ⊤` | `IsCompl` | +| Contrary | `φ ⊓ ψ = ⊥`, `φ ⊔ ψ ≠ ⊤` | `Disjoint ∧ ¬ Codisjoint` | +| Subcontrary | `φ ⊓ ψ ≠ ⊥`, `φ ⊔ ψ = ⊤` | `¬ Disjoint ∧ Codisjoint` | +| Subalternation | `φ < ψ` | `(· < ·)` | + +The collection `{CD, C, SC, SA}` is the *Aristotelian geometry*; elements +standing in none of the four are *unconnected* (@cite{smessaert-demey-2014}). + +The relations are defined over an arbitrary `[BooleanAlgebra α]` — the abstract +"template" of @cite{demey-smessaert-2024}. Concrete instances follow by plugging +in a Boolean algebra: the powerset `Set W`, predicate spaces `W → Prop` / +`W → Bool`, bitvectors `Fin n → Bool`, or a Lindenbaum–Tarski algebra. The +relations *are* mathlib's `IsCompl` / `Disjoint` / `Codisjoint` / `<`, so they +inherit that API. + +## Main declarations + +* `AristotelianRel` — the four relations (plus `unconnected`) as an inductive + label, used by `Diagram.relation` to label edges. +* `IsContradictory`, `IsContrary`, `IsSubcontrary`, `IsSubaltern`, + `IsUnconnected` — the relations over `[BooleanAlgebra α]`. +* `isContradictory_apply_orderIso` and siblings — a Boolean isomorphism + (`OrderIso`) is an *Aristotelian isomorphism*: it preserves and reflects all + four relations (@cite{deklerck-vignero-demey-2024}). +* `isContradictory_iff_forall` and siblings — the pointwise `∀ w` + characterization at the `W → Bool` instance. + +## Implementation notes + +`IsContradictory := IsCompl`, `IsSubaltern := (· < ·)`, and contrariety / +subcontrariety are `Disjoint` / `Codisjoint` combinations, so symmetry and the +`OrderIso` transfer come almost entirely from mathlib's order API. + +The relations are computed relative to a fixed Boolean algebra (equivalently a +single logic `S`). The same pair can stand in different relations under different +background logics; this *logic-sensitivity* (@cite{demey-frijters-2023}) is the +natural next layer. + +This is the base of a three-layer development: `Diagram.lean` adds labeled-poset +structure (squares, hexagons, cubes), and `Bitstring.lean` the partition-based +bitstring representation. The probabilistic generalization lives in +`Probabilistic.lean`. + +## Todo + +* Prove that `IsUnconnected` coincides with "no Aristotelian relation" under an + explicit contingency hypothesis. +* A first-class `AristotelianMorphism` / category of diagrams + (@cite{deklerck-vignero-demey-2024}); the `OrderIso` transfer lemmas are the + immediately-useful slice. +-/ + +namespace Aristotelian + +variable {W : Type*} + +/-- The four Aristotelian relations as a single inductive label, plus +`unconnected` for pairs standing in none of them. Used by `Diagram.relation` +to label edges. -/ +inductive AristotelianRel where + | contradictory + | contrary + | subcontrary + /-- The `φ → ψ` direction: `φ` is the stronger (superaltern), `ψ` the weaker + (subaltern). Asymmetric, so `subaltern φ ψ ≠ subaltern ψ φ`. -/ + | subaltern + | unconnected + deriving DecidableEq, Repr, Inhabited + +/-! ### The four relations -/ + +section Algebraic +variable {α : Type*} [BooleanAlgebra α] + +/-- BA-generic contradictoriness: `φ` and `ψ` are complementary — mathlib's + `IsCompl` (`Disjoint ∧ Codisjoint`); in a Boolean algebra, `ψ = φᶜ`. -/ +abbrev IsContradictory (φ ψ : α) : Prop := IsCompl φ ψ + +/-- BA-generic contrariety: jointly impossible (`Disjoint`) but not jointly + exhaustive (`¬ Codisjoint` — both can be false). -/ +abbrev IsContrary (φ ψ : α) : Prop := Disjoint φ ψ ∧ ¬ Codisjoint φ ψ + +/-- BA-generic subcontrariety: not jointly impossible (`¬ Disjoint` — both can + be true) but jointly exhaustive (`Codisjoint`). -/ +abbrev IsSubcontrary (φ ψ : α) : Prop := ¬ Disjoint φ ψ ∧ Codisjoint φ ψ + +/-- BA-generic *proper* subalternation: `φ` strictly entails `ψ`, i.e. `φ < ψ`. -/ +abbrev IsSubaltern (φ ψ : α) : Prop := φ < ψ + +/-- BA-generic unconnectedness: `φ` and `ψ` stand in none of the four + Aristotelian relations. Per @cite{demey-smessaert-2024}. -/ +abbrev IsUnconnected (φ ψ : α) : Prop := + ¬ Disjoint φ ψ ∧ ¬ Codisjoint φ ψ ∧ ¬ φ ≤ ψ ∧ ¬ ψ ≤ φ + +/-! ### Symmetry + +`IsContradictory` is symmetric via `IsCompl.symm` (`h.symm`); contrariety and +subcontrariety get their own lemmas; `IsSubaltern` is directional. -/ + +theorem IsContrary.symm {φ ψ : α} (h : IsContrary φ ψ) : + IsContrary ψ φ := ⟨h.1.symm, fun h' => h.2 h'.symm⟩ + +theorem IsSubcontrary.symm {φ ψ : α} (h : IsSubcontrary φ ψ) : + IsSubcontrary ψ φ := ⟨fun h' => h.1 h'.symm, h.2.symm⟩ + +/-! ### Transfer along a Boolean isomorphism + +A Boolean isomorphism — an `OrderIso` of Boolean algebras — is an *Aristotelian +isomorphism*: it preserves and reflects all four relations +(@cite{deklerck-vignero-demey-2024}, @cite{demey-smessaert-2024}; the abstract +content of @cite{demey-smessaert-2018}'s bitstring transfer). Each lemma is a +direct consequence of mathlib's `OrderIso` order-preservation API. -/ + +variable {β : Type*} [BooleanAlgebra β] + +theorem isContradictory_apply_orderIso (e : α ≃o β) {φ ψ : α} : + IsContradictory (e φ) (e ψ) ↔ IsContradictory φ ψ := (e.isCompl_iff).symm + +theorem isContrary_apply_orderIso (e : α ≃o β) {φ ψ : α} : + IsContrary (e φ) (e ψ) ↔ IsContrary φ ψ := by + simp only [IsContrary, disjoint_map_orderIso_iff, codisjoint_map_orderIso_iff] + +theorem isSubcontrary_apply_orderIso (e : α ≃o β) {φ ψ : α} : + IsSubcontrary (e φ) (e ψ) ↔ IsSubcontrary φ ψ := by + simp only [IsSubcontrary, disjoint_map_orderIso_iff, codisjoint_map_orderIso_iff] + +theorem isSubaltern_apply_orderIso (e : α ≃o β) {φ ψ : α} : + IsSubaltern (e φ) (e ψ) ↔ IsSubaltern φ ψ := e.lt_iff_lt + +end Algebraic + +/-! ### Pointwise characterization for `W → Bool` + +A `W → Bool` predicate is an element of the Boolean algebra `W → Bool`; the +abstract relations unfold to the familiar model-theoretic `∀ w` conditions +(validity `⊨ φ := ∀ w, φ w = true`). -/ + +section Pointwise +variable {φ ψ : W → Bool} + +private lemma bool_inf_eq_bot_iff (a b : Bool) : + a ⊓ b = ⊥ ↔ ¬ (a = true ∧ b = true) := by cases a <;> cases b <;> decide +private lemma bool_sup_eq_top_iff (a b : Bool) : + a ⊔ b = ⊤ ↔ (a = true ∨ b = true) := by cases a <;> cases b <;> decide +private lemma bool_le_iff (a b : Bool) : + a ≤ b ↔ (a = true → b = true) := by cases a <;> cases b <;> decide + +theorem isContradictory_iff_forall : + IsContradictory φ ψ ↔ + (∀ w, ¬ (φ w = true ∧ ψ w = true)) ∧ (∀ w, φ w = true ∨ ψ w = true) := by + unfold IsContradictory + rw [isCompl_iff, disjoint_iff, codisjoint_iff, funext_iff, funext_iff] + exact and_congr + (forall_congr' fun w => by + simp only [Pi.inf_apply, Pi.bot_apply]; exact bool_inf_eq_bot_iff (φ w) (ψ w)) + (forall_congr' fun w => by + simp only [Pi.sup_apply, Pi.top_apply]; exact bool_sup_eq_top_iff (φ w) (ψ w)) + +theorem isContrary_iff_forall : + IsContrary φ ψ ↔ + (∀ w, ¬ (φ w = true ∧ ψ w = true)) ∧ ¬ (∀ w, φ w = true ∨ ψ w = true) := by + unfold IsContrary + rw [disjoint_iff, codisjoint_iff] + refine and_congr ?_ (not_congr ?_) + · rw [funext_iff] + exact forall_congr' fun w => by + simp only [Pi.inf_apply, Pi.bot_apply]; exact bool_inf_eq_bot_iff (φ w) (ψ w) + · rw [funext_iff] + exact forall_congr' fun w => by + simp only [Pi.sup_apply, Pi.top_apply]; exact bool_sup_eq_top_iff (φ w) (ψ w) + +theorem isSubcontrary_iff_forall : + IsSubcontrary φ ψ ↔ + ¬ (∀ w, ¬ (φ w = true ∧ ψ w = true)) ∧ (∀ w, φ w = true ∨ ψ w = true) := by + unfold IsSubcontrary + rw [disjoint_iff, codisjoint_iff] + refine and_congr (not_congr ?_) ?_ + · rw [funext_iff] + exact forall_congr' fun w => by + simp only [Pi.inf_apply, Pi.bot_apply]; exact bool_inf_eq_bot_iff (φ w) (ψ w) + · rw [funext_iff] + exact forall_congr' fun w => by + simp only [Pi.sup_apply, Pi.top_apply]; exact bool_sup_eq_top_iff (φ w) (ψ w) + +theorem isSubaltern_iff_forall : + IsSubaltern φ ψ ↔ + (∀ w, φ w = true → ψ w = true) ∧ ¬ (∀ w, ψ w = true → φ w = true) := by + unfold IsSubaltern + rw [lt_iff_le_and_ne] + have key : (φ ≤ ψ ∧ φ ≠ ψ) ↔ (φ ≤ ψ ∧ ¬ ψ ≤ φ) := + and_congr_right fun hle => + ⟨fun hne hge => hne (le_antisymm hle hge), fun hnge heq => hnge heq.ge⟩ + rw [key, Pi.le_def, Pi.le_def] + exact and_congr (forall_congr' fun w => bool_le_iff (φ w) (ψ w)) + (not_congr (forall_congr' fun w => bool_le_iff (ψ w) (φ w))) + +theorem disjoint_iff_forall : + Disjoint φ ψ ↔ ∀ w, ¬ (φ w = true ∧ ψ w = true) := by + rw [disjoint_iff, funext_iff] + exact forall_congr' fun w => by + simp only [Pi.inf_apply, Pi.bot_apply]; exact bool_inf_eq_bot_iff (φ w) (ψ w) + +theorem codisjoint_iff_forall : + Codisjoint φ ψ ↔ ∀ w, φ w = true ∨ ψ w = true := by + rw [codisjoint_iff, funext_iff] + exact forall_congr' fun w => by + simp only [Pi.sup_apply, Pi.top_apply]; exact bool_sup_eq_top_iff (φ w) (ψ w) + +theorem le_iff_forall : + φ ≤ ψ ↔ ∀ w, φ w = true → ψ w = true := by + rw [Pi.le_def]; exact forall_congr' fun w => bool_le_iff (φ w) (ψ w) + +end Pointwise + +end Aristotelian diff --git a/Linglib/Core/Logic/Aristotelian/Bitstring.lean b/Linglib/Core/Logic/Aristotelian/Bitstring.lean new file mode 100644 index 000000000..0e8a0da68 --- /dev/null +++ b/Linglib/Core/Logic/Aristotelian/Bitstring.lean @@ -0,0 +1,405 @@ +import Linglib.Core.Logic.Aristotelian.Basic +import Linglib.Core.Logic.Aristotelian.Partition +import Mathlib.Data.Fintype.Order +import Mathlib.Order.BooleanSubalgebra + +/-! +# Bitstring semantics for logical fragments + +Per @cite{demey-smessaert-2018} §3.2. For a fragment `φ : ι → W → Bool`, the +bitstring of a formula `ψ` in the Boolean closure of `Set.range φ` records, for +each consistent anchor cell, whether that cell entails `ψ`. This map is a Boolean +isomorphism onto `Fin n → Bool` (Theorem 1), hence an Aristotelian isomorphism +(Theorem 2). + +## Main declarations + +* `bitstringOf` — the bitstring map (Definition 7). +* `bitstringOf_orderIso` — the isomorphism `closure (Set.range φ) ≃o (Fin n → Bool)`. +* `isAtom_anchor` — consistent anchor cells are the atoms of the closure. +* `isContradictory_bitstring_iff` and siblings — the Aristotelian relations transfer. + +## Implementation notes + +The closure-membership lemmas need only `[Fintype ι]` and live in the plain `{W}` +scope; the world-enumeration declarations index the `partition` and live in +`section WorldEnumeration` (`[Fintype W]`) below. +-/ + +namespace Aristotelian + +variable {W : Type*} + +/-! ### Anchor-decidedness -/ + +/-- Lemma 6 for the indexed-family `anchor`: every closure element is entailed by +an anchor or by its complement (@cite{demey-smessaert-2018}). -/ +theorem anchor_le_or_le_compl_mem_closure + {ι : Type*} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) {ψ : W → Bool} + (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) : + anchor φ σ ≤ ψ ∨ anchor φ σ ≤ ψᶜ := by + induction hψ using BooleanSubalgebra.closure_bot_sup_induction with + | mem ψ' hψ' => + obtain ⟨i, rfl⟩ := hψ' + by_cases h : σ i = true + · left + rw [le_iff_forall] + intro w hw + unfold anchor at hw + rw [decide_eq_true_eq] at hw + have := hw i + rw [if_pos h] at this + exact this + · right + rw [le_iff_forall] + intro w hw + have hf : σ i = false := Bool.eq_false_iff.mpr h + unfold anchor at hw + rw [decide_eq_true_eq] at hw + have := hw i + rw [if_neg h] at this + simp [this] + | bot => + right + rw [le_iff_forall] + intro w _ + rfl + | sup x _ y _ ihx ihy => + rcases ihx with hx | hx + · left; exact hx.trans le_sup_left + rcases ihy with hy | hy + · left; exact hy.trans le_sup_right + · right; rw [compl_sup]; exact le_inf hx hy + | compl x _ ih => + rcases ih with h | h + · right; rw [compl_compl]; exact h + · left; exact h + +/-! ### Anchor formulas lie in the closure -/ + +private theorem lit_mem_closure {ι : Type*} [Fintype ι] + (φ : ι → W → Bool) (σ : ι → Bool) (i : ι) : + (if σ i then φ i else (φ i)ᶜ) ∈ + BooleanSubalgebra.closure (Set.range φ) := by + by_cases h : σ i = true + · simp only [h, ↓reduceIte] + exact BooleanSubalgebra.subset_closure ⟨i, rfl⟩ + · have hf : σ i = false := Bool.eq_false_iff.mpr h + simp only [hf, Bool.false_eq_true, ↓reduceIte] + exact BooleanSubalgebra.compl_mem (BooleanSubalgebra.subset_closure ⟨i, rfl⟩) + +/-- The anchor over a `Finset s`: the conjunction of literals `±φ i` for `i ∈ s`. -/ +private def anchorOnFinset {ι : Type*} [DecidableEq ι] + (φ : ι → W → Bool) (σ : ι → Bool) (s : Finset ι) : W → Bool := + fun w => decide (∀ i ∈ s, if σ i then φ i w = true else φ i w = false) + +private theorem anchorOnFinset_empty {ι : Type*} [DecidableEq ι] + (φ : ι → W → Bool) (σ : ι → Bool) : + anchorOnFinset φ σ ∅ = (⊤ : W → Bool) := by + funext w + simp [anchorOnFinset] + +private theorem anchorOnFinset_insert {ι : Type*} [DecidableEq ι] + (φ : ι → W → Bool) (σ : ι → Bool) (i : ι) (s : Finset ι) : + anchorOnFinset φ σ (insert i s) = + anchorOnFinset φ σ s ⊓ (if σ i then φ i else (φ i)ᶜ) := by + funext w + show decide _ = _ + rw [decide_eq_decide.mpr (Finset.forall_mem_insert (s := s) (a := i) + (p := fun j => if σ j then φ j w = true else φ j w = false))] + rw [Bool.decide_and, Bool.and_comm, Pi.inf_apply] + congr 1 + cases hi : σ i <;> simp + +private theorem anchorOnFinset_mem_closure {ι : Type*} [DecidableEq ι] [Fintype ι] + (φ : ι → W → Bool) (σ : ι → Bool) (s : Finset ι) : + anchorOnFinset φ σ s ∈ BooleanSubalgebra.closure (Set.range φ) := by + induction s using Finset.induction_on with + | empty => + rw [anchorOnFinset_empty] + exact (BooleanSubalgebra.closure (Set.range φ)).top_mem + | insert i s his ih => + rw [anchorOnFinset_insert φ σ i s] + exact (BooleanSubalgebra.closure (Set.range φ)).infClosed' ih + (lit_mem_closure φ σ i) + +/-- Anchor formulas lie in the Boolean closure of `Set.range φ`. -/ +theorem anchor_mem_closure {ι : Type*} [DecidableEq ι] [Fintype ι] + (φ : ι → W → Bool) (σ : ι → Bool) : + anchor φ σ ∈ BooleanSubalgebra.closure (Set.range φ) := by + have hEq : anchor φ σ = anchorOnFinset φ σ Finset.univ := by + funext w + unfold anchor anchorOnFinset + congr 1 + exact propext ⟨fun h i _ => h i, fun h i => h i (Finset.mem_univ i)⟩ + rw [hEq] + exact anchorOnFinset_mem_closure φ σ Finset.univ + +/-! ### Atoms of the closure -/ + +/-- A consistent anchor cell is an atom of `closure (Set.range φ)`: it is below or +disjoint from every closure element (Lemma 6), so once nonzero nothing lies +strictly between it and `⊥`. -/ +theorem isAtom_anchor {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (σ : ι → Bool) (hCons : ∃ w, anchor φ σ w = true) : + IsAtom (⟨anchor φ σ, anchor_mem_closure φ σ⟩ : + BooleanSubalgebra.closure (Set.range φ)) := by + refine ⟨?_, fun b hb => ?_⟩ + · intro hbot + obtain ⟨w, hw⟩ := hCons + have hval : anchor φ σ = (⊥ : W → Bool) := congrArg Subtype.val hbot + rw [hval] at hw + exact Bool.noConfusion hw + · have hble : (b : W → Bool) ≤ anchor φ σ := hb.le + rcases anchor_le_or_le_compl_mem_closure φ σ b.2 with hL | hR + · exact absurd (Subtype.ext (le_antisymm hble hL)) hb.ne + · have hself : (b : W → Bool) ≤ (b : W → Bool)ᶜ := hble.trans hR + exact Subtype.ext (le_compl_self.mp hself) + +section WorldEnumeration + +variable [Fintype W] + +/-! ### Bitstring representation (Definition 7) -/ + +/-- A positional index for the anchor cells, via `partition.equivFin`. -/ +private noncomputable def anchorIndex {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) : + Fin (partition ι W φ).card → (ι → Bool) := + fun i => ((partition ι W φ).equivFin.symm i).val + +/-- The bitstring of `ψ` relative to `φ`: bit `i` is `true` iff anchor `i` entails +`ψ` (@cite{demey-smessaert-2018}, Definition 7). -/ +noncomputable def bitstringOf {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (ψ : W → Bool) : + Fin (partition ι W φ).card → Bool := + fun i => decide (∀ w, anchor φ (anchorIndex φ i) w = true → ψ w = true) + +private theorem anchorIndex_consistent {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (i : Fin (partition ι W φ).card) : + ∃ w, anchor φ (anchorIndex φ i) w = true := by + classical + have hMem : ((partition ι W φ).equivFin.symm i).val ∈ partition ι W φ := + ((partition ι W φ).equivFin.symm i).property + unfold partition at hMem + rw [Finset.mem_filter] at hMem + simpa [anchorIndex] using hMem.2 + +/-! ### Bitstring evaluation -/ + +/-- If `w` satisfies anchor `i` and `ψ` is in the closure, then `bitstringOf φ ψ i` +is `ψ w`. -/ +theorem bitstringOf_eq_apply_at_anchor + {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) {ψ : W → Bool} + (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) + (i : Fin (partition ι W φ).card) {w : W} + (hw : anchor φ (anchorIndex φ i) w = true) : + bitstringOf φ ψ i = ψ w := by + rcases anchor_le_or_le_compl_mem_closure φ (anchorIndex φ i) hψ with hL | hR + · have hβ : bitstringOf φ ψ i = true := by + unfold bitstringOf + rw [decide_eq_true_eq] + exact fun w' hw' => (le_iff_forall.mp hL) w' hw' + have hψw : ψ w = true := (le_iff_forall.mp hL) w hw + rw [hβ, hψw] + · have hψw : ψ w = false := by + have := (le_iff_forall.mp hR) w hw + simpa using this + have hβ : bitstringOf φ ψ i = false := by + cases hb : bitstringOf φ ψ i + · rfl + · exfalso + unfold bitstringOf at hb + rw [decide_eq_true_eq] at hb + rw [hb w hw] at hψw + exact Bool.noConfusion hψw + rw [hβ, hψw] + +/-- An anchor index satisfied by `w`. -/ +noncomputable def worldAnchorIndex {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (w : W) : Fin (partition ι W φ).card := + let σ := Classical.choose (anchor_jointly_exhaustive φ w) + let hσ := Classical.choose_spec (anchor_jointly_exhaustive φ w) + (partition ι W φ).equivFin ⟨σ, by + unfold partition + rw [Finset.mem_filter] + exact ⟨Finset.mem_univ _, decide_eq_true ⟨w, hσ⟩⟩⟩ + +theorem anchor_worldAnchorIndex {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (w : W) : + anchor φ (anchorIndex φ (worldAnchorIndex φ w)) w = true := by + unfold worldAnchorIndex anchorIndex + simp only [Equiv.symm_apply_apply] + exact Classical.choose_spec (anchor_jointly_exhaustive φ w) + +/-- `bitstringOf φ ψ` at a world's anchor index recovers `ψ` at that world. -/ +theorem bitstringOf_apply_at_world + {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) {ψ : W → Bool} + (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) (w : W) : + bitstringOf φ ψ (worldAnchorIndex φ w) = ψ w := + bitstringOf_eq_apply_at_anchor φ hψ _ (anchor_worldAnchorIndex φ w) + +/-- `bitstringOf φ` is injective on the Boolean closure. -/ +theorem bitstringOf_injOn_closure + {ι : Type*} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : + Set.InjOn (bitstringOf φ) + (BooleanSubalgebra.closure (Set.range φ) : Set (W → Bool)) := by + intro ψ₁ hψ₁ ψ₂ hψ₂ hEq + funext w + rw [← bitstringOf_apply_at_world φ hψ₁ w, hEq, bitstringOf_apply_at_world φ hψ₂ w] + +/-! ### The inverse and round trips -/ + +/-- The supremum of the anchor cells whose bit is `true` — the inverse of +`bitstringOf` on the closure. -/ +noncomputable def bitstringInverse {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : W → Bool := + ⨆ i, (if b i then anchor φ (anchorIndex φ i) else (⊥ : W → Bool)) + +theorem bitstringInverse_mem_closure {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : + bitstringInverse φ b ∈ BooleanSubalgebra.closure (Set.range φ) := by + unfold bitstringInverse + apply BooleanSubalgebra.iSup_mem + intro i + by_cases h : b i = true + · simp only [h, ↓reduceIte] + exact anchor_mem_closure φ _ + · have hf : b i = false := Bool.eq_false_iff.mpr h + simp only [hf, Bool.false_eq_true, ↓reduceIte] + exact (BooleanSubalgebra.closure (Set.range φ)).bot_mem + +private theorem anchorIndex_injective {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) : + Function.Injective (anchorIndex φ) := by + intro i j h + unfold anchorIndex at h + exact (partition ι W φ).equivFin.symm.injective (Subtype.ext h) + +private theorem anchor_at_world_unique + {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) {i j : Fin (partition ι W φ).card} {w : W} + (hi : anchor φ (anchorIndex φ i) w = true) + (hj : anchor φ (anchorIndex φ j) w = true) : + i = j := by + by_contra hne + apply anchor_mutually_exclusive φ (anchorIndex φ i) (anchorIndex φ j) + (fun heq => hne (anchorIndex_injective φ heq)) w + exact ⟨hi, hj⟩ + +/-- If `w` satisfies anchor `j`, then `bitstringInverse φ b w` is the `j`-th bit: +the `iSup` collapses to the summand at `j`. -/ +theorem bitstringInverse_apply_at_anchor + {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) + (j : Fin (partition ι W φ).card) {w : W} + (hw : anchor φ (anchorIndex φ j) w = true) : + bitstringInverse φ b w = b j := by + unfold bitstringInverse + rw [iSup_apply] + apply le_antisymm + · apply iSup_le + intro i + by_cases hij : i = j + · subst hij + by_cases hbi : b i = true + · simp [hbi, hw] + · have : b i = false := Bool.eq_false_iff.mpr hbi + simp [this] + · have hf : anchor φ (anchorIndex φ i) w = false := by + cases hai : anchor φ (anchorIndex φ i) w + · rfl + · exact absurd (anchor_at_world_unique φ hai hw) hij + by_cases hbi : b i = true + · simp [hbi, hf] + · have : b i = false := Bool.eq_false_iff.mpr hbi + simp [this] + · by_cases hbj : b j = true + · have h1 : (if b j then anchor φ (anchorIndex φ j) else (⊥ : W → Bool)) w = true := by + simp [hbj, hw] + calc b j = true := hbj + _ = (if b j then anchor φ (anchorIndex φ j) else (⊥ : W → Bool)) w := h1.symm + _ ≤ ⨆ i, (if b i then anchor φ (anchorIndex φ i) else (⊥ : W → Bool)) w := + le_iSup (fun i => (if b i then anchor φ (anchorIndex φ i) + else (⊥ : W → Bool)) w) j + · have : b j = false := Bool.eq_false_iff.mpr hbj + rw [this] + exact Bool.false_le _ + +theorem bitstringOf_bitstringInverse {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : + bitstringOf φ (bitstringInverse φ b) = b := by + funext j + obtain ⟨w, hw⟩ := anchorIndex_consistent φ j + rw [bitstringOf_eq_apply_at_anchor φ (bitstringInverse_mem_closure φ b) j hw] + exact bitstringInverse_apply_at_anchor φ b j hw + +theorem bitstringInverse_bitstringOf {ι : Type*} [Fintype ι] [DecidableEq ι] + (φ : ι → W → Bool) {ψ : W → Bool} + (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) : + bitstringInverse φ (bitstringOf φ ψ) = ψ := by + funext w + rw [bitstringInverse_apply_at_anchor φ (bitstringOf φ ψ) + (worldAnchorIndex φ w) (anchor_worldAnchorIndex φ w)] + exact bitstringOf_apply_at_world φ hψ w + +/-! ### Theorem 1: the Boolean isomorphism -/ + +/-- **Theorem 1** (@cite{demey-smessaert-2018}): `bitstringOf φ` is an order +isomorphism `closure (Set.range φ) ≃o (Fin n → Bool)`, `n = |partition|`. -/ +noncomputable def bitstringOf_orderIso + {ι : Type*} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : + BooleanSubalgebra.closure (Set.range φ) ≃o + (Fin (partition ι W φ).card → Bool) where + toFun := fun ⟨ψ, _⟩ => bitstringOf φ ψ + invFun := fun b => ⟨bitstringInverse φ b, bitstringInverse_mem_closure φ b⟩ + left_inv := fun ⟨ψ, hψ⟩ => Subtype.ext (bitstringInverse_bitstringOf φ hψ) + right_inv := fun b => bitstringOf_bitstringInverse φ b + map_rel_iff' := by + rintro ⟨ψ₁, hψ₁⟩ ⟨ψ₂, hψ₂⟩ + show bitstringOf φ ψ₁ ≤ bitstringOf φ ψ₂ ↔ ψ₁ ≤ ψ₂ + rw [le_iff_forall, le_iff_forall] + constructor + · intro h w hw₁ + have := h (worldAnchorIndex φ w) + rw [bitstringOf_apply_at_world φ hψ₁ w, + bitstringOf_apply_at_world φ hψ₂ w] at this + exact this hw₁ + · intro h i + obtain ⟨w, hw⟩ := anchorIndex_consistent φ i + rw [bitstringOf_eq_apply_at_anchor φ hψ₁ i hw, + bitstringOf_eq_apply_at_anchor φ hψ₂ i hw] + exact h w + +/-! ### Theorem 2: Aristotelian transfer + +Each relation transfers along the Boolean isomorphism `bitstringOf_orderIso` +(@cite{demey-smessaert-2018}, Theorem 2). -/ + +section Transfer +variable {ι : Type*} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) + (a b : BooleanSubalgebra.closure (Set.range φ)) + +theorem isContradictory_bitstring_iff : + IsContradictory (bitstringOf φ a.val) (bitstringOf φ b.val) ↔ IsContradictory a b := + isContradictory_apply_orderIso (bitstringOf_orderIso φ) + +theorem isContrary_bitstring_iff : + IsContrary (bitstringOf φ a.val) (bitstringOf φ b.val) ↔ IsContrary a b := + isContrary_apply_orderIso (bitstringOf_orderIso φ) + +theorem isSubcontrary_bitstring_iff : + IsSubcontrary (bitstringOf φ a.val) (bitstringOf φ b.val) ↔ IsSubcontrary a b := + isSubcontrary_apply_orderIso (bitstringOf_orderIso φ) + +theorem isSubaltern_bitstring_iff : + IsSubaltern (bitstringOf φ a.val) (bitstringOf φ b.val) ↔ IsSubaltern a b := + isSubaltern_apply_orderIso (bitstringOf_orderIso φ) + +end Transfer + +end WorldEnumeration + +end Aristotelian diff --git a/Linglib/Core/Logic/Aristotelian/Diagram.lean b/Linglib/Core/Logic/Aristotelian/Diagram.lean new file mode 100644 index 000000000..d854bd943 --- /dev/null +++ b/Linglib/Core/Logic/Aristotelian/Diagram.lean @@ -0,0 +1,37 @@ +import Linglib.Core.Logic.Aristotelian.Basic +import Mathlib.Data.Fintype.Basic + +/-! +# Aristotelian diagrams + +Per @cite{demey-smessaert-2024} (Definition 1). An Aristotelian diagram is a +fragment in a Boolean algebra: a finite indexed family `φ : ι → α` together with +the matrix of Aristotelian relations between its members. The classical square +(`Square.lean`) is the case `ι = Fin 4`. + +## TODO + +Hexagon (`ι = Fin 6`) and cube (`ι = Fin 8`) specializations. +-/ + +namespace Aristotelian + +variable {α : Type*} [BooleanAlgebra α] + +/-- An Aristotelian diagram (@cite{demey-smessaert-2024}, Definition 1): a finite +indexed family `φ : ι → α` with a relation matrix, where `relation_correct` +asserts the labels match the actual Aristotelian relations. `relation` is +convenience data, determined by `φ`. -/ +structure Diagram (ι : Type*) [Fintype ι] (α : Type*) [BooleanAlgebra α] where + /-- The corner-to-formula assignment. -/ + φ : ι → α + /-- The labeled relation between any two corners. -/ + relation : ι → ι → AristotelianRel + /-- The labels match the actual relations (`unconnected` is the residual). -/ + relation_correct : ∀ i j, + (relation i j = AristotelianRel.contradictory → IsContradictory (φ i) (φ j)) ∧ + (relation i j = AristotelianRel.contrary → IsContrary (φ i) (φ j)) ∧ + (relation i j = AristotelianRel.subcontrary → IsSubcontrary (φ i) (φ j)) ∧ + (relation i j = AristotelianRel.subaltern → IsSubaltern (φ i) (φ j)) + +end Aristotelian diff --git a/Linglib/Core/Logic/Aristotelian/Partition.lean b/Linglib/Core/Logic/Aristotelian/Partition.lean new file mode 100644 index 000000000..27dafcd89 --- /dev/null +++ b/Linglib/Core/Logic/Aristotelian/Partition.lean @@ -0,0 +1,65 @@ +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Fintype.Basic +import Mathlib.Data.Fintype.Pi + +/-! +# Partitions induced by logical fragments + +Per @cite{demey-smessaert-2018} §3.1. The partition of a finite fragment +`φ : ι → W → Bool` is its set of consistent *anchor formulas* — complete +conjunctions of literals `±φ i`. The anchors are mutually exclusive and jointly +exhaustive (Lemma 3), and their count is the bitstring length. + +## Main declarations + +* `anchor` — the anchor formula of a polarity assignment (Definition 5). +* `partition` — the consistent anchors of a fragment. +* `anchor_mutually_exclusive` / `anchor_jointly_exhaustive` — Lemma 3. +-/ + +namespace Aristotelian + +variable {W : Type*} + +/-! ### Anchor formulas (Definition 5) -/ + +/-- The anchor formula for polarity assignment `σ`: the conjunction `±φ_1 ∧ ⋯ ∧ ±φ_m`. -/ +def anchor {ι : Type*} [Fintype ι] (φ : ι → W → Bool) + (σ : ι → Bool) (w : W) : Bool := + decide (∀ i : ι, if σ i then (φ i w = true) else (φ i w = false)) + +/-- The partition of a fragment: all consistent polarity assignments. -/ +def partition (ι : Type*) [Fintype ι] [DecidableEq ι] (W : Type*) [Fintype W] + (φ : ι → W → Bool) : Finset (ι → Bool) := + Finset.univ.filter (fun σ => decide (∃ w : W, anchor φ σ w = true)) + +/-! ### Lemma 3 — mutual exclusivity and joint exhaustion -/ + +/-- Two distinct anchor formulas are jointly inconsistent. -/ +theorem anchor_mutually_exclusive {ι : Type*} [Fintype ι] + (φ : ι → W → Bool) (σ τ : ι → Bool) (h : σ ≠ τ) : + ∀ w, ¬ (anchor φ σ w = true ∧ anchor φ τ w = true) := by + intro w ⟨hσ, hτ⟩ + obtain ⟨i, hi⟩ : ∃ i, σ i ≠ τ i := by + by_contra hAll + push Not at hAll + exact h (funext hAll) + rw [anchor, decide_eq_true_eq] at hσ hτ + have hσi := hσ i + have hτi := hτ i + rcases hσ_val : σ i with _ | _ <;> rcases hτ_val : τ i with _ | _ + all_goals simp_all + +/-- Every world satisfies some anchor formula. -/ +theorem anchor_jointly_exhaustive {ι : Type*} [Fintype ι] + (φ : ι → W → Bool) (w : W) : + ∃ σ, anchor φ σ w = true := by + refine ⟨fun i => φ i w, ?_⟩ + rw [anchor, decide_eq_true_eq] + intro i + by_cases h : φ i w = true + · simp [h] + · have : φ i w = false := by cases hb : φ i w <;> simp_all + simp [this] + +end Aristotelian diff --git a/Linglib/Core/Logic/Aristotelian/Probabilistic.lean b/Linglib/Core/Logic/Aristotelian/Probabilistic.lean new file mode 100644 index 000000000..b045b541e --- /dev/null +++ b/Linglib/Core/Logic/Aristotelian/Probabilistic.lean @@ -0,0 +1,162 @@ +import Linglib.Core.Logic.Aristotelian.Basic +import Linglib.Core.Probability.Finite + +/-! +# Probabilistic Aristotelian relations + +When `W` carries a probability measure `μ : PMF W`, the four Aristotelian +relations generalise to linear (in)equalities on `P_μ[φ] := μ {w | φ w = true}`: + +| Boolean relation | Probabilistic counterpart | +|------------------------|---------------------------| +| `IsContradictory φ ψ` | `P[φ] + P[ψ] = 1` | +| `IsContrary φ ψ` | `P[φ] + P[ψ] ≤ 1` | +| `IsSubcontrary φ ψ` | `P[φ] + P[ψ] ≥ 1` | +| `IsSubaltern φ ψ` | `P[φ] ≤ P[ψ]` | + +The discrete case (`μ a ∈ {0,1}`) recovers Definition 1 of +@cite{demey-smessaert-2018}. The main results are the transfer theorems: a +Boolean Aristotelian relation implies its probabilistic counterpart under every +`μ` (the converse fails). +-/ + +namespace Aristotelian + +open scoped ENNReal + +variable {W : Type*} [Fintype W] + +/-! ### Probability of a Boolean predicate -/ + +/-- The probability of `φ : W → Bool` under `μ : PMF W`, i.e. `μ {w | φ w = true}`. -/ +noncomputable def boolProb (μ : PMF W) (φ : W → Bool) : ℝ≥0∞ := + PMF.probOfSet μ {w | φ w = true} + +@[inherit_doc boolProb] +notation "P[" φ " ; " μ "]" => boolProb μ φ + +/-- The PMF sums to 1 over the finite sample space. -/ +private lemma pmf_sum_univ (μ : PMF W) : ∑ x, μ x = (1 : ℝ≥0∞) := by + have h : ∑ x, μ x = (∑' x, μ x : ℝ≥0∞) := + (tsum_eq_sum (f := μ) (s := Finset.univ) + (fun x hx => absurd (Finset.mem_univ x) hx)).symm + rw [h, PMF.tsum_coe] + +/-- Total probability: `P[φ] + P[¬φ] = 1`. -/ +theorem boolProb_add_compl (μ : PMF W) (φ : W → Bool) : + boolProb μ φ + boolProb μ (fun w => !φ w) = 1 := by + classical + unfold boolProb PMF.probOfSet + rw [PMF.toOuterMeasure_apply_fintype, PMF.toOuterMeasure_apply_fintype, + ← Finset.sum_add_distrib] + have hsum : ∀ x, ({w | φ w = true} : Set W).indicator μ x + + ({w | (!φ w) = true} : Set W).indicator μ x = μ x := by + intro x + cases hφ : φ x + · simp [Set.indicator, hφ] + · simp [Set.indicator, hφ] + rw [Finset.sum_congr rfl (fun x _ => hsum x)] + exact pmf_sum_univ μ + +/-! ### Probabilistic Aristotelian relations (Definition 1, convex form) -/ + +/-- Probabilistic contradictoriness: `P[φ] + P[ψ] = 1`. -/ +def ProbContradictory (μ : PMF W) (φ ψ : W → Bool) : Prop := + boolProb μ φ + boolProb μ ψ = 1 + +/-- Probabilistic contrariety: `P[φ] + P[ψ] ≤ 1`. -/ +def ProbContrary (μ : PMF W) (φ ψ : W → Bool) : Prop := + boolProb μ φ + boolProb μ ψ ≤ 1 + +/-- Probabilistic subcontrariety: `P[φ] + P[ψ] ≥ 1`. -/ +def ProbSubcontrary (μ : PMF W) (φ ψ : W → Bool) : Prop := + boolProb μ φ + boolProb μ ψ ≥ 1 + +/-- Probabilistic subalternation: `P[φ] ≤ P[ψ]`. -/ +def ProbSubaltern (μ : PMF W) (φ ψ : W → Bool) : Prop := + boolProb μ φ ≤ boolProb μ ψ + +/-! ### Transfer theorems: Boolean ⇒ Probabilistic (for every μ) -/ + +/-- Boolean contradictoriness transfers to every measure (`ψ` is pointwise `!φ`). -/ +theorem ProbContradictory.of_isContradictory {φ ψ : W → Bool} + (h : IsContradictory φ ψ) (μ : PMF W) : + ProbContradictory μ φ ψ := by + obtain ⟨hAnd, hOr⟩ := isContradictory_iff_forall.mp h + have hPointwise : ∀ w, ψ w = !φ w := by + intro w + have h1 := hAnd w + have h2 := hOr w + cases hφ : φ w + · cases hψ : ψ w + · exfalso; exact h2.elim (fun h => by rw [hφ] at h; exact Bool.noConfusion h) + (fun h => by rw [hψ] at h; exact Bool.noConfusion h) + · simp [hφ] + · cases hψ : ψ w + · simp [hφ] + · exfalso; exact h1 ⟨hφ, hψ⟩ + have hψ_eq : ψ = (fun w => !φ w) := funext hPointwise + unfold ProbContradictory + rw [hψ_eq] + exact boolProb_add_compl μ φ + +/-- Boolean subalternation transfers to every measure (PMF monotonicity). -/ +theorem ProbSubaltern.of_isSubaltern {φ ψ : W → Bool} + (h : IsSubaltern φ ψ) (μ : PMF W) : + ProbSubaltern μ φ ψ := by + obtain ⟨hle, _⟩ := isSubaltern_iff_forall.mp h + unfold ProbSubaltern boolProb PMF.probOfSet + apply MeasureTheory.OuterMeasure.mono + intro w hw + exact hle w hw + +/-- Boolean contrariety transfers to every measure. -/ +theorem ProbContrary.of_isContrary {φ ψ : W → Bool} + (h : IsContrary φ ψ) (μ : PMF W) : + ProbContrary μ φ ψ := by + classical + obtain ⟨hAnd, _⟩ := isContrary_iff_forall.mp h + unfold ProbContrary boolProb PMF.probOfSet + rw [PMF.toOuterMeasure_apply_fintype, PMF.toOuterMeasure_apply_fintype, + ← Finset.sum_add_distrib] + have hbnd : ∀ x ∈ Finset.univ, + ({w | φ w = true} : Set W).indicator μ x + + ({w | ψ w = true} : Set W).indicator μ x ≤ μ x := by + intro x _ + by_cases hφ : φ x = true + · by_cases hψ : ψ x = true + · exact absurd ⟨hφ, hψ⟩ (hAnd x) + · simp [Set.indicator, hφ, hψ] + · by_cases hψ : ψ x = true + · simp [Set.indicator, hφ, hψ] + · simp [Set.indicator, hφ, hψ] + calc (∑ x, (({w | φ w = true} : Set W).indicator μ x + + ({w | ψ w = true} : Set W).indicator μ x)) + ≤ ∑ x, μ x := Finset.sum_le_sum hbnd + _ = 1 := pmf_sum_univ μ + +/-- Boolean subcontrariety transfers to every measure. -/ +theorem ProbSubcontrary.of_isSubcontrary {φ ψ : W → Bool} + (h : IsSubcontrary φ ψ) (μ : PMF W) : + ProbSubcontrary μ φ ψ := by + classical + obtain ⟨_, hOr⟩ := isSubcontrary_iff_forall.mp h + unfold ProbSubcontrary boolProb PMF.probOfSet + rw [PMF.toOuterMeasure_apply_fintype, PMF.toOuterMeasure_apply_fintype, + ← Finset.sum_add_distrib] + have hbnd : ∀ x ∈ Finset.univ, + μ x ≤ ({w | φ w = true} : Set W).indicator μ x + + ({w | ψ w = true} : Set W).indicator μ x := by + intro x _ + rcases hOr x with hφ | hψ + · simp [Set.indicator, hφ] + · by_cases hφ' : φ x = true + · simp [Set.indicator, hφ', hψ] + · simp [Set.indicator, hφ', hψ] + calc (1 : ℝ≥0∞) + = ∑ x, μ x := (pmf_sum_univ μ).symm + _ ≤ ∑ x, (({w | φ w = true} : Set W).indicator μ x + + ({w | ψ w = true} : Set W).indicator μ x) := + Finset.sum_le_sum hbnd + +end Aristotelian diff --git a/Linglib/Core/Logic/Aristotelian/Square.lean b/Linglib/Core/Logic/Aristotelian/Square.lean new file mode 100644 index 000000000..f43478e71 --- /dev/null +++ b/Linglib/Core/Logic/Aristotelian/Square.lean @@ -0,0 +1,80 @@ +import Linglib.Core.Logic.Aristotelian.Basic + +/-! +# Square of Opposition + +@cite{barwise-cooper-1981} @cite{horn-2001}. The Aristotelian square reified as an +algebraic object: four corners `A`, `E`, `I`, `O` over a Boolean algebra, related +by contradiction (A–O, E–I), contrariety (A–E), subcontrariety (I–O), and +subalternation (A→I, E→O). Concrete instantiations (quantifiers, modals, +attitudes) live in their respective theory modules. +-/ + +namespace Aristotelian + +/-! ### The Square -/ + +/-- The four vertices of a Square of Opposition. -/ +structure Square (α : Type*) where + /-- A-corner: universal affirmative (every, □, Bel p). -/ + A : α + /-- E-corner: universal negative (no, □¬, Bel ¬p). -/ + E : α + /-- I-corner: particular affirmative (some, ◇, ◇p). -/ + I : α + /-- O-corner: particular negative (not-every, ¬□, ¬Bel p). -/ + O : α + deriving Repr + +/-! ### Square relations -/ + +/-- The six relations of the Square over a Boolean algebra. Contradiction +diagonals are the full `IsContradictory`; contrariety/subcontrariety give one +direction (`Disjoint`/`Codisjoint`); subalternations are non-strict (`≤`). The +bridges below recover `IsContrary`/`IsSubaltern` from the missing witness. -/ +structure SquareRelations {α : Type*} [BooleanAlgebra α] (sq : Square α) where + /-- A entails I. -/ + subalternAI : sq.A ≤ sq.I + /-- E entails O. -/ + subalternEO : sq.E ≤ sq.O + /-- A and O are contradictories. -/ + contradAO : IsContradictory sq.A sq.O + /-- E and I are contradictories. -/ + contradEI : IsContradictory sq.E sq.I + /-- A and E are contraries. -/ + contraryAE : Disjoint sq.A sq.E + /-- I and O are subcontraries. -/ + subcontrIO : Codisjoint sq.I sq.O + +/-! ### Bridges to the Aristotelian predicates -/ + +/-- Lift to `IsSubaltern sq.A sq.I` given strictness `sq.A ≠ sq.I`. -/ +theorem SquareRelations.toSubalternAI {α : Type*} [BooleanAlgebra α] {sq : Square α} + (rel : SquareRelations sq) (hne : sq.A ≠ sq.I) : IsSubaltern sq.A sq.I := + lt_of_le_of_ne rel.subalternAI hne + +/-- Lift to `IsContrary sq.A sq.E` given non-exhaustion `sq.A ⊔ sq.E ≠ ⊤`. -/ +theorem SquareRelations.toContraryAE {α : Type*} [BooleanAlgebra α] {sq : Square α} + (rel : SquareRelations sq) (hne : sq.A ⊔ sq.E ≠ ⊤) : IsContrary sq.A sq.E := + ⟨rel.contraryAE, fun hc => hne (codisjoint_iff.mp hc)⟩ + +/-! ### The box-derived square -/ + +/-- The square of propositions from a box-like operator `box`: `A = box p`, +`E = box pᶜ`, `I = (box pᶜ)ᶜ`, `O = (box p)ᶜ`. -/ +def Square.fromBox {α : Type*} [BooleanAlgebra α] (box : α → α) (p : α) : + Square α where + A := box p + E := box pᶜ + I := (box pᶜ)ᶜ + O := (box p)ᶜ + +theorem fromBox_contradAO {α : Type*} [BooleanAlgebra α] (box : α → α) (p : α) : + (Square.fromBox box p).A = (Square.fromBox box p).Oᶜ := by + simp [Square.fromBox] + +theorem fromBox_contradEI {α : Type*} [BooleanAlgebra α] (box : α → α) (p : α) : + (Square.fromBox box p).E = (Square.fromBox box p).Iᶜ := by + simp [Square.fromBox] + +end Aristotelian diff --git a/Linglib/Core/Logic/Opposition/Aristotelian.lean b/Linglib/Core/Logic/Opposition/Aristotelian.lean deleted file mode 100644 index 7edd299b4..000000000 --- a/Linglib/Core/Logic/Opposition/Aristotelian.lean +++ /dev/null @@ -1,207 +0,0 @@ -import Mathlib.Logic.Basic -import Mathlib.Order.BooleanAlgebra.Basic - -/-! -# The four Aristotelian relations @cite{demey-smessaert-2018} - -Per Demey & Smessaert 2018 "Combinatorial Bitstring Semantics for Arbitrary -Logical Fragments" (J Phil Logic 47:325–363), Definition 1. - -Given a logical system `S` with Boolean operators and model-theoretic semantics -`⊨_S`, two formulas φ and ψ stand in one of four *Aristotelian relations*: - -| Relation | Definition | -|----------------|-----------------------------------------------------| -| Contradictory | `⊨ ¬(φ ∧ ψ)` and `⊨ φ ∨ ψ` | -| Contrary | `⊨ ¬(φ ∧ ψ)` and `⊭ φ ∨ ψ` | -| Subcontrary | `⊭ ¬(φ ∧ ψ)` and `⊨ φ ∨ ψ` | -| Subalternation | `⊨ φ → ψ` and `⊭ ψ → φ` | - -The collection `𝒜𝒢_S := {CD_S, C_S, SC_S, SA_S}` is called the *Aristotelian -geometry* of `S`. - -This file formalizes the relations directly over a model class `W` (where each -"formula" is a predicate `W → Bool`). Validity `⊨ φ` becomes `∀ w, φ w = true`. -The four conditions in Definition 1 are pure Boolean conditions on truth -values, and the universal closure over `W` is the standard model-theoretic -gloss of `⊨_S`, so this representation is faithful. (Demey-Smessaert's -Lemma 1, p. 329, separately establishes that every Boolean isomorphism is an -Aristotelian isomorphism — this is the *transfer* property exploited in -`Bitstring.lean`'s Theorem 2, not a justification of the encoding here.) - -## Generality - -Three layers of generality, each downstream of the previous: - -1. **`AristotelianRel`** (this file) — relations over a model class `W` with - formulas as `W → Bool` predicates. Sufficient for instantiating any - concrete logical system: classical logic, modal logic, GQ theory, etc. - -2. **`Diagram`** (`Diagram.lean`) — labeled-poset structure with a finite - indexed family of formulas and the relation matrix between them. Squares, - hexagons, cubes, n-cubes are all `Diagram` specializations. - -3. **`BitstringSemantics`** (`Bitstring.lean`) — the partition-based bitstring - representation that makes Aristotelian structure transparent (Thm 1–2). - -Probabilistic generalization lives in `Probabilistic.lean`. --/ - -namespace Core.Opposition - -variable {W : Type*} - -/-- The four Aristotelian relations as a single inductive label. - Used by `Diagram.relation` to label edges. -/ -inductive AristotelianRel where - | contradictory - | contrary - | subcontrary - | subaltern -- φ → ψ direction (asymmetric: A is *sub*altern to ψ here means φ ⊨ ψ) - | unconnected - deriving DecidableEq, Repr, Inhabited - --- ============================================================================ --- §1. The four relations as predicates --- ============================================================================ - -/-- `Contradictory φ ψ`: `φ ∧ ψ` is unsatisfiable AND `φ ∨ ψ` is valid. - Equivalently, exactly one of φ, ψ is true at each world. -/ -def Contradictory (φ ψ : W → Bool) : Prop := - (∀ w, ¬ (φ w = true ∧ ψ w = true)) ∧ (∀ w, φ w = true ∨ ψ w = true) - -/-- `Contrary φ ψ`: cannot both be true, but can both be false. - `φ ∧ ψ` is unsatisfiable AND `φ ∨ ψ` is not valid. -/ -def Contrary (φ ψ : W → Bool) : Prop := - (∀ w, ¬ (φ w = true ∧ ψ w = true)) ∧ ¬ (∀ w, φ w = true ∨ ψ w = true) - -/-- `Subcontrary φ ψ`: cannot both be false, but can both be true. - `φ ∧ ψ` is satisfiable AND `φ ∨ ψ` is valid. -/ -def Subcontrary (φ ψ : W → Bool) : Prop := - ¬ (∀ w, ¬ (φ w = true ∧ ψ w = true)) ∧ (∀ w, φ w = true ∨ ψ w = true) - -/-- `Subaltern φ ψ`: `φ` entails `ψ` but not conversely. - Asymmetric: `Subaltern φ ψ` ≠ `Subaltern ψ φ` in general. -/ -def Subaltern (φ ψ : W → Bool) : Prop := - (∀ w, φ w = true → ψ w = true) ∧ ¬ (∀ w, ψ w = true → φ w = true) - -/-- `Unconnected φ ψ`: φ and ψ stand in NO Aristotelian relation. They are - "logically independent" in the Aristotelian sense — all four truth - combinations are realized. Per Smessaert & Demey 2014. -/ -def Unconnected (φ ψ : W → Bool) : Prop := - (∃ w, φ w = true ∧ ψ w = true) ∧ - (∃ w, φ w = true ∧ ψ w = false) ∧ - (∃ w, φ w = false ∧ ψ w = true) ∧ - (∃ w, φ w = false ∧ ψ w = false) - --- ============================================================================ --- §2. Symmetry properties --- ============================================================================ - -/-- Contradictoriness is symmetric. -/ -theorem Contradictory.symm {φ ψ : W → Bool} (h : Contradictory φ ψ) : - Contradictory ψ φ := by - refine ⟨fun w hand => h.1 w ⟨hand.2, hand.1⟩, fun w => ?_⟩ - rcases h.2 w with hφ | hψ - · exact Or.inr hφ - · exact Or.inl hψ - -/-- Contrariety is symmetric. -/ -theorem Contrary.symm {φ ψ : W → Bool} (h : Contrary φ ψ) : - Contrary ψ φ := by - refine ⟨fun w hand => h.1 w ⟨hand.2, hand.1⟩, ?_⟩ - intro hOr; apply h.2; intro w - rcases hOr w with hψ | hφ - · exact Or.inr hψ - · exact Or.inl hφ - -/-- Subcontrariety is symmetric. -/ -theorem Subcontrary.symm {φ ψ : W → Bool} (h : Subcontrary φ ψ) : - Subcontrary ψ φ := by - refine ⟨?_, fun w => ?_⟩ - · intro hAnd; apply h.1; intro w hwand - exact hAnd w ⟨hwand.2, hwand.1⟩ - · rcases h.2 w with hφ | hψ - · exact Or.inr hφ - · exact Or.inl hψ - --- (Subaltern is not symmetric; that's the point.) - --- ============================================================================ --- §3. Classification (mutual exclusion) --- ============================================================================ - -/-- Per Demey & Smessaert §2.1, the four Aristotelian relations are mutually - exclusive: any pair of formulas stands in at most one relation (or in - none, in which case they are `Unconnected`). -/ -theorem contradictory_not_contrary {φ ψ : W → Bool} - (hCD : Contradictory φ ψ) : ¬ Contrary φ ψ := by - intro hC; exact hC.2 hCD.2 - -theorem contradictory_not_subcontrary {φ ψ : W → Bool} - (hCD : Contradictory φ ψ) : ¬ Subcontrary φ ψ := fun hSC => hSC.1 hCD.1 - -theorem contrary_not_subcontrary {φ ψ : W → Bool} - (hC : Contrary φ ψ) : ¬ Subcontrary φ ψ := fun hSC => hSC.1 hC.1 - --- ============================================================================ --- §4. BA-generic Aristotelian relations (Prop↔Bool gap closure) --- ============================================================================ - -/-! The four Aristotelian relations are purely algebraic — they are statements -about `⊓`, `⊔`, `⊥`, `⊤` in a Boolean algebra. The model-theoretic forms -above (specialized to `W → Bool` predicates) are concrete instances; the -BA-generic forms below provide a unified API that works for both `W → Bool` -and `W → Prop` predicates (and `Set W`, propositional fragments, sub-σ-algebras -of measurable sets, etc.) via `Pi.instBooleanAlgebra` or other BA instances. - -**Why this matters**: closes the architectural gap identified in the audit -between this file's `W → Bool` predicates and `Semantics/ -Quantification/Quantifier.lean`'s `(F.Entity → Prop)`-valued GQ semantics -(plus the 5 modality `theorem duality`s, BC1981 §8 GQ duality, etc.). All -those Prop-valued statements can now instantiate the same BA-generic -predicates via `Pi.instBooleanAlgebra` for `Prop`. -/ - -section Algebraic -variable {α : Type*} [BooleanAlgebra α] - -/-- BA-generic contradictoriness: `φ ⊓ ψ = ⊥` and `φ ⊔ ψ = ⊤`. The two - elements are jointly impossible AND exhaustive. In any Boolean algebra - this is equivalent to `ψ = φᶜ` (uniqueness of complement). -/ -def IsContradictory (φ ψ : α) : Prop := φ ⊓ ψ = ⊥ ∧ φ ⊔ ψ = ⊤ - -/-- BA-generic contrariety: `φ ⊓ ψ = ⊥` (jointly impossible) but - `φ ⊔ ψ ≠ ⊤` (not jointly exhaustive — both can be false). -/ -def IsContrary (φ ψ : α) : Prop := φ ⊓ ψ = ⊥ ∧ φ ⊔ ψ ≠ ⊤ - -/-- BA-generic subcontrariety: `φ ⊓ ψ ≠ ⊥` (can both be true) AND - `φ ⊔ ψ = ⊤` (jointly exhaustive — at least one must be true). -/ -def IsSubcontrary (φ ψ : α) : Prop := φ ⊓ ψ ≠ ⊥ ∧ φ ⊔ ψ = ⊤ - -/-- BA-generic *proper* subalternation: `φ ≤ ψ` (entailment) but `φ ≠ ψ` - (strictly stronger). -/ -def IsSubaltern (φ ψ : α) : Prop := φ ≤ ψ ∧ φ ≠ ψ - -end Algebraic - --- ============================================================================ --- §5. Bridges to model-theoretic forms (deferred — see docstring) --- ============================================================================ - -/-! Bridge `iff` lemmas connecting `IsContradictory`/`IsSubaltern`/etc. for -the Pi-instances `W → Bool` and `W → Prop` to the model-theoretic conventions -those predicate spaces commonly use (existential/universal quantification over -worlds with `= true` checks for Bool, direct conjunctive/disjunctive form for -Prop) are deferred to a follow-on. The `iff`s are routine but Lean-fiddly -(many `Pi.inf_apply` / `Pi.bot_apply` rewrites + Bool/Prop case analysis) — -each one easily 15-20 LOC, 8 lemmas total ≈ ~140 LOC. - -For now, the gap is closed at the *type* level: `IsContradictory` works -uniformly for any `[BooleanAlgebra α]`, and consumers that want to use it on -`W → Bool` or `W → Prop` predicates can do so directly via the Pi-instance -without going through a model-theoretic intermediary. The model-theoretic -forms above (`Contradictory`/`Contrary`/`Subaltern`/`Subcontrary`/`Unconnected` -specialized to `W → Bool`) remain valid; bridges land when consumer demand -materializes. -/ - -end Core.Opposition diff --git a/Linglib/Core/Logic/Opposition/Atoms.lean b/Linglib/Core/Logic/Opposition/Atoms.lean deleted file mode 100644 index d9ea4aba3..000000000 --- a/Linglib/Core/Logic/Opposition/Atoms.lean +++ /dev/null @@ -1,140 +0,0 @@ -import Mathlib.Order.BooleanSubalgebra -import Mathlib.Order.Atoms - -/-! -# Anchor formulas in a Boolean algebra: Lemma 6 of @cite{demey-smessaert-2018} - -For a finite generator set `s : Finset α` of a Boolean algebra `α`, an -*anchor formula* is a meet of literals over `s` — one literal `lit φ b` -per generator, with polarity selected by an assignment `σ : s → Bool`: - - anchorBA s σ := ⨅ x ∈ s, (if σ x then x else xᶜ) - -The central technical lemma (Demey-Smessaert §3, Lemma 6) is *anchor- -decidedness*: for every element `ψ` of the Boolean closure of `s`, every -anchor formula either entails `ψ` or entails `¬ψ`. Equivalently, the anchor -formulas partition the closure's "truth space" into mutually-deciding cells. - -Lemma 6 is the engine driving the bitstring representation in `Bitstring.lean`: -the i-th bit of `bitstringOf φ ψ` is well-defined precisely because the i-th -anchor decides ψ. Closing Theorems 1 and 2 from `Bitstring.lean` reduces to -this lemma plus mathlib's existing infrastructure. - -## What this file uses from mathlib - -- `BooleanSubalgebra` (Yaël Dillies, 2024) for `closure`-based reasoning -- `closure_bot_sup_induction` for the inductive proof of Lemma 6 -- Standard `BooleanAlgebra` API (`compl_sup`, `compl_compl`, `le_inf`, ...) - -## Generality - -The lemma is stated for an arbitrary `[BooleanAlgebra α]`. Specializations to -`α = W → Bool` (the syllogistic case) are immediate. --/ - -namespace Core.Opposition - -variable {α : Type*} [BooleanAlgebra α] - --- ============================================================================ --- §1. Literals and anchor formulas --- ============================================================================ - -/-- A *literal* over a generator `φ : α`: either `φ` itself (positive polarity) - or its complement `φᶜ` (negative polarity). -/ -def lit (φ : α) (b : Bool) : α := if b then φ else φᶜ - -@[simp] lemma lit_true (φ : α) : lit φ true = φ := rfl -@[simp] lemma lit_false (φ : α) : lit φ false = φᶜ := rfl - -/-- The *anchor formula* for a polarity assignment `σ : s → Bool` over a - finite generator set `s : Finset α`: the meet of `lit x (σ x)` over all - `x ∈ s`. This is a generic Boolean-algebra version of the Demey-Smessaert - anchor (Definition 5). -/ -def anchorBA (s : Finset α) (σ : s → Bool) : α := - s.attach.inf (fun x => lit x.val (σ x)) - -/-- The anchor lies below each of its constituent literals. -/ -lemma anchorBA_le_lit (s : Finset α) (σ : s → Bool) (x : s) : - anchorBA s σ ≤ lit x.val (σ x) := - Finset.inf_le (s.mem_attach x) - -/-- A specific positive-polarity case: if `σ x = true`, then `anchorBA s σ ≤ x`. -/ -lemma anchorBA_le_of_pos {s : Finset α} {σ : s → Bool} {x : s} (h : σ x = true) : - anchorBA s σ ≤ x.val := by - have := anchorBA_le_lit s σ x - rwa [lit, if_pos h] at this - -/-- A specific negative-polarity case: if `σ x = false`, then `anchorBA s σ ≤ xᶜ`. -/ -lemma anchorBA_le_compl_of_neg {s : Finset α} {σ : s → Bool} {x : s} - (h : σ x = false) : anchorBA s σ ≤ x.valᶜ := by - have hLit := anchorBA_le_lit s σ x - rw [lit, h] at hLit - exact hLit - --- ============================================================================ --- §2. Lemma 6 — anchor-decidedness for closure elements --- ============================================================================ - -/-- **Lemma 6 (Demey & Smessaert 2018)**: every element of the Boolean closure - of a finite generator set is *anchor-decided* — every anchor formula either - entails it or entails its complement. - - This holds **unconditionally** (no consistency hypothesis on the anchor): - if the anchor is `⊥`, both disjuncts hold trivially. The bitstring - semantics in `Bitstring.lean` uses Lemma 6 with the anchor known to be - nonzero (i.e., σ in the partition), giving the *exclusive* decidedness - that makes each bit well-defined. - - Proof: induction on closure membership via `closure_bot_sup_induction`. - - `mem`: anchor includes `lit x (σ x)` as a meet; sign of `σ x` decides. - - `bot`: `anchor ≤ ⊥ᶜ = ⊤` trivially. - - `sup`: case on which side of the disjunction the anchor sits below. - - `compl`: flip the disjunction (`compl_compl`). -/ -theorem anchorBA_le_or_le_compl_mem_closure - {s : Finset α} (σ : s → Bool) {ψ : α} - (hψ : ψ ∈ BooleanSubalgebra.closure (s : Set α)) : - anchorBA s σ ≤ ψ ∨ anchorBA s σ ≤ ψᶜ := by - induction hψ using BooleanSubalgebra.closure_bot_sup_induction with - | mem ψ' hψ' => - -- ψ' ∈ s; the anchor includes lit ⟨ψ', hψ'⟩ (σ ⟨ψ', hψ'⟩) as a meet - by_cases h : σ ⟨ψ', hψ'⟩ = true - · left - have := anchorBA_le_of_pos (s := s) (σ := σ) (x := ⟨ψ', hψ'⟩) h - simpa using this - · right - have hf : σ ⟨ψ', hψ'⟩ = false := Bool.eq_false_iff.mpr h - have := anchorBA_le_compl_of_neg (s := s) (σ := σ) (x := ⟨ψ', hψ'⟩) hf - simpa using this - | bot => - right - simp - | sup x _ y _ ihx ihy => - rcases ihx with hx | hx - · left; exact hx.trans le_sup_left - rcases ihy with hy | hy - · left; exact hy.trans le_sup_right - · right; rw [compl_sup]; exact le_inf hx hy - | compl x _ ih => - rcases ih with h | h - · right; rw [compl_compl]; exact h - · left; exact h - -/-- The *exclusive* form: for a consistent anchor, exactly one disjunct of - Lemma 6 holds. (If both held, anchor would be below `ψ ⊓ ψᶜ = ⊥`.) -/ -theorem anchorBA_le_or_le_compl_exclusive {s : Finset α} (σ : s → Bool) {ψ : α} - (hψ : ψ ∈ BooleanSubalgebra.closure (s : Set α)) - (hCons : anchorBA s σ ≠ ⊥) : - (anchorBA s σ ≤ ψ ∧ ¬ anchorBA s σ ≤ ψᶜ) ∨ - (¬ anchorBA s σ ≤ ψ ∧ anchorBA s σ ≤ ψᶜ) := by - rcases anchorBA_le_or_le_compl_mem_closure σ hψ with hL | hR - · left - refine ⟨hL, fun hR => hCons ?_⟩ - have : anchorBA s σ ≤ ψ ⊓ ψᶜ := le_inf hL hR - rwa [inf_compl_eq_bot, le_bot_iff] at this - · right - refine ⟨fun hL => hCons ?_, hR⟩ - have : anchorBA s σ ≤ ψ ⊓ ψᶜ := le_inf hL hR - rwa [inf_compl_eq_bot, le_bot_iff] at this - -end Core.Opposition diff --git a/Linglib/Core/Logic/Opposition/Bitstring.lean b/Linglib/Core/Logic/Opposition/Bitstring.lean deleted file mode 100644 index 6d0a8c9df..000000000 --- a/Linglib/Core/Logic/Opposition/Bitstring.lean +++ /dev/null @@ -1,675 +0,0 @@ -import Linglib.Core.Logic.Opposition.Partition -import Linglib.Core.Logic.Opposition.Atoms -import Mathlib.Data.Fintype.Order -import Mathlib.Order.BooleanSubalgebra - -/-! -# Bitstring semantics for logical fragments (skeleton) - -Per @cite{demey-smessaert-2018} §3.2, Definition 7 and Theorems 1–2. - -Given a fragment `ℱ` with partition `Π_S(ℱ) = {α_1, ..., α_n}`, the bitstring -semantics `β_S^ℱ : 𝔹(ℱ) → BitVec n` assigns each formula in the Boolean -closure of ℱ a bitstring whose `i`-th position is `1` iff the anchor -formula `α_i` entails it: - - [β_S^ℱ(φ)]_i := 1 iff ⊨_S α_i → φ - -**Theorem 1**: `β_S^ℱ` is a Boolean-algebra isomorphism. -**Theorem 2**: `β_S^ℱ` is therefore an Aristotelian isomorphism (Lemma 1). - -The Aristotelian relations on bitstrings (Definition 2) are bitwise: - -| Relation | Bitstring condition | -|----------------|------------------------------| -| Contradictory | `b₁ ∧ b₂ = 0` and `b₁ ∨ b₂ = 1` | -| Contrary | `b₁ ∧ b₂ = 0` and `b₁ ∨ b₂ ≠ 1` | -| Subcontrary | `b₁ ∧ b₂ ≠ 0` and `b₁ ∨ b₂ = 1` | -| Subaltern | `b₁ ∧ b₂ = b₁` and `b₁ ∨ b₂ ≠ b₁` | - -## What's here - -- `bitstringOf φ ψ` — Definition 7 (the bit at index `i` says whether anchor - `α_i` entails `ψ`) -- `BitContradictory`/`BitContrary`/`BitSubcontrary`/`BitSubaltern` — - Definition 2 (Aristotelian relations on bitstrings) -- `bitstringOf_orderIso : closure (Set.range φ) ≃o (Fin n → Bool)` — - **Theorem 1** (Boolean-algebra isomorphism), §11 -- `contradictory_iff_bitContradictory` and three siblings — **Theorem 2** - (Aristotelian relations transfer), §10 --/ - -namespace Core.Opposition - -variable {W : Type*} [Fintype W] - --- ============================================================================ --- §1. Bitstring representation (Definition 7) --- ============================================================================ - -/-- Index a Finset by a Fin, giving each anchor formula a positional index. - The choice of indexing is arbitrary up to permutation; downstream - Aristotelian relations are invariant under it. -/ -private noncomputable def anchorIndex {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) : - Fin (partition ι W φ).card → (ι → Bool) := - fun i => ((partition ι W φ).equivFin.symm i).val - -/-- The bitstring of a Boolean predicate `ψ` relative to a fragment `φ`: - bit `i` is `true` iff anchor formula `i` entails `ψ`. -/ -noncomputable def bitstringOf {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (ψ : W → Bool) : - Fin (partition ι W φ).card → Bool := - fun i => decide (∀ w, anchor φ (anchorIndex φ i) w = true → ψ w = true) - --- ============================================================================ --- §2. Aristotelian relations on bitstrings (Definition 2) --- ============================================================================ - -/-- Bitwise AND. -/ -def bitAnd {n : ℕ} (b₁ b₂ : Fin n → Bool) : Fin n → Bool := - fun i => b₁ i && b₂ i - -/-- Bitwise OR. -/ -def bitOr {n : ℕ} (b₁ b₂ : Fin n → Bool) : Fin n → Bool := - fun i => b₁ i || b₂ i - -/-- All-zeros bitstring. -/ -def zeros (n : ℕ) : Fin n → Bool := fun _ => false - -/-- All-ones bitstring. -/ -def ones (n : ℕ) : Fin n → Bool := fun _ => true - -@[simp] lemma bitAnd_apply {n : ℕ} (b₁ b₂ : Fin n → Bool) (i : Fin n) : - bitAnd b₁ b₂ i = (b₁ i && b₂ i) := rfl - -@[simp] lemma bitOr_apply {n : ℕ} (b₁ b₂ : Fin n → Bool) (i : Fin n) : - bitOr b₁ b₂ i = (b₁ i || b₂ i) := rfl - -@[simp] lemma zeros_apply {n : ℕ} (i : Fin n) : zeros n i = false := rfl - -@[simp] lemma ones_apply {n : ℕ} (i : Fin n) : ones n i = true := rfl - -/-- Bitstring contradictoriness: `b₁ ∧ b₂ = 0` and `b₁ ∨ b₂ = 1`. -/ -def BitContradictory {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop := - bitAnd b₁ b₂ = zeros n ∧ bitOr b₁ b₂ = ones n - -/-- Bitstring contrariety: `b₁ ∧ b₂ = 0` and `b₁ ∨ b₂ ≠ 1`. -/ -def BitContrary {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop := - bitAnd b₁ b₂ = zeros n ∧ bitOr b₁ b₂ ≠ ones n - -/-- Bitstring subcontrariety: `b₁ ∧ b₂ ≠ 0` and `b₁ ∨ b₂ = 1`. -/ -def BitSubcontrary {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop := - bitAnd b₁ b₂ ≠ zeros n ∧ bitOr b₁ b₂ = ones n - -/-- Bitstring subalternation: `b₁ ⊆ b₂` (bitwise ≤) and not equal. -/ -def BitSubaltern {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop := - bitAnd b₁ b₂ = b₁ ∧ bitOr b₁ b₂ ≠ b₁ - --- ============================================================================ --- §3. Forward Aristotelian transfer (partial — what goes through without closure) --- ============================================================================ - -/-- The anchor at position `i` is consistent: there exists a world satisfying it. - Extracted from the `partition` Finset's filter membership. -/ -private theorem anchorIndex_consistent {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (i : Fin (partition ι W φ).card) : - ∃ w, anchor φ (anchorIndex φ i) w = true := by - classical - have hMem : ((partition ι W φ).equivFin.symm i).val ∈ partition ι W φ := - ((partition ι W φ).equivFin.symm i).property - unfold partition at hMem - rw [Finset.mem_filter] at hMem - simpa [anchorIndex] using hMem.2 - -/-- **Forward direction of Theorem 2 (bitAnd half)**: Boolean contradictoriness - of two arbitrary `W → Bool` predicates implies their bitstrings have empty - bitwise-AND. This direction goes through without Boolean-closure - infrastructure — only the partition's anchor-consistency matters. - - The reverse direction (`BitContradictory → Contradictory`) and the - bitOr-direction (`Contradictory → bitOr = ones`) require the Boolean-closure - precondition (Demey-Smessaert §3, Lemma 6: every `φ ∈ 𝔹(ℱ)` is - anchor-decided), which would in turn need Theorem 1's Boolean-algebra - structure on `𝔹(ℱ)`. -/ -theorem bitAnd_bitstringOf_eq_zeros_of_contradictory - {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (h : Contradictory ψ₁ ψ₂) : - bitAnd (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = zeros _ := by - funext i - unfold bitAnd zeros - obtain ⟨w, hw⟩ := anchorIndex_consistent φ i - by_cases h1 : bitstringOf φ ψ₁ i = true - · by_cases h2 : bitstringOf φ ψ₂ i = true - · exfalso - unfold bitstringOf at h1 h2 - rw [decide_eq_true_eq] at h1 h2 - exact h.1 w ⟨h1 w hw, h2 w hw⟩ - · simp [h1, h2] - · simp [h1] - --- ============================================================================ --- §4. Bridge: `anchor` in the `W → Bool` BooleanAlgebra --- ============================================================================ - -/-- Pointwise reduction of `≤` in `W → Bool`: `f ≤ g` iff `f w = true → g w = true` - everywhere. Standard `Pi.le_def` instantiation for `Bool`-valued functions. -/ -private lemma le_iff_pointwise_imp {f g : W → Bool} : - f ≤ g ↔ ∀ w, f w = true → g w = true := by - rw [Pi.le_def] - refine forall_congr' fun w => ?_ - cases f w <;> cases g w <;> simp <;> decide - -/-- Lemma 6 specialized to our indexed-family `anchor`: every `ψ` in the Boolean - closure of `Set.range φ` is anchor-decided. Direct induction on closure. - - **Note**: `Atoms.lean::anchorBA_le_or_le_compl_mem_closure` proves the same - statement for the BA-generic `anchorBA s σ` form (`s : Finset α`, `σ : s → Bool`). - The two are not directly bridged: the bridge would require `Finset.image φ` - to collapse duplicate generators and a corresponding choice of polarity per - duplicate-class — adding case analysis that exceeds the cost of just - reproving the specialized form here. The structural proof (induction on - `closure_bot_sup_induction`) is the same in both files; if either changes, - so does the other. -/ -theorem anchor_le_or_le_compl_mem_closure - {ι : Type} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) {ψ : W → Bool} - (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) : - anchor φ σ ≤ ψ ∨ anchor φ σ ≤ ψᶜ := by - induction hψ using BooleanSubalgebra.closure_bot_sup_induction with - | mem ψ' hψ' => - obtain ⟨i, rfl⟩ := hψ' - by_cases h : σ i = true - · left - rw [le_iff_pointwise_imp] - intro w hw - unfold anchor at hw - rw [decide_eq_true_eq] at hw - have := hw i - rw [if_pos h] at this - exact this - · right - rw [le_iff_pointwise_imp] - intro w hw - have hf : σ i = false := Bool.eq_false_iff.mpr h - unfold anchor at hw - rw [decide_eq_true_eq] at hw - have := hw i - rw [if_neg h] at this - simp [this] - | bot => - right - rw [le_iff_pointwise_imp] - intro w _ - rfl - | sup x _ y _ ihx ihy => - rcases ihx with hx | hx - · left; exact hx.trans le_sup_left - rcases ihy with hy | hy - · left; exact hy.trans le_sup_right - · right; rw [compl_sup]; exact le_inf hx hy - | compl x _ ih => - rcases ih with h | h - · right; rw [compl_compl]; exact h - · left; exact h - --- §5. Theorem 1 statement is now `bitstringOf_orderIso` in §11 (the full --- bidirectional Boolean-algebra isomorphism). The supporting infrastructure --- (master bridge, anchor_mem_closure, bitstringInverse, round trips) is --- built up in §6-§10 below. - --- ============================================================================ --- §6. Master bridge: bitstringOf at a world equals ψ at that world --- ============================================================================ - -/-- **The bridge lemma**: for any `ψ` in the Boolean closure and any world `w` - that satisfies the anchor at index `i`, the bit `bitstringOf φ ψ i` equals - `ψ w`. This is the well-definedness of the bitstring representation: - Lemma 6 (anchor-decidedness) plus consistency means every anchor-witness - world agrees on `ψ`'s truth value, so the bit is unambiguous. - - All four Aristotelian-relation theorems below are corollaries of this - lemma + partition exhaustion. -/ -theorem bitstringOf_eq_apply_at_anchor - {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {ψ : W → Bool} - (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) - (i : Fin (partition ι W φ).card) {w : W} - (hw : anchor φ (anchorIndex φ i) w = true) : - bitstringOf φ ψ i = ψ w := by - rcases anchor_le_or_le_compl_mem_closure φ (anchorIndex φ i) hψ with hL | hR - · -- anchor ≤ ψ: both bit and ψ w are true - have hβ : bitstringOf φ ψ i = true := by - unfold bitstringOf - rw [decide_eq_true_eq] - exact fun w' hw' => (le_iff_pointwise_imp.mp hL) w' hw' - have hψw : ψ w = true := (le_iff_pointwise_imp.mp hL) w hw - rw [hβ, hψw] - · -- anchor ≤ ψᶜ: both bit and ψ w are false - have hψw : ψ w = false := by - have := (le_iff_pointwise_imp.mp hR) w hw - simpa using this - have hβ : bitstringOf φ ψ i = false := by - cases hb : bitstringOf φ ψ i - · rfl - · exfalso - unfold bitstringOf at hb - rw [decide_eq_true_eq] at hb - rw [hb w hw] at hψw - exact Bool.noConfusion hψw - rw [hβ, hψw] - -/-- For each world, the index of an anchor it satisfies (chosen via Classical - on `anchor_jointly_exhaustive`). Composes with `bitstringOf_eq_apply_at_anchor` - to give `bitstringOf φ ψ (worldAnchorIndex φ w) = ψ w`. -/ -noncomputable def worldAnchorIndex {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (w : W) : Fin (partition ι W φ).card := - let σ := Classical.choose (anchor_jointly_exhaustive φ w) - let hσ := Classical.choose_spec (anchor_jointly_exhaustive φ w) - (partition ι W φ).equivFin ⟨σ, by - unfold partition - rw [Finset.mem_filter] - exact ⟨Finset.mem_univ _, decide_eq_true ⟨w, hσ⟩⟩⟩ - -/-- The anchor at `worldAnchorIndex φ w` is satisfied by `w`. -/ -theorem anchor_worldAnchorIndex {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (w : W) : - anchor φ (anchorIndex φ (worldAnchorIndex φ w)) w = true := by - unfold worldAnchorIndex anchorIndex - simp only [Equiv.symm_apply_apply] - exact Classical.choose_spec (anchor_jointly_exhaustive φ w) - -/-- **The world-side bridge**: at any world, `bitstringOf φ ψ` evaluated at - that world's anchor index returns `ψ` at that world. Direct corollary of - `bitstringOf_eq_apply_at_anchor` + `anchor_worldAnchorIndex`. -/ -theorem bitstringOf_apply_at_world - {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {ψ : W → Bool} - (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) (w : W) : - bitstringOf φ ψ (worldAnchorIndex φ w) = ψ w := - bitstringOf_eq_apply_at_anchor φ hψ _ (anchor_worldAnchorIndex φ w) - -/-- **Theorem 1's injectivity half**: `bitstringOf φ` is injective on the - Boolean closure. Two formulas in the closure with the same bitstring - representation agree at every world. - - One-line proof: at each `w`, `ψ_j w = bitstringOf φ ψ_j (worldAnchorIndex φ w)` - for both `j ∈ {1, 2}`, and the bitstrings are equal by hypothesis. -/ -theorem bitstringOf_injOn_closure - {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : - Set.InjOn (bitstringOf φ) - (BooleanSubalgebra.closure (Set.range φ) : Set (W → Bool)) := by - intro ψ₁ hψ₁ ψ₂ hψ₂ hEq - funext w - rw [← bitstringOf_apply_at_world φ hψ₁ w, hEq, bitstringOf_apply_at_world φ hψ₂ w] - --- ============================================================================ --- §7. anchor formulas live in the closure (the surjectivity prerequisite) --- ============================================================================ - -/-- A literal `lit (φ i) (σ i)` (positive when `σ i = true`, negative otherwise) - lies in the Boolean closure of `Set.range φ`. -/ -private theorem lit_mem_closure {ι : Type} [Fintype ι] - (φ : ι → W → Bool) (σ : ι → Bool) (i : ι) : - (if σ i then φ i else (φ i)ᶜ) ∈ - BooleanSubalgebra.closure (Set.range φ) := by - by_cases h : σ i = true - · simp only [h, ↓reduceIte] - exact BooleanSubalgebra.subset_closure ⟨i, rfl⟩ - · have hf : σ i = false := Bool.eq_false_iff.mpr h - simp only [hf, Bool.false_eq_true, ↓reduceIte] - exact BooleanSubalgebra.compl_mem (BooleanSubalgebra.subset_closure ⟨i, rfl⟩) - -/-- The "anchor over a Finset" form of our `anchor` predicate. Used as the - induction target for `anchor_mem_closure` — the bridge from `decide (∀ i : ι, ...)` - to a Finset-indexed conjunction. -/ -private def anchorOnFinset {ι : Type} [DecidableEq ι] - (φ : ι → W → Bool) (σ : ι → Bool) (s : Finset ι) : W → Bool := - fun w => decide (∀ i ∈ s, if σ i then φ i w = true else φ i w = false) - -/-- The empty-Finset anchor is `⊤` (vacuously true). -/ -private theorem anchorOnFinset_empty {ι : Type} [DecidableEq ι] - (φ : ι → W → Bool) (σ : ι → Bool) : - anchorOnFinset φ σ ∅ = (⊤ : W → Bool) := by - funext w - simp [anchorOnFinset] - -/-- Insert step: the anchor over `insert i s` decomposes as the anchor over `s` - meet the literal at `i`. -/ -private theorem anchorOnFinset_insert {ι : Type} [DecidableEq ι] - (φ : ι → W → Bool) (σ : ι → Bool) (i : ι) (s : Finset ι) : - anchorOnFinset φ σ (insert i s) = - anchorOnFinset φ σ s ⊓ (if σ i then φ i else (φ i)ᶜ) := by - funext w - show decide _ = _ - -- Use decide_eq_decide to lift the bounded-forall iff under decide - rw [decide_eq_decide.mpr (Finset.forall_mem_insert (s := s) (a := i) - (p := fun j => if σ j then φ j w = true else φ j w = false))] - rw [Bool.decide_and, Bool.and_comm] - -- Evaluate Pi-inf at w: (a ⊓ b) w = a w && b w - rw [Pi.inf_apply] - -- Now both sides are && of two Bool atoms - congr 1 - cases hi : σ i <;> simp [hi] - -/-- The Finset-indexed anchor lies in the Boolean closure, by induction on the - Finset. Used to prove `anchor_mem_closure` for the Fintype.univ case. -/ -private theorem anchorOnFinset_mem_closure {ι : Type} [DecidableEq ι] [Fintype ι] - (φ : ι → W → Bool) (σ : ι → Bool) (s : Finset ι) : - anchorOnFinset φ σ s ∈ BooleanSubalgebra.closure (Set.range φ) := by - induction s using Finset.induction_on with - | empty => - rw [anchorOnFinset_empty] - exact (BooleanSubalgebra.closure (Set.range φ)).top_mem - | insert i s his ih => - rw [anchorOnFinset_insert φ σ i s] - exact (BooleanSubalgebra.closure (Set.range φ)).infClosed' ih - (lit_mem_closure φ σ i) - -/-- **Anchor formulas live in the Boolean closure.** This is the key Layer-3 - bridge: our `decide (∀ i : ι, ...)` form of `anchor` (from `Partition.lean`) - matches the Finset-indexed anchor over `Finset.univ`, which lives in the - closure by induction. -/ -theorem anchor_mem_closure {ι : Type} [DecidableEq ι] [Fintype ι] - (φ : ι → W → Bool) (σ : ι → Bool) : - anchor φ σ ∈ BooleanSubalgebra.closure (Set.range φ) := by - have hEq : anchor φ σ = anchorOnFinset φ σ Finset.univ := by - funext w - unfold anchor anchorOnFinset - congr 1 - exact propext ⟨fun h i _ => h i, fun h i => h i (Finset.mem_univ i)⟩ - rw [hEq] - exact anchorOnFinset_mem_closure φ σ Finset.univ - --- ============================================================================ --- §8. The inverse: bitstringInverse and round trips --- ============================================================================ - -/-- The inverse of `bitstringOf` on the Boolean closure: takes a bitstring `b` - to the Boolean-algebra supremum of those anchor formulas whose bit is `true`. - The result lies in the closure (sup of closure elements via `iSup_mem`). -/ -noncomputable def bitstringInverse {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : W → Bool := - ⨆ i, (if b i then anchor φ (anchorIndex φ i) else (⊥ : W → Bool)) - -theorem bitstringInverse_mem_closure {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : - bitstringInverse φ b ∈ BooleanSubalgebra.closure (Set.range φ) := by - unfold bitstringInverse - apply BooleanSubalgebra.iSup_mem - intro i - by_cases h : b i = true - · simp only [h, ↓reduceIte] - exact anchor_mem_closure φ _ - · have hf : b i = false := Bool.eq_false_iff.mpr h - simp only [hf, Bool.false_eq_true, ↓reduceIte] - exact (BooleanSubalgebra.closure (Set.range φ)).bot_mem - -/-- `anchorIndex` is injective: distinct indices give distinct polarity - assignments (since `equivFin.symm` is a bijection from `Fin n` to a subtype). -/ -private theorem anchorIndex_injective {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) : - Function.Injective (anchorIndex φ) := by - intro i j h - unfold anchorIndex at h - exact (partition ι W φ).equivFin.symm.injective (Subtype.ext h) - -/-- **Uniqueness of anchor at a world**: at each world, the anchor at any - consistent index that holds at the world is *uniquely* this index. Combines - `anchor_mutually_exclusive` (Partition) with `anchorIndex_injective`. -/ -private theorem anchor_at_world_unique - {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {i j : Fin (partition ι W φ).card} {w : W} - (hi : anchor φ (anchorIndex φ i) w = true) - (hj : anchor φ (anchorIndex φ j) w = true) : - i = j := by - by_contra hne - apply anchor_mutually_exclusive φ (anchorIndex φ i) (anchorIndex φ j) - (fun heq => hne (anchorIndex_injective φ heq)) w - exact ⟨hi, hj⟩ - -/-- **The bitstringInverse-evaluation lemma**: at a world `w` satisfying the - anchor at index `j`, the inverse bitstring evaluates to the `j`-th bit. - Heart of both round trips: shows that the `iSup` collapses to a single - summand (the one at `j`) by uniqueness of the satisfied anchor. -/ -theorem bitstringInverse_apply_at_anchor - {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) - (j : Fin (partition ι W φ).card) {w : W} - (hw : anchor φ (anchorIndex φ j) w = true) : - bitstringInverse φ b w = b j := by - unfold bitstringInverse - rw [iSup_apply] - apply le_antisymm - · -- ≤ direction: every summand at w is ≤ b j - apply iSup_le - intro i - by_cases hij : i = j - · subst hij - by_cases hbi : b i = true - · simp [hbi, hw] - · have : b i = false := Bool.eq_false_iff.mpr hbi - simp [this] - · -- i ≠ j: anchor σᵢ w = false by uniqueness - have hf : anchor φ (anchorIndex φ i) w = false := by - cases hai : anchor φ (anchorIndex φ i) w - · rfl - · exact absurd (anchor_at_world_unique φ hai hw) hij - by_cases hbi : b i = true - · simp [hbi, hf] - · have : b i = false := Bool.eq_false_iff.mpr hbi - simp [this] - · -- ≥ direction: the j-th summand at w equals b j - by_cases hbj : b j = true - · -- bj=true: j-th summand at w = anchor σⱼ w = true = b j - have h1 : (if b j then anchor φ (anchorIndex φ j) else (⊥ : W → Bool)) w = true := by - simp [hbj, hw] - calc b j = true := hbj - _ = (if b j then anchor φ (anchorIndex φ j) else (⊥ : W → Bool)) w := h1.symm - _ ≤ ⨆ i, (if b i then anchor φ (anchorIndex φ i) else (⊥ : W → Bool)) w := - le_iSup (fun i => (if b i then anchor φ (anchorIndex φ i) - else (⊥ : W → Bool)) w) j - · -- bj=false: anything ≤ ⨆ - have : b j = false := Bool.eq_false_iff.mpr hbj - rw [this] - exact Bool.false_le _ - -/-- Round trip 1: `bitstringOf ∘ bitstringInverse = id` on `Fin n → Bool`. - Use `bitstringOf_eq_apply_at_anchor` (lifting through any anchor witness) - + `bitstringInverse_apply_at_anchor` (evaluating the inverse). -/ -theorem bitstringOf_bitstringInverse {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : - bitstringOf φ (bitstringInverse φ b) = b := by - funext j - obtain ⟨w, hw⟩ := anchorIndex_consistent φ j - rw [bitstringOf_eq_apply_at_anchor φ (bitstringInverse_mem_closure φ b) j hw] - exact bitstringInverse_apply_at_anchor φ b j hw - -/-- Round trip 2: `bitstringInverse ∘ bitstringOf = id` on closure elements. - Symmetric to round trip 1, using `bitstringOf_apply_at_world` for evaluation - of `bitstringOf ψ` at the worldAnchorIndex. -/ -theorem bitstringInverse_bitstringOf {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {ψ : W → Bool} - (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) : - bitstringInverse φ (bitstringOf φ ψ) = ψ := by - funext w - rw [bitstringInverse_apply_at_anchor φ (bitstringOf φ ψ) - (worldAnchorIndex φ w) (anchor_worldAnchorIndex φ w)] - exact bitstringOf_apply_at_world φ hψ w - --- ============================================================================ --- §11. Theorem 1 — the Boolean isomorphism (full ≃o) --- ============================================================================ - -/-- **Theorem 1 (Demey & Smessaert 2018) — the full Boolean-algebra isomorphism**. - `bitstringOf φ` restricted to the Boolean closure of `Set.range φ` is an - order isomorphism onto `Fin n → Bool` where `n = |partition|`. As an - OrderIso between Boolean algebras, it is automatically a Boolean-algebra - isomorphism (BA structure is determined by the order). - - Construction: `toFun := bitstringOf φ`, `invFun := bitstringInverse φ`, - round trips established above; monotonicity from - `bitAnd_eq_left_iff_forall_imp` (entailment ↔ bitwise inclusion). -/ -noncomputable def bitstringOf_orderIso - {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : - BooleanSubalgebra.closure (Set.range φ) ≃o - (Fin (partition ι W φ).card → Bool) where - toFun := fun ⟨ψ, _⟩ => bitstringOf φ ψ - invFun := fun b => ⟨bitstringInverse φ b, bitstringInverse_mem_closure φ b⟩ - left_inv := fun ⟨ψ, hψ⟩ => Subtype.ext (bitstringInverse_bitstringOf φ hψ) - right_inv := fun b => bitstringOf_bitstringInverse φ b - map_rel_iff' := by - rintro ⟨ψ₁, hψ₁⟩ ⟨ψ₂, hψ₂⟩ - show bitstringOf φ ψ₁ ≤ bitstringOf φ ψ₂ ↔ ψ₁ ≤ ψ₂ - rw [le_iff_pointwise_imp (f := bitstringOf φ ψ₁) (g := bitstringOf φ ψ₂), - le_iff_pointwise_imp (f := ψ₁) (g := ψ₂)] - -- Note: this proof structure parallels `bitAnd_eq_left_iff_forall_imp` (§9) - -- but is independent: §11 (Theorem 1, here) precedes §9 in file order - -- because §10's iff theorems use `bitstringOf_orderIso`-related machinery. - -- A unification (lift §11 to after §9) would save ~10 LOC; deferred. - constructor - · intro h w hw₁ - have := h (worldAnchorIndex φ w) - rw [bitstringOf_apply_at_world φ hψ₁ w, - bitstringOf_apply_at_world φ hψ₂ w] at this - exact this hw₁ - · intro h i - obtain ⟨w, hw⟩ := anchorIndex_consistent φ i - rw [bitstringOf_eq_apply_at_anchor φ hψ₁ i hw, - bitstringOf_eq_apply_at_anchor φ hψ₂ i hw] - exact h w - --- ============================================================================ --- §9. Three iff lemmas: bit-level conditions ↔ pointwise predicates --- ============================================================================ - -/-! All four Aristotelian-relation theorems below reduce to combinations of -three iff lemmas. Each `Bit*` predicate decomposes into bit-level conditions, -and each bit-level condition matches a pointwise predicate via the bridge -`bitstringOf_eq_apply_at_anchor` (forward) and `bitstringOf_apply_at_world` -(reverse). -/ - -section IffLemmas - -variable {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} - (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) - (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) - -include hψ₁ hψ₂ in -theorem bitAnd_eq_zeros_iff_forall_not_and : - bitAnd (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = zeros _ ↔ - ∀ w, ¬ (ψ₁ w = true ∧ ψ₂ w = true) := by - classical - refine ⟨fun hAnd w ⟨hw₁, hw₂⟩ => ?_, fun h => ?_⟩ - · have := congrFun hAnd (worldAnchorIndex φ w) - simp [bitAnd, zeros, bitstringOf_apply_at_world φ hψ₁ w, - bitstringOf_apply_at_world φ hψ₂ w, hw₁, hw₂] at this - · funext i - obtain ⟨w, hw⟩ := anchorIndex_consistent φ i - simp only [bitAnd, zeros, bitstringOf_eq_apply_at_anchor φ hψ₁ i hw, - bitstringOf_eq_apply_at_anchor φ hψ₂ i hw] - have := h w - cases hw₁ : ψ₁ w <;> cases hw₂ : ψ₂ w <;> simp_all - -include hψ₁ hψ₂ in -theorem bitOr_eq_ones_iff_forall_or : - bitOr (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = ones _ ↔ - ∀ w, ψ₁ w = true ∨ ψ₂ w = true := by - classical - refine ⟨fun hOr w => ?_, fun h => ?_⟩ - · have := congrFun hOr (worldAnchorIndex φ w) - simp only [bitOr, ones, bitstringOf_apply_at_world φ hψ₁ w, - bitstringOf_apply_at_world φ hψ₂ w] at this - cases hw₁ : ψ₁ w <;> cases hw₂ : ψ₂ w <;> simp_all - · funext i - obtain ⟨w, hw⟩ := anchorIndex_consistent φ i - simp only [bitOr, ones, bitstringOf_eq_apply_at_anchor φ hψ₁ i hw, - bitstringOf_eq_apply_at_anchor φ hψ₂ i hw] - rcases h w with h | h <;> simp [h] - -include hψ₁ hψ₂ in -theorem bitAnd_eq_left_iff_forall_imp : - bitAnd (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = bitstringOf φ ψ₁ ↔ - ∀ w, ψ₁ w = true → ψ₂ w = true := by - classical - refine ⟨fun hAnd w hw₁ => ?_, fun h => ?_⟩ - · have := congrFun hAnd (worldAnchorIndex φ w) - simp [bitAnd, bitstringOf_apply_at_world φ hψ₁ w, - bitstringOf_apply_at_world φ hψ₂ w, hw₁] at this - exact this - · funext i - obtain ⟨w, hw⟩ := anchorIndex_consistent φ i - simp only [bitAnd, bitstringOf_eq_apply_at_anchor φ hψ₁ i hw, - bitstringOf_eq_apply_at_anchor φ hψ₂ i hw] - cases hw₁ : ψ₁ w - · simp - · simp [h w hw₁] - -include hψ₁ hψ₂ in -theorem bitOr_eq_left_iff_forall_imp_rev : - bitOr (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = bitstringOf φ ψ₁ ↔ - ∀ w, ψ₂ w = true → ψ₁ w = true := by - classical - refine ⟨fun hOr w hw₂ => ?_, fun h => ?_⟩ - · have := congrFun hOr (worldAnchorIndex φ w) - simp [bitOr, bitstringOf_apply_at_world φ hψ₁ w, - bitstringOf_apply_at_world φ hψ₂ w, hw₂] at this - cases hw₁ : ψ₁ w - · rw [hw₁] at this; simpa using this - · rfl - · funext i - obtain ⟨w, hw⟩ := anchorIndex_consistent φ i - simp only [bitOr, bitstringOf_eq_apply_at_anchor φ hψ₁ i hw, - bitstringOf_eq_apply_at_anchor φ hψ₂ i hw] - cases hw₂ : ψ₂ w - · simp - · simp [h w hw₂] - -end IffLemmas - --- ============================================================================ --- §10. Theorem 2 — Aristotelian relations transfer (all four cases) --- ============================================================================ - -variable {ι : Type} [Fintype ι] [DecidableEq ι] - (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} - (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) - (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) - -include hψ₁ hψ₂ in -/-- **Theorem 2 — Contradictory** (Demey & Smessaert 2018). -/ -theorem contradictory_iff_bitContradictory : - Contradictory ψ₁ ψ₂ ↔ - BitContradictory (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) := by - unfold Contradictory BitContradictory - simp_rw [bitAnd_eq_zeros_iff_forall_not_and φ hψ₁ hψ₂, - bitOr_eq_ones_iff_forall_or φ hψ₁ hψ₂] - -include hψ₁ hψ₂ in -/-- **Theorem 2 — Contrary** (shares bitAnd half with Contradictory). -/ -theorem contrary_iff_bitContrary : - Contrary ψ₁ ψ₂ ↔ - BitContrary (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) := by - unfold Contrary BitContrary - exact ((bitAnd_eq_zeros_iff_forall_not_and φ hψ₁ hψ₂).and - (not_congr (bitOr_eq_ones_iff_forall_or φ hψ₁ hψ₂))).symm - -include hψ₁ hψ₂ in -/-- **Theorem 2 — Subcontrary** (dual of Contrary). -/ -theorem subcontrary_iff_bitSubcontrary : - Subcontrary ψ₁ ψ₂ ↔ - BitSubcontrary (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) := by - unfold Subcontrary BitSubcontrary - exact ((not_congr (bitAnd_eq_zeros_iff_forall_not_and φ hψ₁ hψ₂)).and - (bitOr_eq_ones_iff_forall_or φ hψ₁ hψ₂)).symm - -include hψ₁ hψ₂ in -/-- **Theorem 2 — Subaltern** (pointwise inclusion ↔ bitwise). -/ -theorem subaltern_iff_bitSubaltern : - Subaltern ψ₁ ψ₂ ↔ - BitSubaltern (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) := by - unfold Subaltern BitSubaltern - exact ((bitAnd_eq_left_iff_forall_imp φ hψ₁ hψ₂).and - (not_congr (bitOr_eq_left_iff_forall_imp_rev φ hψ₁ hψ₂))).symm - -end Core.Opposition diff --git a/Linglib/Core/Logic/Opposition/Diagram.lean b/Linglib/Core/Logic/Opposition/Diagram.lean deleted file mode 100644 index a7f6fff9e..000000000 --- a/Linglib/Core/Logic/Opposition/Diagram.lean +++ /dev/null @@ -1,95 +0,0 @@ -import Linglib.Core.Logic.Opposition.Aristotelian -import Mathlib.Data.Fintype.Card - -/-! -# Aristotelian diagrams (skeleton) - -Per @cite{demey-smessaert-2018} (and the broader Logica Universalis tradition -of Béziau, Pellissier, Smessaert and collaborators): - -An *Aristotelian diagram* is a finite indexed family of formulas together with -the matrix of Aristotelian relations between them. The classical Square is the -simplest non-trivial case (4 corners); other notable instances include: - -- **Hexagons** (6 corners, 3 contradiction diagonals) — Jacoby–Sesmat–Blanché, - Sherwood–Czeżowski, Unconnected-4 -- **Cubes / octagons** (8 corners) — Smessaert 2009 logical cube, - Buridan's octagon -- **Rhombic dodecahedron** (14 contingent corners) — the Boolean closure - of any 4-formula fragment in classical propositional logic - -This file provides the bare structural skeleton — full development of -specializations (hexagon shapes, cube generators) is deferred. The goal here -is to anchor the Square (`Square.lean`) and any future hexagons as instances -of one general structure rather than parallel ad-hoc definitions. - -## Design - -A `Diagram` is parameterized by: -- `ι : Type` — the index set of corners (e.g., `Fin 4` for Square, `Fin 6` for hexagon) -- `W : Type*` — the model class -- `φ : ι → W → Bool` — the corner-to-formula map - -The relation matrix `relation : ι → ι → AristotelianRel` is *derived* from -`φ` (one of the four `Contradictory`/`Contrary`/`Subcontrary`/`Subaltern` -predicates from `Aristotelian.lean` holds, or `unconnected`). --/ - -namespace Core.Opposition - -variable {W : Type*} - -/-- An Aristotelian diagram: a finite indexed family of formulas with their - Aristotelian relations. - - The `relation_correct` field asserts that the labeled relation matrix - matches the actual Aristotelian relations between the indexed formulas. - Since the four relations + unconnected partition all formula-pairs (per - Demey & Smessaert §2.1), this matrix is uniquely determined by `φ` — - `relation` is convenience data, `relation_correct` enforces consistency. -/ -structure Diagram (ι : Type) [Fintype ι] (W : Type*) where - /-- The corner-to-formula assignment. -/ - φ : ι → W → Bool - /-- The labeled relation between any two corners. -/ - relation : ι → ι → AristotelianRel - /-- Soundness: the labels match the actual Aristotelian relations. - Stated only for `contradictory`/`contrary`/`subcontrary`/`subaltern`; - `unconnected` is the residual when none of the others holds. -/ - relation_correct : ∀ i j, - (relation i j = AristotelianRel.contradictory → Contradictory (φ i) (φ j)) ∧ - (relation i j = AristotelianRel.contrary → Contrary (φ i) (φ j)) ∧ - (relation i j = AristotelianRel.subcontrary → Subcontrary (φ i) (φ j)) ∧ - (relation i j = AristotelianRel.subaltern → Subaltern (φ i) (φ j)) - -namespace Diagram - -variable {ι : Type} [Fintype ι] - -/-- The number of corners in the diagram. -/ -def size (_ : Diagram ι W) : ℕ := Fintype.card ι - -/-- A diagram corner satisfying its formula at a particular world. -/ -def trueAt (D : Diagram ι W) (i : ι) (w : W) : Prop := D.φ i w = true - -end Diagram - --- ============================================================================ --- §1. Specialization tags (planned home for Square / Hexagon / Cube) --- ============================================================================ - -/-! Specializations live in sibling files: - -- `Square.lean` — `Diagram (Fin 4)` with the canonical CD/CD/C/SC/SA/SA pattern -- `Hexagon.lean` — `Diagram (Fin 6)` (TODO; 3 Aristotelian families per - @cite{demey-smessaert-2018} Fig. 2: JSB, SC, U4. The strong/weak JSB - distinction within JSB is Aristotelian-iso but not Boolean-iso, p. 350-352) -- `Cube.lean` — `Diagram (Fin 8)` (TODO; Smessaert 2009 "On the 3D visualisation - of logical relations," Logica Universalis 3, 303-332 — bib entry deferred - pending verified DOI) - -Adding a specialization is a matter of (a) picking an `ι` enum, (b) writing -the `relation` matrix, (c) discharging `relation_correct`. The bitstring -machinery in `Bitstring.lean` makes (c) automatic for Boolean-closed fragments. --/ - -end Core.Opposition diff --git a/Linglib/Core/Logic/Opposition/Partition.lean b/Linglib/Core/Logic/Opposition/Partition.lean deleted file mode 100644 index b06881c79..000000000 --- a/Linglib/Core/Logic/Opposition/Partition.lean +++ /dev/null @@ -1,114 +0,0 @@ -import Linglib.Core.Logic.Opposition.Aristotelian -import Mathlib.Data.Finset.Basic -import Mathlib.Data.Fintype.Basic -import Mathlib.Data.Fintype.Pi -import Mathlib.Data.Fintype.Prod - -/-! -# Partitions induced by logical fragments (skeleton) - -Per @cite{demey-smessaert-2018} §3.1, Definitions 5–6. - -Given a logical system `S` and a finite fragment `ℱ = {φ_1, ..., φ_m}`, the -partition `Π_S(ℱ)` is the set of *anchor formulas* — maximal-information -conjunctions of literals over ℱ that are S-consistent: - - Π_S(ℱ) := {α | α ≡_S ±φ_1 ∧ ... ∧ ±φ_m, α is S-consistent} - -The anchor formulas are mutually exclusive and jointly exhaustive (Lemma 3), -forming a partition of the model class. Their cardinality `n = |Π_S(ℱ)|` -determines the bitstring length: `|𝔹(ℱ)| = 2^n`. - --/ - -namespace Core.Opposition - -variable {W : Type*} - --- ============================================================================ --- §1. Polarity literals --- ============================================================================ - -/-- A *literal* over a Boolean predicate: either the predicate itself or - its negation. Used to build anchor formulas. -/ -inductive Literal (W : Type*) where - | pos (φ : W → Bool) - | neg (φ : W → Bool) - -/-- Interpret a literal as a Boolean predicate. -/ -def Literal.eval : Literal W → W → Bool - | .pos φ, w => φ w - | .neg φ, w => !φ w - -/-- A *polarity assignment* selects one literal per fragment formula. -/ -abbrev PolarityAssignment (ι : Type) (W : Type*) := ι → (W → Bool) → Literal W - --- ============================================================================ --- §2. Anchor formulas (Definition 5) --- ============================================================================ - -/-- The anchor formula for polarity assignment `σ` over fragment `φ`: - the conjunction `±φ_1 ∧ ... ∧ ±φ_m` with signs given by σ. -/ -def anchor {ι : Type} [Fintype ι] (φ : ι → W → Bool) - (σ : ι → Bool) (w : W) : Bool := - decide (∀ i : ι, if σ i then (φ i w = true) else (φ i w = false)) - -/-- An anchor formula is *consistent* if it is satisfiable in some world. -/ -def anchorConsistent {ι : Type} [Fintype ι] (φ : ι → W → Bool) - (σ : ι → Bool) : Prop := - ∃ w : W, anchor φ σ w = true - -/-- The partition of a fragment: all consistent polarity assignments. -/ -def partition (ι : Type) [Fintype ι] [DecidableEq ι] (W : Type*) [Fintype W] - (φ : ι → W → Bool) : Finset (ι → Bool) := - Finset.univ.filter (fun σ => decide (∃ w : W, anchor φ σ w = true)) - --- ============================================================================ --- §3. Lemma 3 — mutual exclusivity and joint exhaustion --- ============================================================================ - -/-- Two distinct anchor formulas are jointly inconsistent. -/ -theorem anchor_mutually_exclusive {ι : Type} [Fintype ι] - (φ : ι → W → Bool) (σ τ : ι → Bool) (h : σ ≠ τ) : - ∀ w, ¬ (anchor φ σ w = true ∧ anchor φ τ w = true) := by - intro w ⟨hσ, hτ⟩ - -- σ ≠ τ ⇒ ∃ i, σ i ≠ τ i - obtain ⟨i, hi⟩ : ∃ i, σ i ≠ τ i := by - by_contra hAll - push_neg at hAll - exact h (funext hAll) - -- Unpack both anchor conditions at index i - rw [anchor, decide_eq_true_eq] at hσ hτ - have hσi := hσ i - have hτi := hτ i - -- σ i ≠ τ i means one is true, the other false; derive contradiction on φ i w - rcases hσ_val : σ i with _ | _ <;> rcases hτ_val : τ i with _ | _ - all_goals simp_all - -/-- Every world satisfies exactly one anchor formula (joint exhaustion). -/ -theorem anchor_jointly_exhaustive {ι : Type} [Fintype ι] - (φ : ι → W → Bool) (w : W) : - ∃ σ, anchor φ σ w = true := by - -- Take σ i := φ i w; then anchor φ σ w trivially holds - refine ⟨fun i => φ i w, ?_⟩ - rw [anchor, decide_eq_true_eq] - intro i - by_cases h : φ i w = true - · simp [h] - · have : φ i w = false := by cases hb : φ i w <;> simp_all - simp [this] - --- ============================================================================ --- §4. Meet of partitions (Definition 6) --- ============================================================================ - -/-- The meet of two partitions: anchor formulas of the union fragment. - Per Lemma 4, `Π(ℱ₁ ∪ ℱ₂) = Π(ℱ₁) ∧ Π(ℱ₂)`. -/ -def partitionMeet {ι₁ ι₂ : Type} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] - [DecidableEq ι₂] {W : Type*} [Fintype W] - (φ₁ : ι₁ → W → Bool) (φ₂ : ι₂ → W → Bool) : - Finset ((ι₁ → Bool) × (ι₂ → Bool)) := - (Finset.univ.product Finset.univ).filter (fun p => - decide (∃ w : W, anchor φ₁ p.1 w = true ∧ anchor φ₂ p.2 w = true)) - -end Core.Opposition diff --git a/Linglib/Core/Logic/Opposition/Probabilistic.lean b/Linglib/Core/Logic/Opposition/Probabilistic.lean deleted file mode 100644 index 12e8dfdf0..000000000 --- a/Linglib/Core/Logic/Opposition/Probabilistic.lean +++ /dev/null @@ -1,221 +0,0 @@ -import Linglib.Core.Logic.Opposition.Aristotelian -import Linglib.Core.Probability.Finite - -/-! -# Probabilistic Aristotelian relations - -When the model class `W` is equipped with a probability measure `μ : PMF W`, -the four Aristotelian relations have natural probabilistic generalisations -as linear (in)equalities on the probabilities `P_μ[φ] := μ({w | φ w = true})`: - -| Boolean Aristotelian relation | Probabilistic counterpart | -|-------------------------------|---------------------------| -| `Contradictory φ ψ` | `P[φ] + P[ψ] = 1` | -| `Contrary φ ψ` | `P[φ] + P[ψ] ≤ 1` | -| `Subcontrary φ ψ` | `P[φ] + P[ψ] ≥ 1` | -| `Subaltern φ ψ` | `P[φ] ≤ P[ψ]` | - -This is the convex extension of the Boolean Aristotelian geometry: the discrete -case (each `μ a ∈ {0,1}`) recovers Definition 1 of @cite{demey-smessaert-2018} -exactly; the convex case is what Bayesian listeners actually compute. - -## Why this matters for RSA / Bayesian-pragmatic models - -The Tessler–Tenenbaum–Goodman 2022 syllogistic model (and any RSA-style -Bayesian-pragmatic model that reasons about quantifier inference) computes a -posterior `μ : PMF W` over states given premises, then evaluates conclusion -probabilities `P_μ[c]`. The Belief Alignment / State Communication / Literal -Speaker utilities are functionals of these `P_μ[c]` values across the -conclusion space — and those values are jointly constrained by the -probabilistic Aristotelian inequalities. Subalternation `P[All A-C] ≤ -P[Some A-C]` for the *same* posterior μ is a constraint the speaker model -respects automatically. - -## Transfer theorems - -The key result of this file: **if `φ` and `ψ` stand in a Boolean Aristotelian -relation, then they stand in the corresponding probabilistic relation under -every probability measure `μ`.** The Boolean → probabilistic direction is free; -the converse fails (μ-specific equalities can hold without Boolean entailment). -For example, two Boolean-`Unconnected` predicates `φ`, `ψ` can satisfy -`P_μ[φ] + P_μ[ψ] = 1` for a particular μ that happens to allocate measure -exactly to `{φ ∨ ψ}` and zero to `{¬φ ∧ ¬ψ}`, without being Boolean-contradictory. - -## Related literature - -The probabilistic-square tradition is distinct from the Logica Universalis -"abstract Aristotelian diagrams" tradition that this file specializes. Pfeifer -and collaborators (Pfeifer 2006, Pfeifer & Sanfilippo subsequent work) develop -probabilistic squares of opposition based on coherent conditional probability; -that line gives a different (conditional, not absolute) reading of the four -inequalities. The version here is the **unconditional / absolute** form, -appropriate for RSA-style models where the posterior `μ : PMF W` over states -is the object of study. (Bib entries for the Pfeifer line not yet in linglib; -add when a consumer needs the conditional version.) --/ - -namespace Core.Opposition - -open scoped ENNReal - -variable {W : Type*} [Fintype W] - --- ============================================================================ --- §1. Probability of a Boolean predicate --- ============================================================================ - -/-- The probability of a Boolean predicate `φ : W → Bool` under `μ : PMF W`, - i.e. `μ({w | φ w = true})`. Built on `Finite.probOfSet`. -/ -noncomputable def boolProb (μ : PMF W) (φ : W → Bool) : ℝ≥0∞ := - PMF.probOfSet μ {w | φ w = true} - -@[inherit_doc boolProb] -notation "P[" φ " ; " μ "]" => boolProb μ φ - -/-- Total probability: `P[φ] + P[¬φ] = 1`. The basic conservation law. - Proof: convert each side to a Finset sum via `toOuterMeasure_apply_fintype`, - then observe that the two indicators are pointwise complementary and sum to - `μ x` at every x; PMF totality (`tsum_coe`) closes the result. -/ -theorem boolProb_add_compl (μ : PMF W) (φ : W → Bool) : - boolProb μ φ + boolProb μ (fun w => !φ w) = 1 := by - classical - unfold boolProb PMF.probOfSet - rw [PMF.toOuterMeasure_apply_fintype, PMF.toOuterMeasure_apply_fintype, - ← Finset.sum_add_distrib] - have hsum : ∀ x, ({w | φ w = true} : Set W).indicator μ x + - ({w | (!φ w) = true} : Set W).indicator μ x = μ x := by - intro x - cases hφ : φ x - · simp [Set.indicator, hφ] - · simp [Set.indicator, hφ] - rw [Finset.sum_congr rfl (fun x _ => hsum x)] - have : ∑ x, μ x = (∑' x, μ x : ℝ≥0∞) := - (tsum_eq_sum (f := μ) (s := Finset.univ) - (fun x h => absurd (Finset.mem_univ x) h)).symm - rw [this, PMF.tsum_coe] - --- ============================================================================ --- §2. Probabilistic Aristotelian relations (Definition 1, convex form) --- ============================================================================ - -/-- Probabilistic contradictoriness: `P[φ] + P[ψ] = 1`. Discrete case - recovers `Contradictory`. -/ -def ProbContradictory (μ : PMF W) (φ ψ : W → Bool) : Prop := - boolProb μ φ + boolProb μ ψ = 1 - -/-- Probabilistic contrariety: `P[φ] + P[ψ] ≤ 1`, with strict inequality - possible. Discrete case recovers `Contrary` (where `P[φ] + P[ψ] < 1` - when neither holds at some world). -/ -def ProbContrary (μ : PMF W) (φ ψ : W → Bool) : Prop := - boolProb μ φ + boolProb μ ψ ≤ 1 - -/-- Probabilistic subcontrariety: `P[φ] + P[ψ] ≥ 1`. Discrete case recovers - `Subcontrary` (where `P[φ] + P[ψ] > 1` when both hold at some world). -/ -def ProbSubcontrary (μ : PMF W) (φ ψ : W → Bool) : Prop := - boolProb μ φ + boolProb μ ψ ≥ 1 - -/-- Probabilistic subalternation: `P[φ] ≤ P[ψ]`. Discrete case (Boolean - `Subaltern φ ψ`) implies this for *every* μ via monotonicity of `μ`. -/ -def ProbSubaltern (μ : PMF W) (φ ψ : W → Bool) : Prop := - boolProb μ φ ≤ boolProb μ ψ - --- ============================================================================ --- §3. Transfer theorems: Boolean ⇒ Probabilistic (for every μ) --- ============================================================================ - -/-- Boolean contradictoriness implies probabilistic contradictoriness for - every probability measure. Direct from `boolProb_add_compl` once we - note that `Contradictory φ ψ` makes ψ pointwise `!φ`. -/ -theorem Contradictory.toProb {φ ψ : W → Bool} - (h : Contradictory φ ψ) (μ : PMF W) : - ProbContradictory μ φ ψ := by - -- Show ψ = (fun w => !φ w) as Boolean functions, then apply boolProb_add_compl - have hPointwise : ∀ w, ψ w = !φ w := by - intro w - have h1 := h.1 w - have h2 := h.2 w - cases hφ : φ w - · cases hψ : ψ w - · exfalso; exact h2.elim (fun h => by rw [hφ] at h; exact Bool.noConfusion h) - (fun h => by rw [hψ] at h; exact Bool.noConfusion h) - · simp [hφ] - · cases hψ : ψ w - · simp [hφ] - · exfalso; exact h1 ⟨hφ, hψ⟩ - have hψ_eq : ψ = (fun w => !φ w) := funext hPointwise - unfold ProbContradictory - rw [hψ_eq] - exact boolProb_add_compl μ φ - -/-- Boolean subalternation implies probabilistic subalternation: if `φ ⊨ ψ` - holds pointwise, then `P_μ[φ] ≤ P_μ[ψ]` for every μ (PMF monotonicity). -/ -theorem Subaltern.toProb {φ ψ : W → Bool} - (h : Subaltern φ ψ) (μ : PMF W) : - ProbSubaltern μ φ ψ := by - unfold ProbSubaltern boolProb PMF.probOfSet - apply MeasureTheory.OuterMeasure.mono - intro w hw - exact h.1 w hw - -/-- Boolean contrariety implies probabilistic contrariety: if `φ` and `ψ` - cannot both be true, then `P[φ] + P[ψ] ≤ 1`. At each x, the two - indicators sum to at most `μ x` (both nonzero would mean φ ∧ ψ at x). -/ -theorem Contrary.toProb {φ ψ : W → Bool} - (h : Contrary φ ψ) (μ : PMF W) : - ProbContrary μ φ ψ := by - classical - unfold ProbContrary boolProb PMF.probOfSet - rw [PMF.toOuterMeasure_apply_fintype, PMF.toOuterMeasure_apply_fintype, - ← Finset.sum_add_distrib] - have hbnd : ∀ x ∈ Finset.univ, - ({w | φ w = true} : Set W).indicator μ x + - ({w | ψ w = true} : Set W).indicator μ x ≤ μ x := by - intro x _ - by_cases hφ : φ x = true - · by_cases hψ : ψ x = true - · exact absurd ⟨hφ, hψ⟩ (h.1 x) - · simp [Set.indicator, hφ, hψ] - · by_cases hψ : ψ x = true - · simp [Set.indicator, hφ, hψ] - · simp [Set.indicator, hφ, hψ] - have htotal : ∑ x, μ x = (1 : ℝ≥0∞) := by - have : ∑ y, μ y = (∑' y, μ y : ℝ≥0∞) := - (tsum_eq_sum (f := μ) (s := Finset.univ) - (fun y hy => absurd (Finset.mem_univ y) hy)).symm - rw [this, PMF.tsum_coe] - calc (∑ x, (({w | φ w = true} : Set W).indicator μ x + - ({w | ψ w = true} : Set W).indicator μ x)) - ≤ ∑ x, μ x := Finset.sum_le_sum hbnd - _ = 1 := htotal - -/-- Boolean subcontrariety implies probabilistic subcontrariety: if `φ ∨ ψ` - is valid, then `P[φ] + P[ψ] ≥ 1`. At each x, the indicator sum is at - least `μ x` (at least one of φ, ψ is true at x by `h.2`). -/ -theorem Subcontrary.toProb {φ ψ : W → Bool} - (h : Subcontrary φ ψ) (μ : PMF W) : - ProbSubcontrary μ φ ψ := by - classical - unfold ProbSubcontrary boolProb PMF.probOfSet - rw [PMF.toOuterMeasure_apply_fintype, PMF.toOuterMeasure_apply_fintype, - ← Finset.sum_add_distrib] - have hbnd : ∀ x ∈ Finset.univ, - μ x ≤ ({w | φ w = true} : Set W).indicator μ x + - ({w | ψ w = true} : Set W).indicator μ x := by - intro x _ - rcases h.2 x with hφ | hψ - · simp [Set.indicator, hφ] - · by_cases hφ' : φ x = true - · simp [Set.indicator, hφ', hψ] - · simp [Set.indicator, hφ', hψ] - have htotal : (1 : ℝ≥0∞) = ∑ x, μ x := by - have : ∑ y, μ y = (∑' y, μ y : ℝ≥0∞) := - (tsum_eq_sum (f := μ) (s := Finset.univ) - (fun y hy => absurd (Finset.mem_univ y) hy)).symm - rw [this, PMF.tsum_coe] - calc (1 : ℝ≥0∞) - = ∑ x, μ x := htotal - _ ≤ ∑ x, (({w | φ w = true} : Set W).indicator μ x + - ({w | ψ w = true} : Set W).indicator μ x) := - Finset.sum_le_sum hbnd - -end Core.Opposition diff --git a/Linglib/Core/Logic/Opposition/Square.lean b/Linglib/Core/Logic/Opposition/Square.lean deleted file mode 100644 index 35e7be5c9..000000000 --- a/Linglib/Core/Logic/Opposition/Square.lean +++ /dev/null @@ -1,320 +0,0 @@ -import Linglib.Core.Logic.Quantification -import Linglib.Core.Logic.Opposition.Aristotelian - -/-! -# Square of Opposition -@cite{barwise-cooper-1981} @cite{horn-2001} - -The Aristotelian Square of Opposition reified as a first-class algebraic object. - -The square arranges four operators at its vertices: - -``` - contraries - A ──────────────── E - │ │ - │ subalterns subalterns - │ │ - I ──────────────── O - subcontraries -``` - -The six relations: -- **Contraries** (A–E): cannot both be true -- **Subcontraries** (I–O): cannot both be false -- **Contradictories** (A–O, E–I): exactly one is true -- **Subalterns** (A→I, E→O): the universal entails the particular - -The square unifies quantifiers, modals, connectives, and attitudes: -- Quantifiers: A = every, E = no, I = some, O = not-every -- Modals: A = □, E = □¬, I = ◇, O = ¬□ -- Attitudes: A = Bel(p), E = Bel(¬p), I = ◇p, O = ¬Bel(p) - -The three duality operations (outer negation, inner negation, dual) generate -the square from any single vertex. This module provides the abstract framework; -concrete instantiations live in their respective theory modules. - --/ - -namespace Core.Opposition - -open Core.Quantification (GQ outerNeg innerNeg dualQ) - --- ============================================================================ --- §1 The Square --- ============================================================================ - -/-- The four vertices of a Square of Opposition. -/ -structure Square (α : Type*) where - /-- A-corner: universal affirmative (every, □, Bel(p)) -/ - A : α - /-- E-corner: universal negative (no, □¬, Bel(¬p)) -/ - E : α - /-- I-corner: particular affirmative (some, ◇, ◇p) -/ - I : α - /-- O-corner: particular negative (not-every, ¬□, ¬Bel(p)) -/ - O : α - deriving Repr - -/-- The three operations that generate the square from a single vertex. - -Given a vertex `A`, the other three are determined by: -- `E = innerNeg A` (negate the scope / complement) -- `O = outerNeg A` (negate the result) -- `I = dual A = outerNeg (innerNeg A)` -/ -structure SquareOps (α : Type*) where - /-- Inner negation: A ↦ E, I ↦ O -/ - inner : α → α - /-- Outer negation: A ↦ O, E ↦ I -/ - outer : α → α - /-- Dual: A ↦ I, E ↦ O. Should equal outer ∘ inner. -/ - dual : α → α - -/-- Build a square from a single vertex and the three duality operations. -/ -def Square.fromOps {α : Type*} (a : α) (ops : SquareOps α) : Square α where - A := a - E := ops.inner a - I := ops.dual a - O := ops.outer a - --- ============================================================================ --- §2 Square Relations (propositional level) --- ============================================================================ - -/-- The six logical relations of the Square of Opposition. - -Defined over `W → Bool` (decidable propositions over a domain `W`). -The relations are pointwise: they hold at every point `w : W`. -/ -structure SquareRelations {W : Type*} (sq : Square (W → Bool)) where - /-- A entails I (subalternation). -/ - subalternAI : ∀ w, sq.A w = true → sq.I w = true - /-- E entails O (subalternation). -/ - subalternEO : ∀ w, sq.E w = true → sq.O w = true - /-- A and O are contradictories: A = ¬O. -/ - contradAO : ∀ w, sq.A w = !sq.O w - /-- E and I are contradictories: E = ¬I. -/ - contradEI : ∀ w, sq.E w = !sq.I w - /-- A and E are contraries: cannot both be true. -/ - contraryAE : ∀ w, sq.A w = true → sq.E w = false - /-- I and O are subcontraries: cannot both be false. -/ - subcontrIO : ∀ w, sq.I w = false → sq.O w = true - --- ============================================================================ --- §3 Constructing Squares from Duality Operations --- ============================================================================ - -/-- Build a square from any operator and the GQ duality operations. -/ -def Square.fromGQOps {α : Type*} (q : GQ α) : Square (GQ α) := - Square.fromOps q - { inner := innerNeg - outer := outerNeg - dual := dualQ } - -/-- The standard GQ duality operations. -/ -def gqSquareOps (α : Type*) : SquareOps (GQ α) where - inner := innerNeg - outer := outerNeg - dual := dualQ - --- ============================================================================ --- §4 Deriving Relations from Contradiction --- ============================================================================ - -/-! The six relations are not independent. Given the two contradiction -diagonals (A = ¬O, E = ¬I), the other four relations follow: - -- Contraries: A ∧ E → A ∧ ¬I → (by subalternation) A ∧ ¬A → ⊥ -- Subcontraries: ¬I ∧ ¬O → E ∧ ¬O → (by subalternation) E ∧ ¬E → ⊥ -- Subalternation: derived from contrariety + contradiction - -So the contradiction diagonals are the primitive relations; the rest -are consequences. This matches Horn's analysis: contradiction is fundamental. -/ - -/-- Contraries cannot both be true. -/ -theorem contraries_not_both_true {W : Type*} (sq : Square (W → Bool)) - (rel : SquareRelations sq) (w : W) - (hA : sq.A w = true) : sq.E w = false := - rel.contraryAE w hA - -/-- Subcontraries cannot both be false. -/ -theorem subcontraries_not_both_false {W : Type*} (sq : Square (W → Bool)) - (rel : SquareRelations sq) (w : W) - (hI : sq.I w = false) : sq.O w = true := - rel.subcontrIO w hI - -/-- From the contradiction diagonals, derive that A entails I. -/ -theorem subaltern_from_contradictions {W : Type*} (sq : Square (W → Bool)) - (_hAO : ∀ w, sq.A w = !sq.O w) - (hEI : ∀ w, sq.E w = !sq.I w) - (hAE : ∀ w, sq.A w = true → sq.E w = false) - (w : W) (hA : sq.A w = true) : sq.I w = true := by - -- From A = true and contraryAE, E = false - have hE := hAE w hA - -- From E = ¬I, E = false means I = true - have hEI_w := hEI w - rw [hE] at hEI_w - simp at hEI_w - exact hEI_w - --- ============================================================================ --- §4.5 Bridge to `Aristotelian.lean` predicates --- ============================================================================ - -/-! The `SquareRelations` axioms above are deliberately weaker than the -Aristotelian-relation predicates from `Aristotelian.lean`: each field asserts -just one direction (e.g., `subalternAI` asserts `A → I` but not its strictness; -`contraryAE` asserts impossibility of joint truth but not impossibility of -joint falsity). This is intentional — it lets users provide minimal axioms -and have the rest derived via `subaltern_from_contradictions` etc. - -The bridge lemmas below convert those weaker axioms into the full Aristotelian -predicates, when the necessary side conditions (proper-subalternation -witnesses, etc.) are provided. -/ - -/-- The `contradAO` axiom is exactly `Contradictory sq.A sq.O`. -/ -theorem SquareRelations.toContradictoryAO {W : Type*} {sq : Square (W → Bool)} - (rel : SquareRelations sq) : Contradictory sq.A sq.O := by - refine ⟨?_, ?_⟩ - · intro w ⟨hA, hO⟩ - have := rel.contradAO w - rw [hA, hO] at this - exact Bool.noConfusion this - · intro w - have := rel.contradAO w - cases hA : sq.A w - · right; rw [hA] at this; simpa using this.symm - · left; rfl - -/-- The `contradEI` axiom is exactly `Contradictory sq.E sq.I`. -/ -theorem SquareRelations.toContradictoryEI {W : Type*} {sq : Square (W → Bool)} - (rel : SquareRelations sq) : Contradictory sq.E sq.I := by - refine ⟨?_, ?_⟩ - · intro w ⟨hE, hI⟩ - have := rel.contradEI w - rw [hE, hI] at this - exact Bool.noConfusion this - · intro w - have := rel.contradEI w - cases hE : sq.E w - · right; rw [hE] at this; simpa using this.symm - · left; rfl - -/-- A `SquareRelations` lifts to `Subaltern sq.A sq.I` when given a witness - `w` showing `I` does not entail `A`. The witness is needed because - `Aristotelian.Subaltern` is *proper* subalternation (strict). -/ -theorem SquareRelations.toSubalternAI {W : Type*} {sq : Square (W → Bool)} - (rel : SquareRelations sq) (w : W) - (hwI : sq.I w = true) (hwA : sq.A w = false) : - Subaltern sq.A sq.I := - ⟨rel.subalternAI, fun h => by - have := h w hwI - rw [hwA] at this - exact Bool.noConfusion this⟩ - -/-- A `SquareRelations` lifts to `Contrary sq.A sq.E` when given a witness - `w` where neither `A` nor `E` holds (the joint-non-exhaustion condition - that distinguishes Aristotelian `Contrary` from mere "cannot both be true"). -/ -theorem SquareRelations.toContraryAE {W : Type*} {sq : Square (W → Bool)} - (rel : SquareRelations sq) (w : W) - (hwA : sq.A w = false) (hwE : sq.E w = false) : - Contrary sq.A sq.E := - ⟨fun w' ⟨hA, hE⟩ => by - have := rel.contraryAE w' hA - rw [hE] at this; exact Bool.noConfusion this, - fun h => by - rcases h w with hA | hE - · rw [hwA] at hA; exact Bool.noConfusion hA - · rw [hwE] at hE; exact Bool.noConfusion hE⟩ - -/-- From the outer/inner negation structure, the contradiction diagonals -hold definitionally: A ↔ ¬(outerNeg A) and innerNeg A ↔ ¬(dual A). -/ -theorem outerNeg_contradiction {α : Type*} (q : GQ α) (R S : α → Prop) : - q R S ↔ ¬ (outerNeg q R S) := by - simp [outerNeg, Classical.not_not] - -theorem innerNeg_dual_contradiction {α : Type*} (q : GQ α) (R S : α → Prop) : - innerNeg q R S ↔ ¬ (dualQ q R S) := by - simp [dualQ, outerNeg, innerNeg, Classical.not_not] - --- ============================================================================ --- §5 The Propositional Operator Square --- ============================================================================ - -/- -The square of opposition is non-trivial only for operators with TWO arguments -(like GQs: restrictor × scope) or for modal operators (□/◇ duality). - -For single-argument operators (propositions), inner neg = outer neg, -so the square degenerates. The interesting squares are: -1. GQ squares (two arguments: restrictor, scope) -2. Modal squares (one argument but with an accessibility relation) -3. Attitude squares (one argument but with a belief relation) - -For (2) and (3), the square is built from □/◇ duality at the -propositional level, not from the proposition itself. --/ - -/-- Build a square of propositions from a box-like operator. - -Given `box : (W → Bool) → W → Bool` (e.g., □ = "all accessible worlds satisfy"), -and a proposition `p`, produce the four corners: -- A = box p (□p: necessarily p) -- E = box (¬p) (□¬p: necessarily not-p) -- I = ¬(box (¬p)) (◇p: possibly p) -- O = ¬(box p) (¬□p: not necessarily p) --/ -def Square.fromBox {W : Type*} (box : (W → Bool) → W → Bool) (p : W → Bool) : - Square (W → Bool) where - A := box p - E := box (λ w => !p w) - I := λ w => !(box (λ w' => !p w') w) - O := λ w => !(box p w) - -/-- The box-derived square always satisfies the contradiction diagonals. -/ -theorem fromBox_contradAO {W : Type*} (box : (W → Bool) → W → Bool) - (p : W → Bool) (w : W) : - (Square.fromBox box p).A w = !(Square.fromBox box p).O w := by - simp [Square.fromBox, Bool.not_not] - -theorem fromBox_contradEI {W : Type*} (box : (W → Bool) → W → Bool) - (p : W → Bool) (w : W) : - (Square.fromBox box p).E w = !(Square.fromBox box p).I w := by - simp [Square.fromBox, Bool.not_not] - --- ============================================================================ --- §6 Connection to Horn Scales --- ============================================================================ - -/-! Subalternation is the entailment relation that underlies Horn scales. - -The I–A edge of the quantifier square (some → every) is precisely the -`⟨some, all⟩` Horn scale from `Core.Scale`. More generally: - -- The weak member of a Horn scale sits at I (particular/existential) -- The strong member sits at A (universal) -- Scalar implicature from I negates A: "some" implicates "not all" (= O) - -This means the square of opposition IS the algebraic structure underlying -scalar implicature: using the weak term (I) implicates the negation of -the strong term (¬A = O). The "O-corner gap" — the non-lexicalization of O — -is pragmatically explained: O is always recoverable as the implicature of I. - -`TODO`: Open conjectures (previously stubbed in deleted -`Core/Conjectures.lean`): - -- **O-corner lexicalization gap**: across natural languages, A/E/I are - lexicalized but O is always periphrastic (¬A): `lexicalized A ∧ - lexicalized E ∧ lexicalized I ∧ ¬lexicalized O`. Requires a - cross-linguistic lexicalization registry. -- **Pragmatic explanation of the gap** (@cite{horn-2001}, §4.5): the - scalar implicature of the I-corner recovers the O-corner's content, - making lexicalization of O communicatively redundant. -/ - -/-- Subalternation A→I is equivalent to the Horn-scale ordering: -the A-corner entails the I-corner, which is the scale `⟨I, A⟩`. -/ -theorem subalternation_is_scale_ordering {W : Type*} (sq : Square (W → Bool)) - (rel : SquareRelations sq) : - ∀ w, sq.A w = true → sq.I w = true := - rel.subalternAI - -end Core.Opposition diff --git a/Linglib/Core/Logic/Quantification/Basic.lean b/Linglib/Core/Logic/Quantification/Basic.lean index a8c7187c1..9656d8c10 100644 --- a/Linglib/Core/Logic/Quantification/Basic.lean +++ b/Linglib/Core/Logic/Quantification/Basic.lean @@ -1,6 +1,6 @@ import Linglib.Core.Logic.Quantification.Defs import Linglib.Core.Logic.Quantification.Properties -import Linglib.Core.Logic.Opposition.Aristotelian +import Linglib.Core.Logic.Aristotelian.Basic /-! # Concrete propositional generalized quantifiers @@ -230,7 +230,7 @@ theorem every_filtrating : Filtrating (every_sem (α := α)) := by The six theorems below establish the four Aristotelian relations among GQ denotations `(every_sem, some_sem, no_sem, outerNeg every_sem)` at fixed restrictor `R`. They work over `Prop`-valued predicates, while -`Core.Logic.Opposition.Aristotelian` formulates the same relations over +`Core.Logic.Aristotelian.Basic` formulates the same relations over `Bool`-valued predicates. The two frameworks are mathematically equivalent but type-different. -/ @@ -276,12 +276,14 @@ theorem subcontrariety_i_o (R S : α → Prop) obtain ⟨x, hRx⟩ := hR; exact ⟨x, hRx, hA x hRx⟩ /-- The canonical A↔O contradiction diagonal, packaged as - `Core.Opposition.IsContradictory` over the Pi-instance Boolean algebra + `Aristotelian.IsContradictory` over the Pi-instance Boolean algebra on `(α → Prop) → Prop`. -/ theorem every_satisfies_isContradictory_pointwise (R : α → Prop) : - Core.Opposition.IsContradictory + Aristotelian.IsContradictory ((every_sem (α := α) R) : (α → Prop) → Prop) (outerNeg (every_sem (α := α)) R) := by + unfold Aristotelian.IsContradictory + rw [isCompl_iff, disjoint_iff, codisjoint_iff] refine ⟨?_, ?_⟩ · funext S exact propext ⟨fun ⟨h1, h2⟩ => h2 h1, fun h => h.elim⟩ diff --git a/Linglib/Features/Antonymy.lean b/Linglib/Features/Antonymy.lean index 8170335f0..3a04bf054 100644 --- a/Linglib/Features/Antonymy.lean +++ b/Linglib/Features/Antonymy.lean @@ -29,8 +29,8 @@ namespace Features gradable-adjective semantics to distinguish licensing patterns of the two-threshold model. - **Cross-reference**: `Core.Opposition.AristotelianRel` (in - `Core/Logic/Opposition/Aristotelian.lean`) is a 5-valued enum that + **Cross-reference**: `Aristotelian.AristotelianRel` (in + `Core/Logic/Aristotelian/Basic.lean`) is a 5-valued enum that subsumes both constructors here. A future cleanup could replace `NegationType` with `{ r : AristotelianRel // r ∈ {.contradictory, .contrary} }` or have consumers take `AristotelianRel` directly. Deferred until diff --git a/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean b/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean index ce6bf3438..fbb359ccb 100644 --- a/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean +++ b/Linglib/Pragmatics/Implicature/EpistemicBlocking.lean @@ -71,7 +71,7 @@ instance {W : Type*} (e : EpistemicState W) (φ : W → Prop) [DecidablePred φ] /-- Standard epistemic duality: ¬K¬φ ↔ Pφ. One of five sibling `theorem duality`s (see `Semantics/Modality/Kratzer/Operators.lean::duality` for the - unification opportunity via `Core.Logic.Opposition.Square.fromBox`). -/ + unification opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/ theorem duality {W : Type*} (e : EpistemicState W) (φ : W → Prop) : ¬ knows e (fun w => ¬ φ w) ↔ possible e φ := by simp only [knows, possible, not_forall, not_not, exists_prop] diff --git a/Linglib/Semantics/Attitudes/NegRaising.lean b/Linglib/Semantics/Attitudes/NegRaising.lean index 72c84ee33..072ffc756 100644 --- a/Linglib/Semantics/Attitudes/NegRaising.lean +++ b/Linglib/Semantics/Attitudes/NegRaising.lean @@ -1,5 +1,5 @@ import Linglib.Semantics.Attitudes.Doxastic -import Linglib.Core.Logic.Opposition.Square +import Linglib.Core.Logic.Aristotelian.Square /-! # Neg-Raising as O→E Pragmatic Strengthening @@ -43,7 +43,7 @@ includes cases where p is false, so strengthening to know(¬p) would require namespace Semantics.Attitudes.NegRaising -open Core.Opposition (Square SquareRelations) +open Aristotelian (Square SquareRelations) open Semantics.Attitudes.Doxastic (DoxasticPredicate Veridicality boxAt diaAt AccessRel) diff --git a/Linglib/Semantics/Modality/BiasedPQ.lean b/Linglib/Semantics/Modality/BiasedPQ.lean index 6c776f416..9b7375897 100644 --- a/Linglib/Semantics/Modality/BiasedPQ.lean +++ b/Linglib/Semantics/Modality/BiasedPQ.lean @@ -329,7 +329,7 @@ def evidentialPossibility (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Pro /-- □_ev satisfies modal duality. One of five sibling `theorem duality`s (see `Modality/Kratzer/Operators.lean::duality` for the unification - opportunity via `Core.Logic.Opposition.Square.fromBox`). -/ + opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/ theorem evidentialBias_duality (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : evidentialNecessity f p w ↔ ¬ evidentialPossibility f (fun w' => ¬ p w') w := by unfold evidentialNecessity evidentialPossibility diff --git a/Linglib/Semantics/Modality/EventRelativity.lean b/Linglib/Semantics/Modality/EventRelativity.lean index dafd47119..d244d85aa 100644 --- a/Linglib/Semantics/Modality/EventRelativity.lean +++ b/Linglib/Semantics/Modality/EventRelativity.lean @@ -140,7 +140,7 @@ instance {Event W : Type*} (f : AnchoringFn Event W) (e : Event) /-- Duality: □_{f(e)} p ↔ ¬◇_{f(e)} ¬p. One of five sibling `theorem duality`s (see `Semantics/Modality/Kratzer/Operators.lean::duality` for the - unification opportunity via `Core.Logic.Opposition.Square.fromBox`). -/ + unification opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/ theorem duality {Event W : Type*} (f : AnchoringFn Event W) (e : Event) (allW : List W) (p : W → Prop) [DecidablePred p] (w : W) : necessity f e allW p w ↔ ¬ possibility f e allW (λ w' => ¬ p w') w := by diff --git a/Linglib/Semantics/Modality/Kratzer/Operators.lean b/Linglib/Semantics/Modality/Kratzer/Operators.lean index 6f2ec2420..61a173a09 100644 --- a/Linglib/Semantics/Modality/Kratzer/Operators.lean +++ b/Linglib/Semantics/Modality/Kratzer/Operators.lean @@ -38,7 +38,6 @@ Sources: import Linglib.Semantics.Modality.Kratzer.Ordering import Linglib.Core.Logic.Intensional.RestrictedModality -import Linglib.Core.Logic.Opposition.Aristotelian namespace Semantics.Modality.Kratzer diff --git a/Linglib/Semantics/Modality/Temporal.lean b/Linglib/Semantics/Modality/Temporal.lean index 65a810dee..baf3a0515 100644 --- a/Linglib/Semantics/Modality/Temporal.lean +++ b/Linglib/Semantics/Modality/Temporal.lean @@ -98,7 +98,7 @@ theorem temporal_eq_static {Time : Type*} /-- Temporal duality: □ₜp ↔ ¬◇ₜ¬p. One of five sibling `theorem duality`s (see `Modality/Kratzer/Operators.lean::duality` for the unification - opportunity via `Core.Logic.Opposition.Square.fromBox`). -/ + opportunity via `Core.Logic.Aristotelian.Square.fromBox`). -/ theorem temporal_duality {Time : Type*} (f : TemporalModalBase W Time) (g : TemporalOrderingSource W Time) (t : Time) (p : W → Prop) (w : W) : diff --git a/Linglib/Semantics/Quantification/Syllogistic/Square.lean b/Linglib/Semantics/Quantification/Syllogistic/Square.lean index bf9f991de..e443ba762 100644 --- a/Linglib/Semantics/Quantification/Syllogistic/Square.lean +++ b/Linglib/Semantics/Quantification/Syllogistic/Square.lean @@ -1,5 +1,5 @@ import Linglib.Semantics.Quantification.Syllogistic.Forms -import Linglib.Core.Logic.Opposition.Diagram +import Linglib.Core.Logic.Aristotelian.Diagram /-! # AIEO Square as a Diagram instance @@ -37,7 +37,7 @@ the natural follow-up in `Aristotelian.lean` (TODO). namespace Semantics.Quantification.Syllogistic -open Core.Opposition (AristotelianRel Diagram Contradictory) +open Aristotelian (AristotelianRel Diagram IsContradictory isContradictory_iff_forall) /-! ### Corner indexing -/ @@ -71,7 +71,8 @@ def cornerRel : Corner → Corner → AristotelianRel witness and applying `syllAll`'s universal; the "exhaustion" half is classical LEM on the existence of a Y-counterexample restrictor element. -/ theorem syllAll_contradictory_syllSomeNot (X Y : Region → Bool) : - Contradictory (fun s => syllAll s X Y) (fun s => syllSomeNot s X Y) := by + IsContradictory (fun s => syllAll s X Y) (fun s => syllSomeNot s X Y) := by + rw [isContradictory_iff_forall] refine ⟨?_, ?_⟩ · intro s ⟨hAll, hSomeNot⟩ rw [syllAll_eq_true_iff] at hAll @@ -85,14 +86,15 @@ theorem syllAll_contradictory_syllSomeNot (X Y : Region → Bool) : · right unfold syllSomeNot apply decide_eq_true - push_neg at h + push Not at h obtain ⟨r, hRX, hNotY⟩ := h exact ⟨r, hRX, hNotY⟩ /-- `syllNone` and `syllSome` are contradictories at every state. Symmetric structure to `syllAll_contradictory_syllSomeNot`. -/ theorem syllNone_contradictory_syllSome (X Y : Region → Bool) : - Contradictory (fun s => syllNone s X Y) (fun s => syllSome s X Y) := by + IsContradictory (fun s => syllNone s X Y) (fun s => syllSome s X Y) := by + rw [isContradictory_iff_forall] refine ⟨?_, ?_⟩ · intro s ⟨hNone, hSome⟩ rw [syllNone_eq_true_iff] at hNone @@ -106,7 +108,7 @@ theorem syllNone_contradictory_syllSome (X Y : Region → Bool) : · right unfold syllSome apply decide_eq_true - push_neg at h + push Not at h obtain ⟨r, hRX, hY⟩ := h exact ⟨r, hRX, hY⟩ @@ -116,7 +118,7 @@ theorem syllNone_contradictory_syllSome (X Y : Region → Bool) : Discharges the `contradictory` cases via the lemmas above. The `contrary`/`subcontrary`/`subaltern` cases are vacuous because `cornerRel` labels all non-A↔O / non-E↔I pairs as `unconnected`. -/ -noncomputable def aieoSquare (X Y : Region → Bool) : Diagram Corner VennState where +noncomputable def aieoSquare (X Y : Region → Bool) : Diagram Corner (VennState → Bool) where φ := cornerForm X Y relation := cornerRel relation_correct := by diff --git a/Linglib/Studies/Belnap1970.lean b/Linglib/Studies/Belnap1970.lean index 18c6bce92..fe6a2e7b4 100644 --- a/Linglib/Studies/Belnap1970.lean +++ b/Linglib/Studies/Belnap1970.lean @@ -1,5 +1,5 @@ import Linglib.Semantics.Presupposition.Basic -import Linglib.Core.Logic.Opposition.Square +import Linglib.Core.Logic.Aristotelian.Square import Linglib.Semantics.Quantification.Quantifier import Mathlib.Data.Fintype.Basic @@ -42,7 +42,7 @@ black" = "Consider the crows: each one is black." condition that Belnap derives is exactly what @cite{strawson-1952} stipulated as a presupposition of universals - `content_square_relations`: concrete `SquareRelations` instance from - `Core.Opposition.Square`, connecting to the abstract algebraic framework + `Aristotelian.Square`, connecting to the abstract algebraic framework - `contrapositive_different_assertiveness`: ∀x(Cx/Bx) and ∀x(¬Bx/¬Cx) have different assertiveness conditions — relevant to the confirmation paradox @@ -72,7 +72,7 @@ namespace Belnap1970 open Semantics.Presupposition (PrProp) open Core.Duality (Truth3) -open Core.Opposition (Square SquareRelations) +open Aristotelian (Square SquareRelations) open Semantics.Quantification.Quantifier open Core.Logic.Intensional (Frame) open Semantics.Montague (toyModel ToyEntity) @@ -182,7 +182,7 @@ theorem assertive_iff_restrictor_nonempty {m : Frame} [Fintype m.Entity] -- ════════════════════════════════════════════════════════════════ /-- The **Belnap square**: the four Aristotelian forms as Belnap - restricted quantification, packaged as a `Core.Opposition.Square` + restricted quantification, packaged as a `Aristotelian.Square` of partial propositions (`PrProp Unit`). A: ∀x(Cx/Bx) "All C are B" @@ -255,31 +255,57 @@ theorem content_square_relations {m : Frame} [Fintype m.Entity] [DecidableEq m.E (C B : m.Entity → Bool) (hR : ∃ x : m.Entity, C x = true) : SquareRelations (contentSquare C B) where - contradAO := a_o_contradictory C B - contradEI := e_i_contradictory C B - contraryAE := λ w hA => by - have hEI := e_i_contradictory C B w - rw [hEI]; simp only [Bool.not_eq_false'] - simp only [contentSquare] at * - rw [decide_eq_true_eq] at hA ⊢ - obtain ⟨x, hCx⟩ := hR - exact ⟨x, hCx, hA x hCx⟩ - subalternAI := λ w hA => by - simp only [contentSquare] at * + subalternAI := Aristotelian.le_iff_forall.mpr fun w hA => by + simp only [contentSquare] at hA ⊢ rw [decide_eq_true_eq] at hA ⊢ obtain ⟨x, hCx⟩ := hR exact ⟨x, hCx, hA x hCx⟩ - subalternEO := λ w hE => by - simp only [contentSquare] at * + subalternEO := Aristotelian.le_iff_forall.mpr fun w hE => by + simp only [contentSquare] at hE ⊢ rw [decide_eq_true_eq] at hE ⊢ obtain ⟨x, hCx⟩ := hR exact ⟨x, hCx, hE x hCx⟩ - subcontrIO := λ w hI => by - simp only [contentSquare] at * - rw [decide_eq_false_iff_not] at hI; push Not at hI - obtain ⟨x, hCx⟩ := hR - have hBf := hI x hCx - exact decide_eq_true_eq.mpr ⟨x, hCx, by simp [hBf]⟩ + contradAO := Aristotelian.isContradictory_iff_forall.mpr + ⟨fun w hand => by + have h := a_o_contradictory C B w + rw [hand.1, hand.2] at h; simp at h, + fun w => by + by_cases hO : (contentSquare C B).O w = true + · exact Or.inr hO + · left + have h := a_o_contradictory C B w + rw [show (contentSquare C B).O w = false by simpa using hO] at h + simpa using h⟩ + contradEI := Aristotelian.isContradictory_iff_forall.mpr + ⟨fun w hand => by + have h := e_i_contradictory C B w + rw [hand.1, hand.2] at h; simp at h, + fun w => by + by_cases hI : (contentSquare C B).I w = true + · exact Or.inr hI + · left + have h := e_i_contradictory C B w + rw [show (contentSquare C B).I w = false by simpa using hI] at h + simpa using h⟩ + contraryAE := Aristotelian.disjoint_iff_forall.mpr fun w hand => by + obtain ⟨hA, hE⟩ := hand + have hI : (contentSquare C B).I w = true := by + simp only [contentSquare] at hA ⊢ + rw [decide_eq_true_eq] at hA ⊢ + obtain ⟨x, hCx⟩ := hR + exact ⟨x, hCx, hA x hCx⟩ + have hEI := e_i_contradictory C B w + rw [hI, hE] at hEI; simp at hEI + subcontrIO := Aristotelian.codisjoint_iff_forall.mpr fun w => by + by_cases hI : (contentSquare C B).I w = true + · exact Or.inl hI + · right + have hIf : (contentSquare C B).I w = false := by simpa using hI + simp only [contentSquare] at hIf ⊢ + rw [decide_eq_false_iff_not] at hIf; push Not at hIf + obtain ⟨x, hCx⟩ := hR + have hBf := hIf x hCx + exact decide_eq_true_eq.mpr ⟨x, hCx, by simp [hBf]⟩ -- ════════════════════════════════════════════════════════════════ -- §5. Obversion diff --git a/Linglib/Studies/TesslerTenenbaumGoodman2022.lean b/Linglib/Studies/TesslerTenenbaumGoodman2022.lean index 5df3296b7..c3743c1f8 100644 --- a/Linglib/Studies/TesslerTenenbaumGoodman2022.lean +++ b/Linglib/Studies/TesslerTenenbaumGoodman2022.lean @@ -1,6 +1,6 @@ import Linglib.Semantics.Quantification.Syllogistic.Forms import Linglib.Pragmatics.RSA.Channel -import Linglib.Core.Logic.Opposition.Probabilistic +import Linglib.Core.Logic.Aristotelian.Probabilistic import Mathlib.Analysis.SpecialFunctions.Log.Basic /-! @@ -56,7 +56,7 @@ in this paper, so the asymmetric stance is encoded honestly. ## See also -- `Core.Opposition.Probabilistic` — the Bayesian listener's posterior +- `Aristotelian.Probabilistic` — the Bayesian listener's posterior probabilities `P_μ[c]` jointly satisfy the probabilistic Aristotelian inequalities (subalternation `P[A] ≤ P[I]`, contradiction `P[A]+P[O]=1`, etc.). Tessler's speaker models are functionals of these probabilities; @@ -387,7 +387,8 @@ theorem allAB_allCB_l0_does_not_concentrate : reading: All entails Some (via existential import in `tesslerAll`), and `state_A_AC` witnesses that the converse fails (Some without All). -/ theorem allAC_subaltern_someAC : - Core.Opposition.Subaltern (concMeaning .allAC) (concMeaning .someAC) := by + Aristotelian.IsSubaltern (concMeaning .allAC) (concMeaning .someAC) := by + rw [Aristotelian.isSubaltern_iff_forall] refine ⟨fun s h => all_entails_some_AC s h, ?_⟩ intro hConv have hSome : concMeaning .someAC state_A_AC = true := @@ -403,13 +404,13 @@ theorem allAC_subaltern_someAC : `μ({s | concMeaning c s = true})`. Aristotelian subalternation lifts to this probabilistic level: under any μ, `P_μ[allAC] ≤ P_μ[someAC]`. - The lift is automatic via `Core.Opposition.Subaltern.toProb` once + The lift is automatic via `Aristotelian.ProbSubaltern.of_isSubaltern` once `allAC_subaltern_someAC` is established. The probabilistic Aristotelian diagram (Demey-Smessaert 2018-style, with the convex generalization in `Probabilistic.lean`) is implicitly the framework Tessler's Bayesian listener computes within. -/ theorem prob_subaltern_allAC_someAC (μ : PMF VennState) : - Core.Opposition.ProbSubaltern μ (concMeaning .allAC) (concMeaning .someAC) := - allAC_subaltern_someAC.toProb μ + Aristotelian.ProbSubaltern μ (concMeaning .allAC) (concMeaning .someAC) := + Aristotelian.ProbSubaltern.of_isSubaltern allAC_subaltern_someAC μ end TesslerTenenbaumGoodman2022 diff --git a/blog/references.bib b/blog/references.bib index 514b17c92..bf43b50ca 100644 --- a/blog/references.bib +++ b/blog/references.bib @@ -429,7 +429,63 @@ @article{demey-smessaert-2018 subfield = {logic/opposition}, validated = {true}, role = {formalized}, - sources = {Core/Logic/Opposition/Aristotelian.lean, Core/Logic/Opposition/Diagram.lean, Core/Logic/Opposition/Probabilistic.lean, Core/Logic/Opposition/Partition.lean, Core/Logic/Opposition/Bitstring.lean} + sources = {Core/Logic/Aristotelian/Basic.lean, Core/Logic/Aristotelian/Diagram.lean, Core/Logic/Aristotelian/Probabilistic.lean, Core/Logic/Aristotelian/Partition.lean, Core/Logic/Aristotelian/Bitstring.lean} +} +@article{smessaert-demey-2014, + author = {Smessaert, Hans and Demey, Lorenz}, + year = {2014}, + title = {Logical Geometries and Information in the Square of Oppositions}, + journal = {Journal of Logic, Language and Information}, + volume = {23}, + number = {4}, + pages = {527--565}, + doi = {10.1007/s10849-014-9207-y}, + subfield = {logic/opposition}, + validated = {true}, + role = {formalized}, + sources = {Core/Logic/Aristotelian/Basic.lean} +} +@article{demey-frijters-2023, + author = {Demey, Lorenz and Frijters, Stef}, + year = {2023}, + title = {Logic-Sensitivity and Bitstring Semantics in the Square of Opposition}, + journal = {Journal of Philosophical Logic}, + volume = {52}, + number = {6}, + pages = {1703--1721}, + doi = {10.1007/s10992-023-09723-6}, + subfield = {logic/opposition}, + validated = {true}, + role = {cited}, + sources = {Core/Logic/Aristotelian/Basic.lean} +} +@article{deklerck-vignero-demey-2024, + author = {De Klerck, Alexander and Vignero, Leander and Demey, Lorenz}, + year = {2024}, + title = {Morphisms Between Aristotelian Diagrams}, + journal = {Logica Universalis}, + volume = {18}, + number = {1-2}, + pages = {49--83}, + doi = {10.1007/s11787-023-00340-0}, + subfield = {logic/opposition}, + validated = {true}, + role = {cited}, + sources = {Core/Logic/Aristotelian/Basic.lean} +} +@article{demey-smessaert-2024, + author = {Demey, Lorenz and Smessaert, Hans}, + year = {2024}, + title = {Aristotelian and {Boolean} Properties of the {Keynes}-{Johnson} Octagon of Opposition}, + journal = {Journal of Philosophical Logic}, + volume = {53}, + number = {5}, + pages = {1265--1290}, + doi = {10.1007/s10992-024-09765-4}, + subfield = {logic/opposition}, + validated = {true}, + role = {cited}, + sources = {Core/Logic/Aristotelian/Basic.lean, Core/Logic/Aristotelian/Diagram.lean} } @inproceedings{scontras-tonhauser-2025, author = {Scontras, Gregory and Tonhauser, Judith},