A minimalist two-level foundation for constructive mathematics (Q1032635)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A minimalist two-level foundation for constructive mathematics |
scientific article |
Statements
A minimalist two-level foundation for constructive mathematics (English)
0 references
26 October 2009
0 references
The author develops a formal theory for constructive mathematics along the minimalist lines she and G. Sambin have advocated. This theory has two components, or levels: a ``minmal'' intensional constructive type theory and an extensional set theory. The former may be regarded as a ``programming'' language embodying the ``proofs-as-programs'' doctrine, and the latter as the level at which actual mathematical proofs are formalized. It is shown how to interpret the extensional theory in an enlargement of the intensional theory obtained by adjoining quotient sets.
0 references
constructive mathematics
0 references
intensional constructive type theory
0 references
extensional set theory
0 references
0 references
