Intuitionistic choice and classical logic
type: Item
instance of: scholarly article
title: Intuitionistic choice and classical logic
zbMATH Open document ID: 0947.03078
author: Thierry Coquand
author: Erik Palmgren
published in: Archive for Mathematical Logic
publication date: 2000-11-05T00:00:00Z
review text: Many mathematical results are proven by using non-constructive methods. Sometimes, however, it is possible to re-prove the same result in a more constructive manner. This re-proof is often more complex than the original proof, but it has its advantages: first, if the result stated the existence of an object, the more constructive the proof, the closer we are to actually constructing this object; second, in general, the more constructive the proof, the more reliable the statement. The authors show that a large part of analysis can be formulated and proven within a theory which combines the classical logic's law of excluded middle for ``arithmetic'' statements \(\forall n An\) with decidable \(A\) (\(\forall n(An\vee\neg An)\) implies \(\forall n An\vee \exists n \neg An\)) with an appropriate axiom of choice for sequences (e.g., \(\forall m\exists n A(m,n)\to \exists f\forall m A(m,f(m))\)). The authors provide a constructive model for this theory -- sheaves over (appropriately constructive) Boolean algebras.
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03C90
zbMATH DE Number: 1443413
zbMATH Keywords: constructive meaning
zbMATH Keywords: intuitionistic choice
zbMATH Keywords: Boolean sheaves
reviewed by: Vladik Kreinovich
MaRDI profile type: Publication
full work available at URL: s001530050003
OpenAlex ID: W2031330107
DOI: 10.1007/S001530050003
description: scientific article; zbMATH DE number 1443413