Twierdzenie Diaconescu - Diaconescu's theorem

W logice matematycznej , twierdzenia Diaconescu jest , czy twierdzenia Goodman-Myhill , stwierdza, że pełny aksjomat wyboru jest wystarczająca do uzyskania prawa wyłączonego środka lub ograniczonych form IT w konstruktywnej teorii mnogości . Został odkryty w 1975 roku przez Radu Diaconescu, a później przez Goodmana i Myhilla . Już w 1967 roku Errett Bishop przedstawił twierdzenie jako ćwiczenie (Problem 2 na stronie 58 w Podstawach analizy konstruktywnej ).

Dowód

Dla każdej propozycji możemy zbudować zestawy${\ Displaystyle P \,}$

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

i

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

Są to zbiory, używając aksjomatu specyfikacji . W klasycznej teorii mnogości byłoby to równoważne

${\ Displaystyle U = {\ rozpocząć {przypadków} \ {0,1 \} i {\ mbox {if}} P \\\ {0 \} i {\ mbox {if}} \ neg P \ end { przypadki}}}$

i podobnie dla . Jednak bez prawa wyłączonego środka tych równoważności nie da się udowodnić; w rzeczywistości te dwa zbiory nie są nawet skończone w sposób dający się udowodnić (w zwykłym sensie bycia w bijekcji z liczbą naturalną , chociaż byłyby w sensie Dedekinda ). ${\ Displaystyle V \,}$

Zakładając aksjomat wyboru , istnieje funkcja wyboru dla zbioru ; to znaczy funkcja taka, że ${\ Displaystyle \ {U, V \} \,}$${\ displaystyle f \,}$

${\ Displaystyle [f (U) \ w U] \ klin [f (V) \ w V]. \,}$

Z definicji tych dwóch zbiorów oznacza to, że

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

co oznacza ${\ Displaystyle (f (U) \ neq f (V)) \ vee P.}$

Ale ponieważ (zgodnie z aksjomatem ekstensjonalności ), więc tak ${\ Displaystyle P \ do (U = V)}$${\ Displaystyle P \ do (f (U) = f (V)) \,}$

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

Tak więc, ponieważ można to zrobić dla dowolnego zdania, jest to uzupełnieniem dowodu, że aksjomat wyboru implikuje prawo wyłączonego środka. ${\ displaystyle \ neg P \ vee P.}$

Dowód opiera się na zastosowaniu aksjomatu pełnej separacji. W konstruktywnych teoriach zbiorów z tylko orzeczeniem separacyjnym forma P będzie ograniczona tylko do zdań z ograniczonymi kwantyfikatorami, dając jedynie ograniczoną postać prawa wyłączonego środka. Ta ograniczona forma jest nadal konstruktywnie nie do przyjęcia.

W konstruktywnej teorii typów lub w arytmetyce Heytinga rozszerzonej o typy skończone zazwyczaj nie ma żadnego rozdziału - podzbiory typu są traktowane w różny sposób. Formą aksjomatu wyboru jest twierdzenie, ale wykluczony środek nie jest.

Uwagi