The inconsistency of higher order extensions of Martin-Löf's type theory (Q583201)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | The inconsistency of higher order extensions of Martin-Löf's type theory |
scientific article |
Statements
The inconsistency of higher order extensions of Martin-Löf's type theory (English)
0 references
1989
0 references
The author shows the inconsistency of the higher order system resulting from addition of the axiom PROP:SET, i.e. the category of propositions is a set, to Martin-Löf's constructive type theory. Inconsistency also results for a more restricted extension obtained by adding two new category objects to constructive second order logic.
0 references
constructive higher order systems
0 references
inconsistency
0 references
Martin-Löf's constructive type theory
0 references
