Intuitionistic choice and classical logic (Q1976877)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Intuitionistic choice and classical logic
scientific article

    Statements

    Intuitionistic choice and classical logic (English)
    0 references
    0 references
    0 references
    5 November 2000
    0 references
    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.
    0 references
    constructive meaning
    0 references
    intuitionistic choice
    0 references
    Boolean sheaves
    0 references

    Identifiers