Intuición del teorema de Diaconescu

Question

Teorema de Diaconescu demuestra que el axioma de la elección implica la ley del medio excluido.

Aunque puedo seguir la prueba en el artículo de la wikipedia anterior, sólo parece un truco barato, por así decirlo, en lugar de algo profundo.

Específicamente, estoy tratando de pensar en una forma intuitiva de entender el contrapositivo (jaja -- pero esto está bien, porque podemos probar $(p\to q)\to(\neg q \to \neg p)$ sin la ley del medio excluido, pero no la inversa) de la afirmación en el contexto de la teoría de tipos.

En este caso, la ley del medio excluido afirma esencialmente que "todas las proposiciones son o bien vacías o bien el universo" -- por lo que el contrapositivo del teorema de Diaconescu dice "si hay una proposición que no es ni vacía ni el universo, no se puede tener siempre una función de elección".

Esto me parece una ruta prometedora para entender el teorema, pero no puedo terminar mi tren de pensamiento -- ¿las proposiciones "medias" no permiten una función de elección? ¿Tiene eso sentido? ¿Hay otra manera de entender la prueba de forma más intuitiva?

Answer 1

En base a tu terminología y comentarios, parece que tienes una confusión interna versus externa/sintaxis versus semántica.

Sintácticamente, la Ley del Medio Excluido (LEM) es el esquema axiomático $P\lor\neg P$ . Incluso en la teoría de tipos, esto sería algo así como $\Pi P:\mathsf{Prop}.P\lor (P\to\bot)$ .

Externamente, es decir, semánticamente (y en particular para la semántica categórica), LEM significa que los subobjetos son complementado (o, en particular, los subobjetos de $1$ son). Que las proposiciones estén "vacías" o el "universo" suena a terminología semántica. En la teoría de tipos, $\top$ es simplemente el tipo de unidad que tiene exactamente un valor. Llamarlo "el universo" no tiene mucho sentido (y además entra en conflicto con otros usos del término "universo" en la teoría de tipos). Llamando a $\bot$ el "tipo vacío" es bastante razonable, pero llamarlo "vacío" empieza a sugerir demasiado, pero no es del todo descabellado. En el semántica de la lógica de primer orden (de orden simple), la gente suele hablar de que los predicados "verdaderos" (unarios) se interpretan como el "universo (del discurso)" o "dominio" y los predicados "falsos" se interpretan como el conjunto vacío. Esta terminología de "universo" no funciona tan bien ni siquiera para la lógica de primer orden multiordenada y es aún más inadecuada (en este sentido) para el trabajo de teoría de tipos.

Como ejemplo concreto, $\mathbf{Set}\times\mathbf{Set}$ es un Topos booleanos (por lo que LEM se mantiene) que no es dos valores . En particular, tiene cuatro valores de verdad, $\bot=(0,0)$ , $\top=(1,1)$ y también $(1,0)$ y $(0,1)$ . Todas las operaciones se definen por componentes. Se puede mostrar fácilmente $P\lor\neg P$ e incluso $(P=\top)\lor(P=\bot)$ son válidos con respecto a esta semántica. Esta última puede internamente se puede leer como que "toda proposición es o bien $\bot$ o $\top$ ". Externamente si asignamos el valor de verdad $(1,0)$ a $P$ , entonces estamos pidiendo el valor de verdad de $(1,0)=(1,1)$ y $(1,0)=(0,0)$ que tienen los valores de verdad $(1,0)$ y $(0,1)$ respectivamente. Por supuesto, la unión de estos, es decir, la interperación de $\lor$ es $(1,1)$ es decir, el valor de verdad de $\top$ como exige el LEM.

La prueba de Diaconescu (¡que sólo tiene tres páginas!) habla de topos, es decir, de semántica categórica para teorías de conjuntos constructivas. Como es lógico, se centra en los subobjetos complementados.

$\neg\neg(P\lor\neg P)$ se mantiene de forma constructiva. La única manera de internamente decir "una proposición no es vacía ni el universo" en la forma en que usted parece estar usando las palabras es decir algo que es equivalente 1 a $\neg(P\lor\neg P)$ Por ejemplo $\neg(P=\top)\land\neg(P=\bot)$ pero esto es contradictorio en la propia lógica constructiva incluso antes de hablar de LEM o del axioma de elección. Externamente Si se dice "si tenemos un subobjeto que no se complementa, entonces el axioma de elección no se cumple", que es exactamente lo que ocurre en la prueba de Diaconescu. Sin embargo, si se afirma (externamente) que "si $0_1:0\rightarrowtail 1$ y $id_1:1\rightarrowtail 1$ no son los únicos subobjetos de $1$ entonces el axioma de elección no se cumple", entonces esto es simplemente falso. Cualquier topos booleano que no sea de dos valores, como $\mathbf{Set}\times\mathbf{Set}$ sería un contraejemplo.

1 En presencia de extensionalidad proposicional que El teorema de Diaconescu requiere . Aquí hay una prueba formal en Agda que $\neg(P\equiv\top)\land\neg(P\equiv\bot)$ es contradictoria:

data ⊥ : Set where

record ⊤ : Set where constructor tt

record _∧_ {ℓ}(A B : Set ℓ) : Set ℓ where
    constructor _,_
    field
        fst : A
        snd : B

¬ : ∀{ℓ} → Set ℓ → Set ℓ
¬ A = A → ⊥

data _≡_ {ℓ}{A : Set ℓ} (a : A) : A → Set ℓ where
    Refl : a ≡ a

isProp : Set → Set
isProp P = (x y : P) → x ≡ y

isProp-⊤ : isProp ⊤
isProp-⊤ tt tt = Refl

isProp-⊥ : isProp ⊥
isProp-⊥ () y

_↔_ : Set → Set → Set
P ↔ Q = (P → Q) ∧ (Q → P)

postulate propExt : {P Q : Set} → isProp P → isProp Q → (P ↔ Q) → P ≡ Q

thm1 : {P : Set} → isProp P → P → P ≡ ⊤
thm1 prf p = propExt prf isProp-⊤ ((λ _ → tt) , λ _ → p)

thm2 : {P : Set} → P ≡ ⊤ → P
thm2 Refl = tt

thm3 : {P : Set} → isProp P → ¬ P → P ≡ ⊥
thm3 prf ¬p = propExt prf isProp-⊥ (¬p , λ{ () })

thm4 : {P : Set} → P ≡ ⊥ → ¬ P
thm4 Refl p = p

thm5 : {P : Set} → isProp P → ¬ (P ≡ ⊤) ∧ ¬ (P ≡ ⊥) → ⊥
thm5 prf (¬P≡⊤ , ¬P≡⊥) with (λ p → ¬P≡⊤ (thm1 prf p)) | (λ ¬p → ¬P≡⊥ (thm3 prf ¬p))
... | ¬P | ¬¬P = ¬¬P ¬P