Timeline for Proof strength of Calculus of (Inductive) Constructions
Current License: CC BY-SA 3.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 2, 2011 at 0:46 | comment | added | David Roberts♦ | Thanks, Neel! I had a quick browse of Werner's article while posing this question. But it is the latter part of your answer which is really useful. I was uncertain as to whether restricting one's allowed fragment of logic (to constructive or otherwise) had any bearing on consistency strength. Naively it might have done, but I'm becoming convinced that we are dealing with two separate foundational 'axes' here. | |
| Jul 1, 2011 at 10:56 | history | answered | Neel Krishnaswami | CC BY-SA 3.0 |