A minimalist two-level foundation for constructive mathematics
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2008
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929300689649664 |
|---|---|
| author | Maietti, Maria Emilia |
| author_facet | Maietti, Maria Emilia |
| contents | We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minimal type theory. This theory extends the set-theoretic version introduced in the mentioned paper with collections. The other level is given by an extensional set theory which is interpreted in the first one by means of a quotient model. This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the "proofs-as-programs" paradigm and acts as a programming language. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_0811_2774 |
| institution | arXiv |
| publishDate | 2008 |
| record_format | arxiv |
| spellingShingle | A minimalist two-level foundation for constructive mathematics Maietti, Maria Emilia Logic 03G30, 03B15, 18C50, 03B20, 03F55 We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minimal type theory. This theory extends the set-theoretic version introduced in the mentioned paper with collections. The other level is given by an extensional set theory which is interpreted in the first one by means of a quotient model. This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the "proofs-as-programs" paradigm and acts as a programming language. |
| title | A minimalist two-level foundation for constructive mathematics |
| topic | Logic 03G30, 03B15, 18C50, 03B20, 03F55 |
| url | https://arxiv.org/abs/0811.2774 |