Теорема Диаконеску - Diaconescu's theorem

В математической логике , теоремах Diaconescu в , или теореме Гудман-Майхилле , утверждает , что полная аксиома выбора достаточно вывести закон исключенного третьего , или ограниченных его форм, в конструктивной теории множеств . Он был открыт в 1975 году Раду Диаконеску, а затем Гудманом и Майхиллом . Уже в 1967 году Эрретт Бишоп сформулировал теорему как упражнение (проблема 2 на стр. 58 в « Основах конструктивного анализа» ).

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

Для любого предложения мы можем построить множества${\ 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.}$

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

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

Заметки