Timeline for Consistency proof in topos logic
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 23, 2021 at 20:39 | comment | added | Paul Blain Levy | @PeterLeFanuLumsdaine I've found a reference, Troelstra and van Dalen "Constructivism in Mathematics, an introduction", Volume 1, Chapter 3, Section 9.3. I should have searched before asking you! | |
| Oct 23, 2021 at 20:14 | comment | added | Peter LeFanu Lumsdaine | @PaulBlainLevy: off the top of my head, I’m not sure of a reference that gives it syntactically — my first hope was Lambek & Scott, but I can’t find it there. Mac Lane and Moerdijk Theorem VI.1.3 shows that “in any topos, the subtopos of $\lnot \lnot$-sheaves is Boolean”, which directly implies the syntactic translation. | |
| Oct 23, 2021 at 19:44 | comment | added | Paul Blain Levy | @PeterLeFanuLumsdaine is there a reference for that double-negation translation? So that I can refer to it without having to write it out. | |
| Oct 23, 2021 at 19:36 | comment | added | Paul Blain Levy | Thanks! I have accordingly removed the supplement to my question. It claimed that Bounded Zermelo is conservative over PA$_{\omega}$, and I'm not entirely sure of this, though it does seem plausible. | |
| Oct 22, 2021 at 7:15 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 550 characters in body
|
| Oct 22, 2021 at 7:11 | comment | added | Andrej Bauer |
@PaulBlainLevy: \nat is self-explanatory, I wouldn't worry about it. But to explain what your comment is about, I added an explanation.
|
|
| Oct 22, 2021 at 0:50 | vote | accept | Paul Blain Levy | ||
| Oct 22, 2021 at 0:49 | comment | added | Paul Blain Levy | \nats should be $\mathbb{N}$ in my comment. | |
| Oct 19, 2021 at 6:37 | comment | added | Peter LeFanu Lumsdaine | Another way to see this answer is: $HOL_N$ (classical higher-order logic with NNO; the logic of a Boolean topos with NMO) clearly proves the consistency of each $PA_n$. But $HOL_N$ translates into $IHOL_N$ via the double-negation translation. | |
| Oct 19, 2021 at 6:23 | comment | added | Paul Blain Levy | Great answer, Andrej, but I think you slightly overstated. What this shows is that, for each $n \in \nats$, topos-with-nno logic can build a model of PA$_{n+1}$. I've edited my question to make this clearer. | |
| Oct 19, 2021 at 5:40 | comment | added | Paul Blain Levy | [Deleted earlier comment - I hadn't read your message carefully.] | |
| Oct 17, 2021 at 20:08 | history | answered | Andrej Bauer | CC BY-SA 4.0 |