Book chapter 1382 views
On the Computational Content of Choice Principles
Ulrich Berger,
Monika Seisenberger 
Handbook of Constructive Mathematics, Pages: 806 - 825
Swansea University Authors:
Ulrich Berger, Monika Seisenberger
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...
| 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 |
| 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. |
|---|---|
| College: |
Faculty of Science and Engineering |
| Start Page: |
806 |
| End Page: |
825 |