Journal article 1095 views
Classical truth in higher types
Ulrich Berger 
MLQ, Volume: 54, Issue: 3, Pages: 240 - 246
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1002/malq.200710046
Abstract
We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of continuous functionals, hereditarily effe...
| Published in: | MLQ |
|---|---|
| ISSN: | 0942-5616 1521-3870 |
| Published: |
2008
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa7436 |
| Abstract: |
We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of continuous functionals, hereditarily effective operations, as well as the closed term model of Gödel's system T. The main results are characterisations of prenex classes for which truth in the full set-theoretic model transfers to truth in the other models. As a corollary we obtain that the axiom of choice is not conservative over Gödel's system T with classical logic for closed Sigma-2-formulas. We hope that this study will contribute to a clearer delineation and perception of constructive mathematics from a classical perspective. |
|---|---|
| Keywords: |
logic, higher types, constructive mathematics |
| College: |
Faculty of Science and Engineering |
| Issue: |
3 |
| Start Page: |
240 |
| End Page: |
246 |