minor changes

Author: hjvromen

Cubitt_Sugden_baseline.lean

@@ -156,7 +156,7 @@ Like `A1`, this cannot be derived from primitive operators.
 Vromen proves it as a theorem from the compositional structure of reason terms.
 -/
 
-variable (A6 : ∀ {i j : indiv} {u : Prop}, Ind A i (R j A) ∧ R i (Ind A j u) → Ind A i (R j u))
+variable (A6 : ∀ {i j : indiv} {p: Prop}, Ind A i (R j A) ∧ R i (Ind A j p) → Ind A i (R j p))
 
 /-!
 ---
@@ -199,9 +199,9 @@ variable (C3 : ∀ i : indiv, Ind A i φ)
 /-!
 ### Condition `C4`: Shared Inductive Standards
 
-If `A` indicates `u` to `i`, then `i` has reason to believe that `A` indicates `u` to `j`.
+If `A` indicates `p` to `i`, then `i` has reason to believe that `A` indicates `p` to `j`.
 
-> **Formula:** `Ind A i u → R i (Ind A j u)`
+> **Formula:** `Ind A i p → R i (Ind A j p)`
 
 This formalizes shared reasoning standards—agents know they reason alike.
 This formalizes Lewis' assumption about "common inductive standards and background information".
@@ -212,7 +212,7 @@ necessary - we only need it for certain types of propositions. But it
 simplifies the formalization.
 -/
 
-variable (C4 : ∀ {i j : indiv} {u : Prop}, Ind A i u → R i (Ind A j u))
+variable (C4 : ∀ {i j : indiv} {p : Prop}, Ind A i p → R i (Ind A j p))
 
 include A1 A6 C1 C2 C3 C4
 
@@ -349,7 +349,7 @@ The R-closure of `φ` is the smallest set of propositions that:
 
 inductive RC (φ : Prop) : Prop → Prop where
   | base : RC φ φ
-  | step {u : Prop} (j : indiv) (hu : RC φ u) : RC φ (R j u)
+  | step {p : Prop} (j : indiv) (hu : RC φ p) : RC φ (R j p)
 
 /-!
 ### Key Lemma: Indication Propagates Through R-Closure
@@ -366,7 +366,7 @@ indicate not just `φ`, but all its higher-order iterations.
 -/
 
 omit A1 C1 in
-lemma rc_implies_indication {i : indiv} {q : Prop} (h : @RC indiv R φ q) : Ind A i q := by
+lemma indication_closure {i : indiv} {q : Prop} (h : @RC indiv R φ q) : Ind A i q := by
   induction h with
   | base => exact C3 i
   | @step v j _ ih =>
@@ -388,11 +388,12 @@ in `P` that `x`, then `r^P(x)` is true."
 **Significance:** Common knowledge is not an infinite regress (circular) but an infinite *consequence*of finite, non-circular conditions.
 -/
 
-lemma everyone_reason_of_rc (hp : @RC indiv R φ p) : ∀ i : indiv, R i p := by
+lemma lewis_theorem (hp : @RC indiv R φ p) : ∀ i : indiv, R i p := by
   intro i
-  have hInd : Ind A i p := rc_implies_indication A φ A6 C2 C3 C4 hp
+  have hInd : Ind A i p := indication_closure A φ A6 C2 C3 C4 hp
   exact A1 hInd (C1 i)
 
+
 end Lewis
 
 /-!