Timeline for In what way is the lambda calculus stronger than first-order logic?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 16, 2013 at 22:40 | vote | accept | Mozibur Ullah | ||
| Aug 14, 2013 at 0:39 | comment | added | Dennis | Ah! Here it is. I think what I was remembering was the "I see why the strategy should work" and the "I believe I will believe it" bits. I definitely overstated the claim, though. | |
| Aug 14, 2013 at 0:36 | comment | added | Dennis | It was definitely TST+Inf that I've read Holmes claiming it was equiconsistent with. I can't find what I was reading recently, so I'm stepping back from the "people are optimistic" claim. I vaguely remember it being on the logic matters blog but a quick search didn't turn up anything. Thomas Forster is working through the proof with some students, I believe. The only recent mention I could find is here. | |
| Aug 13, 2013 at 0:25 | comment | added | Thomas Klimpel | @Dennis Perhaps, but the connection to Mac Lane set theory depends on the interpretation of the available tidbits. As Aatu Koskensilta said on the linked page: "TST + Infinity has the same consistency strength as bounded Zermelo set theory." However, later tidbits talked about ZFU instead of TST, so these are still rumors for me. Of course, the goal must be to prove NF equiconsistent with a "predicative mathematics" system, because the idea behind stratification is that it should lead to predicativity. | |
| Aug 12, 2013 at 20:21 | comment | added | Dennis | Also, the rumors are no longer rumors. Holmes presented a proof sketch at a Cambridge gathering. His proof has yet to be confirmed (I believe the sketch is about 40 pages), but people seem optimistic that he was successful. | |
| Aug 12, 2013 at 8:31 | history | answered | Thomas Klimpel | CC BY-SA 3.0 |