##  [Propriété de la Disjonction](/fr/node/60952) 

 Définition

Propriété métathéorique d’un système déductif affirmant que chaque fois que le système démontre une disjonction A ∨ B (généralement une formule close), il démontre A ou il démontre B séparément ; exigence fréquente des systèmes constructifs.

 

 

 

 

 

 





## Principe

Principe

Une preuve constructive d’une disjonction doit contenir l’information indiquant quel disjunct est vrai : prouver A ∨ B doit fournir effectivement une preuve de A ou une preuve de B plutôt que d’écarter simplement leur fausseté conjointe.

 

 

 

 

 





## Démonstration

Démonstration

En logique propositionnelle intuitionniste ou dans certaines théories de types constructives, une dérivation de A ∨ B provient d’un terme de preuve qui est soit l’injection gauche soit l’injection droite dans la somme disjointe, de sorte que le terme atteste quel disjunct est prouvable et le système prouve donc ce disjunct.

 

 

 

 

## Mauvaise application

Mauvaise application

Supposer que la propriété de disjonction vaut en logique classique ou pour n’importe quel encodage métathéorique ; ou interpréter une disjonction dérivée au niveau méta comme la preuve immédiate d’un disjunct sans témoin constructif interne.

 

 

 

 

 





## Conséquence

Conséquence

Si un système possède la propriété de disjonction, on peut extraire une information algorithmique précise des preuves disjonctives, améliorer l’extraction de programmes et garantir que les preuves d’alternatives ne sont pas de simples éliminations non constructives par contradiction.

 

 

 

 

## Inversion

Inversion

Un système sans propriété de disjonction peut démontrer A ∨ B sans prouver ni A ni B, typiquement en recourant à des principes non constructifs tels que le tiers exclu ou le raisonnement classique.

 

 

 

 

 





## Limite

Limite

Concerne la provabilité dans la théorie objet et souvent seulement les formules closes ou arithmétiques ; elle n’affirme pas que toute disjonction méta se relève en un témoin interne dans toute formalisation et peut échouer dans des extensions ajoutant des axiomes classiques.

 

 

 

 

 





## Tension sémantique

Tension sémantique

Tension avec le principe du tiers exclu : ce principe permet de prouver A ∨ ¬A sans fournir quel membre tient, en contradiction directe avec le contenu constructif exigé par la propriété de disjonction.

 

 

 

 

 





## Synthèse

Synthèse

La propriété de disjonction traduit l’exigence constructive que les preuves d’alternatives soient informatives : si le système prouve A ∨ B, il doit prouver, à l’intérieur du système, l’un des disjuncts, garantissant que la preuve disjonctive porte une sélection concrète plutôt qu’une simple non-contradiction.