Diaconescu teoremi - Diaconescu's theorem

Gelen matematiksel mantık , Diaconescu teoremi veya Goodman-Myhill teoremi , tam devletler bu seçim aksiyomu türetmek için yeterlidir dışlanmış orta kanunu veya bunun kısıtlı formları, yapıcı küme teorisinin . 1975'te Radu Diaconescu ve daha sonra Goodman ve Myhill tarafından keşfedildi . Daha 1967'de, Errett Bishop teoremi bir egzersiz olarak ortaya koydu (Yapıcı analizin temelleri , 58. sayfadaki Problem 2 ).

Kanıt

Herhangi için önermenin , biz olabilir kümeleri oluşturmak${\ displaystyle P \,}$

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

ve

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

Bunlar, belirtim aksiyomunu kullanan kümelerdir . Klasik küme teorisinde bu, şuna eşdeğer olacaktır:

${\ displaystyle U = {\ begin {case} \ {0,1 \}, & {\ mbox {if}} P \\\ {0 \} ve {\ mbox {if}} \ neg P \ end { vakalar}}}$

ve benzer şekilde için . Bununla birlikte, dışlanan orta yasası olmadan, bu eşdeğerlikler kanıtlanamaz; gerçekte iki küme kanıtlanabilir şekilde sonlu bile değildir (her zamanki anlamıyla, doğal bir sayı ile eşleşme içinde olsalar da, Dedekind anlamında olacaklardır ). ${\ displaystyle V \,}$

Seçim aksiyomunu varsayarsak, küme için bir seçim fonksiyonu vardır ; yani bir işlev öyle ki ${\ displaystyle \ {U, V \} \,}$${\ displaystyle f \,}$

${\ displaystyle [f (U) \ U] \ kama [f (V) \ V]. \,}$

İki kümenin tanımına göre, bu şu anlama gelir:

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

Hangi ima ${\ displaystyle (f (U) \ neq f (V)) \ vee P.}$

Ancak ( genişlemenin aksiyomuna göre ), bu nedenle , ${\ displaystyle P \ ila (U = V)}$${\ Displaystyle P \ - (f (U) = f (V)) \,}$

${\ displaystyle (f (U) \ neq f (V)) \ ile \ neg P.}$

Böylece , bu herhangi bir önerme için yapılabileceğinden, bu, seçim aksiyomunun dışlanmış orta yasayı ima ettiğinin kanıtını tamamlar. ${\ displaystyle \ neg P \ vee P.}$

Kanıt, tam ayırma aksiyomunun kullanımına dayanır. Yapıcı küme teorilerinde, yalnızca öngörüsel ayrıma sahip , P'nin biçimi, yalnızca sınırlı nicelik belirteçleri olan cümlelerle sınırlandırılır ve dışlanmış orta yasanın yalnızca sınırlı bir biçimini verir. Bu sınırlı biçim, yapıcı olarak hala kabul edilebilir değildir.

Gelen yapıcı tip teori , veya Heyting aritmetik bir tür bütün-alt-gruplar farklı tedaviler verilmiştir sonlu tipleri ile uzatılmış bir ayırma tipik olarak mevcuttur. Seçim aksiyomunun bir biçimi bir teoremdir, ancak dışarıda bırakılan orta değildir.

Notlar