Теорема диаконесков - Diaconescus theorem - Wikipedia

В математическая логика, Теорема Диаконеску, или Теорема Гудмана – Майхилла, заявляет, что полный аксиома выбора достаточно, чтобы получить закон исключенного среднего или его ограниченные формы в конструктивная теория множеств. Он был открыт в 1975 году Диаконеску.^[1] а позже Гудманом и Myhill.^[2] Уже в 1967 г. Эрретт Бишоп сформулировал теорему как упражнение (задача 2 на стр. 58 в Основы конструктивного анализа^[3]).

Доказательство

Для любого предложение ${ Displaystyle P ,}$ , мы можем строить наборы

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

и

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

Это наборы, использующие аксиома спецификации. В классической теории множеств это было бы эквивалентно

{ Displaystyle U = { begin {case} {0,1 }, & { mbox {if}} P {0 }, & { mbox {if}} neg P end { случаи}}}

и аналогично для ${ Displaystyle V ,}$ . Однако без закона исключенного третьего эти эквивалентности не могут быть доказаны; на самом деле эти два набора даже не доказуемо конечный (в обычном смысле биекция с натуральное число, хотя они были бы в Дедекинд смысл).

Если предположить аксиома выбора, существует функция выбора для набора ${ Displaystyle {U, V } ,}$ ; то есть функция ${ displaystyle f ,}$ такой, что

{ Displaystyle [е (U) в U] клин [е (V) в V]. ,}

По определению двух множеств это означает, что

{ Displaystyle [(е (U) = 0) vee P] клин [(f (V) = 1) vee P] ,}

,

что подразумевает ${ Displaystyle (е (U) neq f (V)) vee P.}$

Но с тех пор ${ Displaystyle P к (U = V)}$ (посредством аксиома протяженности ), следовательно ${ Displaystyle Р к (е (U) = е (V)) ,}$ , так

{ Displaystyle (е (U) neq f (V)) к neg P.}

Таким образом ${ displaystyle neg P vee P.}$ Поскольку это может быть сделано для любого предложения, это завершает доказательство того, что аксиома выбора подразумевает закон исключенного третьего.

Доказательство основано на использовании аксиомы полной отделимости. В конструктивных теориях множеств только предикативное разделение, форма п будет ограничен предложениями только со связанными кванторами, давая только ограниченную форму закона исключенного третьего. Эта ограниченная форма пока еще не приемлема конструктивно.

В конструктивная теория типов, или в Арифметика Гейтинга расширенный с помощью конечных типов, как правило, нет разделения вообще - подмножества типа обрабатываются по-разному. Форма аксиомы выбора - это теорема, а исключенная середина - нет.

Примечания

^ Р. Дьяконеску, «Аксиома выбора и дополнения», Труды Американского математического общества 51: 176-178 (1975)
^ Н. Д. Гудман и Дж. Майхилл, «Выбор подразумевает исключенное среднее», Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 24: 461 (1978)
^ Э. Бишоп, Основы конструктивного анализа, Макгроу-Хилл (1967)

[1] Р. Дьяконеску, «Аксиома выбора и дополнения», Труды Американского математического общества 51: 176-178 (1975)

[2] Н. Д. Гудман и Дж. Майхилл, «Выбор подразумевает исключенное среднее», Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 24: 461 (1978)

[3] Э. Бишоп, Основы конструктивного анализа, Макгроу-Хилл (1967)

[1]

[2]

[3]