small improvements

Author: hjvromen

Sillari_refutation.lean

@@ -414,18 +414,25 @@ indicators. Lewis's entire proof collapses.
 -/
 
 lemma B3_fails
-    (h2a : ¬ frame.rel i s s)
-    (h2b : frame.rel i s t) :
+    (h2 : two_worlds s t)
+    (hst : frame.rel i s t) :
     ∃ (w : frame.World) (φ ψ : frame.World → Prop), R i φ w ∧ Ind i φ ψ w ∧ ¬ R i ψ w := by
   let w := s
   let ψ := fun w => w ≠ t
-  let φ := fun w => w ≠ s
+  let φ : frame.World → Prop := fun _ => True
   have h4 : R i φ s := by intro v hv; aesop
-  have h5 : Ind i φ ψ s := by rw [Ind]; aesop
+  have h5 : Ind i φ ψ s := by
+    constructor
+    · exact h4
+    · intro _
+      -- Need to prove ψ s, i.e., s ≠ t
+      -- From h2 : two_worlds s t, we have t ≠ s
+      have hts : t ≠ s := h2; exact hts.symm
   have h6 : ¬ R i ψ s := by aesop
   exact ⟨s, φ, ψ, h4, h5, h6⟩
 
 
+
 /-!
 ### Axiom `B4`: Transitivity of indication
 
@@ -582,22 +589,70 @@ Target: ψ = "at world s"
 **Conclusion:** `C4` fails in this Kripke frame.
 -/
 
-lemma C4_fails
-    (h2a : ¬ frame.rel i s s)
-    (h2b : frame.rel i s t):
-    ∃ (w : frame.World) (φ ψ : frame.World → Prop), (Ind i φ ψ w ∧ ¬ R i (Ind j φ ψ) w) := by
-  let φ := fun _ : frame.World => True
-  let ψ := fun w : frame.World => w = s
-  have h3 : Ind i φ ψ s := by
-    constructor
-    { intro w _; aesop }  -- R i True s (trivial)
-    { aesop }
-  have h3a : ¬ R i (Ind j φ ψ) s := by
-    rw [R]; push_neg; use t
-    constructor
-    · exact h2b
-    · intro hn; have hp : ψ t := hn.2 trivial; aesop
-  exact ⟨s, φ, ψ, h3, h3a⟩
+lemma C4_fails {i1 i2 : Agent}
+    (h1 : three_worlds s u v)
+    (h2 : two_agents i1 i2)
+    (h3 : frame.rel = fun i w1 w2 =>
+      (i = i1 ∧ w1 = s ∧ w2 = u) ∨
+      (w1 = v ∧ w2 = v) ∨
+      (i = i2 ∧ w1 = s ∧ w2 = s) ∨
+      (i = i2 ∧ w1 = u ∧ w2 = v)) :
+    ∃ (w : frame.World) (φ ψ : frame.World → Prop), (Ind i1 φ ψ w ∧ ¬ R i1 (Ind i2 φ ψ) w) := by
+  -- Extract the inequalities from three_worlds
+  obtain ⟨hus, hvu, hvs⟩ : u ≠ s ∧ v ≠ u ∧ v ≠ s := by
+    simpa [three_worlds] using h1
+
+  -- Define φ and ψ
+  let φ : frame.World → Prop := fun w => w ≠ v
+  let ψ : frame.World → Prop := fun w => w ≠ v
+
+  -- We'll show the counterexample holds at world s
+  use s, φ, ψ
+  constructor
+
+  -- Part 1: Show Ind i1 φ ψ s
+  · constructor
+    -- Show R i1 φ s
+    · intro w hw
+      -- If i1 can see w from s, then w = u (by h3)
+      have hw_eq : w = u := by
+        have : (i1 = i1 ∧ s = s ∧ w = u) ∨ (s = v ∧ w = v) ∨
+               (i1 = i2 ∧ s = s ∧ w = s) ∨ (i1 = i2 ∧ s = u ∧ w = v) := by
+          simpa [h3] using hw
+        cases this with
+        | inl h => exact h.2.2
+        | inr h => cases h with
+          | inl h' => exact (hvs h'.1.symm).elim
+          | inr h' => cases h' with
+            | inl h'' => exact (h2.1 h''.1).elim
+            | inr h'' => exact (h2.1 h''.1).elim
+      -- Since w = u and u ≠ v, we have φ w
+      rw [hw_eq]
+      show u ≠ v
+      exact Ne.symm hvu
+    -- Show φ s → ψ s (trivial since φ = ψ)
+    · intro _; assumption
+
+  -- Part 2: Show ¬ R i1 (Ind i2 φ ψ) s
+  · intro hcontra
+    -- If R i1 (Ind i2 φ ψ) s, then Ind i2 φ ψ u (since i1 sees u from s)
+    have rel_s_u : frame.rel i1 s u := by
+      rw [h3]; left; exact ⟨rfl, rfl, rfl⟩
+    have hInd_u : Ind i2 φ ψ u := hcontra u rel_s_u
+
+    -- From Ind i2 φ ψ u, we get R i2 φ u
+    have hR2_u : R i2 φ u := hInd_u.1
+
+    -- But i2 can see v from u (by h3)
+    have rel_u_v : frame.rel i2 u v := by
+      rw [h3]; right; right; right; exact ⟨rfl, rfl, rfl⟩
+
+    -- So φ v must hold, i.e., v ≠ v
+    have : φ v := hR2_u v rel_u_v
+
+    -- But this is a contradiction
+    exact this rfl
+
 
 /-!
 ---

Vromen_justification_logic.lean

@@ -575,9 +575,10 @@ This captures common knowledge as an infinite hierarchy of nested reasons to bel
 Everyone believes `φ`, everyone believes everyone believes `φ`, and so on forever.
 -/
 
-inductive Gclosure (φ : Prop) : Prop → Prop
-  | base : Gclosure φ φ
-  | step (p : Prop) (i : individual) : Gclosure φ p → Gclosure φ (R rb i p)
+inductive Rclosure (rb : reason → individual → Prop → Prop) (φ : Prop) : Prop → Prop
+  | base : Rclosure rb φ φ
+  | step (p : Prop) (i : individual) : Rclosure rb φ p → Rclosure rb φ (R rb i p)
+
 
 /-!
 ### Lewis's Theorem on Common Knowledge
@@ -627,7 +628,7 @@ theorem Lewis (A φ : Prop) (p : Prop)
     (C2 : ∀ i j, Ind rb A i (R rb j A))
     (C3 : ∀ i, Ind rb A i φ)
     (C4 : ∀ α i j, Ind rb A i α → R rb i (Ind rb A j α))
-    (h7 : @Gclosure individual reason rb φ p) :
+    (h7 : Rclosure rb φ p) :
     ∀ i, R rb i p := by
   intro i
   -- Prove stronger claim: Ind A i p (then use A1 + C1)