No Cover Image

Journal article 1095 views

Classical truth in higher types

Ulrich Berger Orcid Logo

MLQ, Volume: 54, Issue: 3, Pages: 240 - 246

Swansea University Author: Ulrich Berger Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

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...

Full description

Published in: MLQ
ISSN: 0942-5616 1521-3870
Published: 2008
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa7436
first_indexed 2013-07-23T11:58:19Z
last_indexed 2018-02-09T04:35:36Z
id cronfa7436
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-06-14T12:56:46.3694461</datestamp><bib-version>v2</bib-version><id>7436</id><entry>2012-02-23</entry><title>Classical truth in higher types</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-02-23</date><deptcode>MACS</deptcode><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&#xF6;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&#xF6;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.</abstract><type>Journal Article</type><journal>MLQ</journal><volume>54</volume><journalNumber>3</journalNumber><paginationStart>240</paginationStart><paginationEnd>246</paginationEnd><publisher/><placeOfPublication/><issnPrint>0942-5616</issnPrint><issnElectronic>1521-3870</issnElectronic><keywords>logic, higher types, constructive mathematics</keywords><publishedDay>31</publishedDay><publishedMonth>5</publishedMonth><publishedYear>2008</publishedYear><publishedDate>2008-05-31</publishedDate><doi>10.1002/malq.200710046</doi><url/><notes></notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-06-14T12:56:46.3694461</lastEdited><Created>2012-02-23T17:01:55.0000000</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-06-14T12:56:46.3694461 v2 7436 2012-02-23 Classical truth in higher types 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2012-02-23 MACS 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. Journal Article MLQ 54 3 240 246 0942-5616 1521-3870 logic, higher types, constructive mathematics 31 5 2008 2008-05-31 10.1002/malq.200710046 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2013-06-14T12:56:46.3694461 2012-02-23T17:01:55.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1
title Classical truth in higher types
spellingShingle Classical truth in higher types
Ulrich Berger
title_short Classical truth in higher types
title_full Classical truth in higher types
title_fullStr Classical truth in higher types
title_full_unstemmed Classical truth in higher types
title_sort Classical truth in higher types
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
format Journal article
container_title MLQ
container_volume 54
container_issue 3
container_start_page 240
publishDate 2008
institution Swansea University
issn 0942-5616
1521-3870
doi_str_mv 10.1002/malq.200710046
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2008-05-31T06:14:44Z
_version_ 1821384988954722304
score 11.04748

Similar Items