Choice and well-ordering (Q579255)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Choice and well-ordering
scientific article

    Statements

    Choice and well-ordering (English)
    0 references
    1987
    0 references
    It is proved that a well-ordering of a set S is intuitionistically definable from any choice function for S, finding an element in any non- void subset of S. The proof is presented in topos-theoretic setting. Main leading ideas are Diaconescu's theorem that the axiom of choice implies excluded middle and the classical derivation of well-ordering from choice. The author's guess was that the language of topos theory is necessary to present his proof, since its recasting in the language of intuitionistic set theory needs machines not yet in existence. Meanwhile such recasting was done by \textit{P. Aczel} [Every choice set can be well- ordered: An elementary proof in intuitionistic set theory, 14 typed pages] and the reviewer was told that A. Blass published a similar proof.
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    intuitionistic definability
    0 references
    well-ordering
    0 references
    choice function
    0 references
    axiom of choice
    0 references
    excluded middle
    0 references
    topos theory
    0 references
    intuitionistic set theory
    0 references
    0 references
    0 references
    0 references