reavowed comments on Troll Bridge

reavowed 31 Aug 2019 10:18 UTC
5 points
Ah, got there. From $□ (A \neq cross)$ , we get specifically $□ (A = cross \Rightarrow U = 10)$ and thus $□ □ (A = cross \Rightarrow U = 10)$ . But we have $□ (A = cross \Rightarrow U = 10) \Rightarrow A = cross$ directly as a theorem (axiom?) about the behaviour of $A$ , and we can lift this to $□ □ (A = cross \Rightarrow U = 10) \Rightarrow □ (A = cross)$ , so $□ (A = cross)$ also and thus $□ ⊥$ .