Diaconescu-Goodman-Myhill theorem

The Diaconescu-Goodman-Myhill Theorem , named after Radu Diaconescu , ND Goodman, and J. Myhill , is a mathematical logic theorem that shows that the excluded third party theorem can be derived from the axiom of choice . R. Diaconescu's original 1975 proof dealt with the situation in Topoi . The version reproduced here goes back to Goodman and Myhill. One therefore speaks of the Goodman-Myhill theorem . However, some authors simply speak of Diaconescu's theorem .

Formulation of the sentence

Against the background of the intuitionistic Zermelo-Fraenkel set theory , the axiom of choice results in the proposition of the excluded third party.

The axiom of choice (usually with AC Engl. Axiom of choice ) designated and the law of the excluded with LEM (Engl. Law of the excluded middle ). This is the short form of Diaconescu-Goodman-Myhill's sentence

${\displaystyle \mathrm {AC} \Rightarrow \mathrm {LEM} }$.

Meaning for intuitionism

In intuitionistic mathematics , an or-statement is only accepted if one has a proof for or a proof for , a justification for without knowing which of the statements is true is rejected. The excluded third party theorem claims that for every statement is true. Intuitionistically it would be the absurdity that one can prove for every statement whether it is true or whether its negation is true. Therefore, in intuitionist logic, one dispenses with the proposition of the excluded third party, but without claiming its falsity, one simply does not use it. ${\displaystyle A\lor B}$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle A\lor B}$ ${\displaystyle A\lor \neg A}$ ${\displaystyle A}$

The Diaconescu-Goodman-Myhill theorem thus shows that the axiom of choice cannot be acceptable to an intuitionist. However, the axiom of choice is rejected quite independently of this proposition, because it asserts the existence of certain functions without being able to demonstrate them.

Proof of the theorem

The brief proof is very interesting intuitionistically and should therefore be discussed briefly.

For any statement, consider the sets defined by the axiom of exclusion ${\displaystyle A}$

${\displaystyle U=\{x\in \{0,1\}\mid (x=0)\lor A\}\subset \{0,1\}}$    and    , ${\displaystyle V=\{x\in \{0,1\}\mid (x=1)\lor A\}\subset \{0,1\}}$

which are inhabited by definition, i.e. have elements. After the pair amount axiom exists and after the axiom of choice, there is a to -defined function with and . According to the definition of quantities and means that ${\displaystyle \{U,V\}}$ ${\displaystyle \{U,V\}}$ ${\displaystyle f}$ ${\displaystyle f(U)\in U}$ ${\displaystyle f(V)\in V}$ ${\displaystyle U}$ ${\displaystyle V}$

${\displaystyle ((f(U)=0)\lor A)\land ((f(V)=1)\lor A)}$    and therefore    ${\displaystyle (f(U)\not =f(V))\lor A}$

So it follows from . This also applies the other way round, because if it is true, then according to the axiom of extensionality and therefore also . So we have ${\displaystyle f(U)=f(V)}$ ${\displaystyle A}$ ${\displaystyle A}$ ${\displaystyle U=\{0,1\}=V}$ ${\displaystyle f(U)=f(V)}$

${\displaystyle f(U)=f(V)\quad \Leftrightarrow \quad A}$.

Is , so also and therefore . This also applies in reverse, because it follows from and and therefore . So is ${\displaystyle f(U)\not =f(V)}$ ${\displaystyle U\not =V}$ ${\displaystyle \neg A}$ ${\displaystyle \neg A}$ ${\displaystyle U=\{0\}}$ ${\displaystyle V=\{1\}}$ ${\displaystyle f(U)=0\not =1=f(V)}$

${\displaystyle f(U)\not =f(V)\quad \Leftrightarrow \quad \neg A}$.

Here and there, even intuitionistically, two natural numbers are either the same or different, one has . From the above equivalences it finally follows . Since the statement was arbitrary, the proposition of the excluded third party is derived from the axiom of choice. ${\displaystyle f(U),f(V)\in \{0,1\}}$ ${\displaystyle (f(U)=f(V))\lor (f(U)\not =f(V))}$ ${\displaystyle A\lor \neg A}$ ${\displaystyle A}$

Notes on Evidence

The definition of the quantities and seems unusual at first glance, as the statement has nothing to do with. However, this does not play a role in the application of the axiom of separation. If we know from somewhere that it is true, then obviously the defining conditions of and are always fulfilled, that is, both sets are equal . Should we know from anywhere that is wrong, then it is evident and . But if we don't know whether or is true, then we don't know whether it consists of one or two elements. ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle A}$ ${\displaystyle x\in \{0,1\}}$ ${\displaystyle A}$ ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle \{0,1\}}$ ${\displaystyle A}$ ${\displaystyle U=\{0\}}$ ${\displaystyle V=\{1\}}$ ${\displaystyle A}$ ${\displaystyle \neg A}$ ${\displaystyle \{U,V\}}$

In set theory one learns that one can find a selection function for finite sets even without a choice axiom. This raises the question of whether we apply the axiom of choice had to, because , and are at last. That is correct in classical logic, but intuitionistically these sets are not finite. Finiteness of a set means that we have a natural number and a proof of the equality of the set . But that is not the case here, because we cannot say whether it is equal to 1, nor can we say whether it is equal to 2. This also applies to and . Therefore, intuitionistically, these quantities are not finite and we had to fall back on the axiom of choice. ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle \{U,V\}}$ ${\displaystyle n}$ ${\displaystyle n=\{0,\ldots ,n-1\}}$ ${\displaystyle U}$ ${\displaystyle U}$ ${\displaystyle V}$ ${\displaystyle \{U,V\}}$

Individual evidence

1. ^ R. Diaconescu: Axiom of choice and complementation , Proc. Amer. Math. Soc. 1975, volume 51, pages 175-178
2. ^ ND Goodman, J. Myhill, “Choice Implies Excluded Middle,” Journal of Mathematical Logic and Fundamentals of Mathematics 1978, Volume 24, page 461
3. ↑ Jörg Neunhäuserer: Introduction to the Philosophy of Mathematics , Springer-Verlag 2019, ISBN 978-3-662-59554-1 , page 102
4. ^ The Diaconescu-Goodman-Myhill theorem in the Proof Wiki
5. ^ The Diaconescu-Goodman-Myhill theorem on nLab