Book chapter 840 views
On the constructive and computational content of abstract mathematics
Ulrich Berger 
Mathesis Universalis, Computability and Proof, Volume: Synthese Library - Studies in Epistemology, Logic, Methodology, and Philosophy of Science
Swansea University Author:
Ulrich Berger
Abstract
This essay describes an approach to constructive mathematics based on abstract i.e. axiomatic mathematics. Rather than insisting on structures to be explicitly constructed, constructivity is dened by the sole requirement that proofs have computational content. It is shown that this approach is compa...
| Published in: | Mathesis Universalis, Computability and Proof |
|---|---|
| Published: |
2019
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa50301 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
This essay describes an approach to constructive mathematics based on abstract i.e. axiomatic mathematics. Rather than insisting on structures to be explicitly constructed, constructivity is dened by the sole requirement that proofs have computational content. It is shown that this approach is compatible with restricted forms of classical logic and choice principles. |
|---|---|
| Keywords: |
constructive mathematics, realizability, program extraction, choice principles |
| College: |
Faculty of Science and Engineering |