Name
Abstract | ||
|---|---|---|
A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTT0 and LTT0∗, which we claim correspond closely to the classical predicative systems of second order arithmetic ACA0 and ACA. We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches to the foundations of mathematics. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1016/j.apal.2010.04.005 | Annals of Pure and Applied Logic |
Keywords | DocType | Volume |
03B15,03B30,03F25,03F35 | Journal | 161 |
Issue | ISSN | Citations |
11 | 0168-0072 | 1 |
PageRank | References | Authors |
0.35 | 8 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Robin Adams | 1 | 60 | 11.61 |
| Zhaohui Luo | 2 | 328 | 38.91 |