reavowed comments on Troll Bridge

reavowed 28 Aug 2019 23:16 UTC
7 points
I’m having difficulty following the line of the proof beginning “so, either way, PA is inconsistent”. We have $□ (A = cross \Rightarrow U = - 10)$ and $□ (A = cross \Rightarrow U \neq - 10)$ , which together imply that $□ (A \neq cross)$ , but I’m not immediately seeing how this leads to $□ ⊥$ ?
- reavowed 31 Aug 2019 10:18 UTC
  5 points
  Parent
  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 $□ ⊥$ .