Constructive theory of sets with types; compatibility with Church's thesis (Q1080424)
From MaRDI portal
| This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Constructive theory of sets with types; compatibility with Church's thesis |
scientific article; zbMATH DE number 3966071
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Constructive theory of sets with types; compatibility with Church's thesis |
scientific article; zbMATH DE number 3966071 |
Statements
Constructive theory of sets with types; compatibility with Church's thesis (English)
0 references
1984
0 references
The author formulates an intuitionistic theory with types for sets and functions, intended for formalizing constructive analysis. It is shown that this theory is compatible with a version of Church's thesis and that it can be interpreted in classical second order arithmetic.
0 references
intuitionistic theory with types for sets and functions
0 references
formalizing constructive analysis
0 references
second order arithmetic
0 references
0.7847130298614502
0 references
0.7798859477043152
0 references