Diaconescuova věta - Diaconescu's theorem

V matematické logiky , Diaconescu věty , nebo Goodman-Myhill věty , uvádí, že plná axiom výběru je dostatečná odvodit právo vyloučeného středa , nebo omezených forem tom, v konstruktivní teorie množin . To bylo objeveno v roce 1975 Radu Diaconescu a později Goodman a Myhill . Již v roce 1967 Errett Bishop představil teorém jako cvičení (Problém 2 na straně 58 v Základy konstruktivní analýzy ).

Důkaz

Pro jakýkoli návrh můžeme sestavit sady${\ displaystyle P \,}$

${\ displaystyle U = \ {x \ v \ {0,1 \} :( x = 0) \ vee P \}}$

a

${\ displaystyle V = \ {x \ v \ {0,1 \} :( x = 1) \ vee P \}.}$

Jedná se o množiny využívající axiom specifikace . V klasické teorii množin by to bylo ekvivalentní

${\ displaystyle U = {\ begin {cases} \ {0,1 \}, & {\ mbox {if}} P \\\ {0 \}, & {\ mbox {if}} \ neg P \ end { případy}}}$

a podobně pro . Bez zákona vyloučeného středu však tyto rovnocennosti nelze prokázat; ve skutečnosti tyto dvě množiny nejsou ani prokazatelně konečné (v obvyklém smyslu, že jsou v bijekci s přirozeným číslem , i když by byly v Dedekindově smyslu). ${\ displaystyle V \,}$

Za předpokladu axiomu výběru existuje funkce výběru pro množinu ; to je funkce taková ${\ displaystyle \ {U, V \} \,}$${\ displaystyle f \,}$

${\ displaystyle [f (U) \ v U] \ klín [f (V) \ ve V]. \,}$

Podle definice těchto dvou sad to znamená

${\ displaystyle [(f (U) = 0) \ vee P] \ klín [(f (V) = 1) \ vee P] \,}$ ,

z čehož vyplývá ${\ Displaystyle (f (U) \ neq f (V)) \ vee P.}$

Ale protože ( axiomem extenzivity ), tak ano ${\ displaystyle P \ to (U = V)}$${\ Displaystyle P \ to (f (U) = f (V)) \,}$

${\ Displaystyle (f (U) \ neq f (V)) \ až \ neg P.}$

Tudíž, jak by to bylo možné udělat pro jakýkoli výrok, doplňuje to důkaz, že axiom výběru znamená zákon vyloučeného středu. ${\ displaystyle \ neg P \ vee P.}$

Důkaz se spoléhá na použití úplného separačního axiomu. V konstruktivních teoriích množin pouze s predikativní separací bude forma P omezena pouze na věty s vázanými kvantifikátory, čímž bude dána pouze omezená forma zákona vyloučeného středu. Tato omezená forma stále není konstruktivně přijatelná.

V konstruktivní teorii typů nebo v Heytingově aritmetice rozšířené o konečné typy obvykle nedochází k žádnému oddělení - podmnožinám typu se dává různá zacházení. Forma axiomu volby je věta, ale vyloučený střed není.

Poznámky