No Cover Image

Book chapter 178 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...

Full description

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: College of Science