No Cover Image

Book chapter 883 views

On the Computational Content of Choice Principles

Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo

Handbook of Constructive Mathematics, Pages: 806 - 825

Swansea University Authors: Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo

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

DOI (Published version): 10.1017/9781009039888.030

Abstract

We discuss the computational content of various choice principles and theorems using them. As a case study, we describe the computational content of Nash-Williams' proof of Higman's Lemma, which uses the axiom of countable choice in combination with classical logic. Our formal system for t...

Full description

Published in: Handbook of Constructive Mathematics
ISBN: 9781316510865 9781009039888
Published: Cambridge University Press 2023
Online Access: http://dx.doi.org/10.1017/9781009039888.030
URI: https://cronfa.swan.ac.uk/Record/cronfa57994
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2021-09-21T08:24:00Z
last_indexed 2023-01-11T14:38:16Z
id cronfa57994
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>57994</id><entry>2021-09-20</entry><title>On the Computational Content of Choice Principles</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><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2021-09-20</date><deptcode>SCS</deptcode><abstract>We discuss the computational content of various choice principles and theorems using them. As a case study, we describe the computational content of Nash-Williams' proof of Higman's Lemma, which uses the axiom of countable choice in combination with classical logic. Our formal system for the extraction of computational content from proofs is a realizability interpretation of an intuitionistic theory of inductive and coinductive definitions as implemented in the Minlog system.</abstract><type>Book chapter</type><journal>Handbook of Constructive Mathematics</journal><volume/><journalNumber/><paginationStart>806</paginationStart><paginationEnd>825</paginationEnd><publisher>Cambridge University Press</publisher><placeOfPublication/><isbnPrint>9781316510865</isbnPrint><isbnElectronic>9781009039888</isbnElectronic><issnPrint/><issnElectronic/><keywords/><publishedDay>30</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-04-30</publishedDate><doi>10.1017/9781009039888.030</doi><url>http://dx.doi.org/10.1017/9781009039888.030</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2024-02-09T13:02:18.2866771</lastEdited><Created>2021-09-20T22:06:43.1553328</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><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid>0000-0002-2226-386X</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling v2 57994 2021-09-20 On the Computational Content of Choice Principles 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 2021-09-20 SCS We discuss the computational content of various choice principles and theorems using them. As a case study, we describe the computational content of Nash-Williams' proof of Higman's Lemma, which uses the axiom of countable choice in combination with classical logic. Our formal system for the extraction of computational content from proofs is a realizability interpretation of an intuitionistic theory of inductive and coinductive definitions as implemented in the Minlog system. Book chapter Handbook of Constructive Mathematics 806 825 Cambridge University Press 9781316510865 9781009039888 30 4 2023 2023-04-30 10.1017/9781009039888.030 http://dx.doi.org/10.1017/9781009039888.030 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2024-02-09T13:02:18.2866771 2021-09-20T22:06:43.1553328 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Monika Seisenberger 0000-0002-2226-386X 2
title On the Computational Content of Choice Principles
spellingShingle On the Computational Content of Choice Principles
Ulrich Berger
Monika Seisenberger
title_short On the Computational Content of Choice Principles
title_full On the Computational Content of Choice Principles
title_fullStr On the Computational Content of Choice Principles
title_full_unstemmed On the Computational Content of Choice Principles
title_sort On the Computational Content of Choice Principles
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
d035399b2b324a63fe472ce0344653e0
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger
author Ulrich Berger
Monika Seisenberger
author2 Ulrich Berger
Monika Seisenberger
format Book chapter
container_title Handbook of Constructive Mathematics
container_start_page 806
publishDate 2023
institution Swansea University
isbn 9781316510865
9781009039888
doi_str_mv 10.1017/9781009039888.030
publisher Cambridge University Press
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
url http://dx.doi.org/10.1017/9781009039888.030
document_store_str 0
active_str 0
description We discuss the computational content of various choice principles and theorems using them. As a case study, we describe the computational content of Nash-Williams' proof of Higman's Lemma, which uses the axiom of countable choice in combination with classical logic. Our formal system for the extraction of computational content from proofs is a realizability interpretation of an intuitionistic theory of inductive and coinductive definitions as implemented in the Minlog system.
published_date 2023-04-30T13:02:17Z
_version_ 1790426468065476608
score 11.035634

Similar Items