Choice and well-ordering (Q579255): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Removed claims |
||
Property / author | |||
Property / author: Peter J. Freyd / rank | |||
Property / reviewed by | |||
Property / reviewed by: Grigori Mints / rank | |||
Revision as of 11:34, 15 February 2024
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
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