Teorema de Diaconescu - Diaconescu's theorem

Na lógica matemática , o teorema de Diaconescu , ou o teorema de Goodman-Myhill , afirma que o axioma completo da escolha é suficiente para derivar a lei do meio excluído , ou formas restritas dele, na teoria dos conjuntos construtivos . Foi descoberto em 1975 por Radu Diaconescu e mais tarde por Goodman e Myhill . Já em 1967, Errett Bishop apresentou o teorema como um exercício (Problema 2 na página 58 em Fundamentos da análise construtiva ).

Prova

Para qualquer proposição , podemos construir os conjuntos

e

Esses são conjuntos, usando o axioma da especificação . Na teoria clássica dos conjuntos, isso seria equivalente a

e da mesma forma para . No entanto, sem a lei do terceiro excluído, essas equivalências não podem ser provadas; na verdade, os dois conjuntos nem mesmo são comprovadamente finitos (no sentido usual de estarem em bijeção com um número natural , embora estivessem no sentido de Dedekind ).

Assumindo o axioma da escolha , existe uma função de escolha para o conjunto ; ou seja, uma função tal que

Pela definição dos dois conjuntos, isso significa que

,

que implica

Mas desde (pelo axioma da extensionalidade ), portanto , então

Assim, como isso poderia ser feito para qualquer proposição, isso completa a prova de que o axioma da escolha implica a lei do terceiro excluído.

A prova se baseia no uso do axioma de separação total. Em teorias de conjuntos construtivas com apenas a separação predicativa , a forma de P será restrita a sentenças apenas com quantificadores ligados, dando apenas uma forma restrita da lei do meio excluído. Esta forma restrita ainda não é aceitável construtivamente.

Na teoria construtiva dos tipos , ou na aritmética de Heyting estendida com tipos finitos, normalmente não há separação alguma - subconjuntos de um tipo recebem tratamentos diferentes. Uma forma do axioma da escolha é um teorema, mas o meio excluído não é.

Notas

  1. ^ R. Diaconescu, "Axiom of choice and complementation" , Proceedings of the American Mathematical Society 51: 176-178 (1975)
  2. ^ ND Goodman e J. Myhill, "Choice Implies Excluded Middle", Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 24: 461 (1978)
  3. ^ E. Bishop, Fundações da análise construtiva , McGraw-Hill (1967)