Una propiedad metateorética de un sistema deductivo que establece que siempre que el sistema demuestra una disyunción A ∨ B (típicamente una fórmula cerrada), demuestra A o demuestra B de forma individual; es una exigencia común en sistemas constructivos.

Principio

Las pruebas constructivas de una disyunción deben contener la información que selecciona qué disyunto es verdadero: demostrar A ∨ B debe proporcionar efectivamente una prueba de A o una prueba de B en lugar de limitarse a excluir su falsedad conjunta.

Demostración

En la lógica proposicional intuicionista o en ciertas teorías de tipos constructivas, una derivación de A ∨ B proviene de un término de prueba que es la inyección izquierda o derecha en la suma disjunta, de modo que el término testifica qué disyunto es demostrable y el sistema demuestra ese disyunto.

Aplicación incorrecta

Suponer que la propiedad de disyunción vale en sistemas clásicos o para codificaciones metateóricas arbitrarias; o interpretar una disyunción demostrada a nivel meta como demostración inmediata de un disyunto sin testigo constructivo interno.

Consecuencia

Si un sistema posee la propiedad de disyunción, puede extraerse información algorítmica definida de las pruebas disyuntivas, mejorando la extracción de programas y asegurando que las pruebas de alternativas no son meras eliminaciones no constructivas por contradicción.

Inversión

Un sistema que carece de la propiedad de disyunción puede demostrar A ∨ B sin demostrar ni A ni B, normalmente recurriendo a principios no constructivos como el principio del tercero excluido o razonamiento clásico.

Límite

Se refiere a la demostrabilidad en la teoría objeto y a menudo solo para fórmulas cerradas o aritméticas; no afirma que toda disyunción metateórica se eleve a un testigo interno en toda formalización y puede fallar en extensiones que añaden axiomas clásicos.

Tensión semántica

Tensión con la ley del tercero excluido: esa ley permite demostrar A ∨ ¬A sin indicar qué miembro se sostiene, en contraste directo con el contenido constructivo requerido por la propiedad de disyunción.

Síntesis

La propiedad de disyunción expresa la exigencia constructiva de que las pruebas de alternativas sean informativas: si el sistema demuestra A ∨ B, debe demostrar, dentro del sistema, uno de los disyuntos, asegurando que la prueba disyuntiva aporta una selección concreta y no solo una no-contradicción.