Book chapter 372 views
On the computational content of choice principles
Ulrich Berger 
,
Monika Seisenberger
,
Monika Seisenberger
Handbook of Bishop Constructive Mathematics
Swansea University Authors:
Ulrich Berger , Monika Seisenberger
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 Bishop Constructive Mathematics |
|---|---|
| ISBN: | 9781009039888 |
| Published: |
Cambridge University Press
2023
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa57994 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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 |