##  [Propiedad de Disyunción](/es/node/60952) 

 Definición

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

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

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

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

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

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

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 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

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.