×

The generalised type-theoretic interpretation of constructive set theory. (English) Zbl 1100.03052

Summary: We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.

MSC:

03F50 Metamathematics of constructive systems
03E70 Nonclassical and second-order set theories
03F25 Relative consistency and interpretations
03F35 Second- and higher-order arithmetic and fragments
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] DOI: 10.1016/j.apal.2004.08.002 · Zbl 1068.03045 · doi:10.1016/j.apal.2004.08.002
[2] Mathematical Structures in Computer Science
[3] Sheaves in Geometry and Logic (1992)
[4] Twenty-five years of Constructive Type Theory pp 221– (1998)
[5] DOI: 10.1016/S0168-0072(03)00052-6 · Zbl 1070.03041 · doi:10.1016/S0168-0072(03)00052-6
[6] DOI: 10.1016/S0304-3975(02)00704-1 · Zbl 1044.54001 · doi:10.1016/S0304-3975(02)00704-1
[7] Theory and applications of categories 15 pp 1– (2005)
[8] Mathematical Logic and its Applications pp 87– (1987)
[9] DOI: 10.1093/logcom/14.4.447 · Zbl 1050.03016 · doi:10.1093/logcom/14.4.447
[10] DOI: 10.1002/malq.200310054 · Zbl 1042.03040 · doi:10.1002/malq.200310054
[11] Logic colloquium ’03 24 pp 282– (2006)
[12] DOI: 10.1007/3-540-45842-5_1 · doi:10.1007/3-540-45842-5_1
[13] DOI: 10.1016/j.apal.2005.05.010 · Zbl 1073.03030 · doi:10.1016/j.apal.2005.05.010
[14] Logic, methodology and philosophy of science VII pp 17– (1986)
[15] The disjunction and related properties for Constructive Zermelo-Frankel Set Theory 70 pp 1233– (2005)
[16] The L. E. J. Brouwer Centenary Symposium pp 1– (1982)
[17] Handbook of Logic in Computer Science 5 (2000)
[18] Logic Colloquium ’77 pp 55– (1978)
[19] Constructive Set Theory 40 pp 347– (1975) · Zbl 0314.02045
[20] DOI: 10.1016/S0168-0072(01)00079-3 · Zbl 0999.03061 · doi:10.1016/S0168-0072(01)00079-3
[21] Stone spaces (1982) · Zbl 0499.54001
[22] Categorical logic and type theory (1999) · Zbl 0911.03001
[23] DOI: 10.1007/BF01278464 · Zbl 0819.03047 · doi:10.1007/BF01278464
[24] Forcing in intuitionistic systems without power-set 48 pp 670– (1983)
[25] DOI: 10.1007/BFb0061825 · doi:10.1007/BFb0061825
[26] DOI: 10.1016/j.apal.2005.05.021 · Zbl 1077.03038 · doi:10.1016/j.apal.2005.05.021
[27] DOI: 10.1093/acprof:oso/9780198566519.003.0004 · doi:10.1093/acprof:oso/9780198566519.003.0004
[28] Laurea dissertation (1999)
[29] DOI: 10.2307/1971023 · Zbl 0353.02014 · doi:10.2307/1971023
[30] DOI: 10.1016/S0168-0072(00)00012-9 · Zbl 1010.03056 · doi:10.1016/S0168-0072(00)00012-9
[31] Intuitionistic type theory – Notes by G. Sambin of a series of lectures given in Padua, June 1980 (1984)
[32] Logic Colloquium ’95 11 pp 153– (1998)
[33] DOI: 10.1093/acprof:oso/9780198566519.003.0006 · doi:10.1093/acprof:oso/9780198566519.003.0006
[34] The consistency of classical set theory relative to a set theory with intuitionistic logic 38 pp 315– (1973) · Zbl 0278.02045
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.