## [Propriété D'Existence](/fr/node/60954) Définition Propriété métathéorique constructive qui affirme que si un système démontre une assertion existentielle ∃x φ(x), alors il existe un terme concret t du langage tel que le système démontre φ(t) ; les preuves d’existence fournissent donc des témoins explicites. ## Principe Principe L’existence constructive requiert un témoin syntaxique : une preuve d’existence doit produire un terme ou une construction t exhibant l’objet prétendu, et non se borner à montrer que la non-existence conduit à une contradiction. ## Démonstration Démonstration Dans une arithmétique constructive ou une théorie des types dépendants, une preuve de ∃x φ(x) est représentée par une paire (t, p) où t est un terme et p est une preuve de φ(t) ; par exemple, une preuve constructive qu’il existe un nombre pair supérieur à 2 fournira un numéral n et une dérivation montrant que 'n est pair et n>2'. ## Mauvaise application Mauvaise application Considérer que les preuves classiques d’existence (qui peuvent s’appuyer sur des principes non constructifs) fournissent des témoins explicites ; ou supposer que la propriété vaut dans tout système formel quelles que soient ses axiomes et règles. ## Conséquence Conséquence La propriété d’existence permet d’extraire le contenu computationnel et des témoins à partir des preuves, soutient la synthèse de programmes à partir de preuves et renforce l’interprétation constructive des théories en garantissant que les assertions existentielles renvoient à des objets concrets du langage de la théorie. ## Inversion Inversion L’échec de la propriété d’existence signifie qu’un système peut prouver ∃x φ(x) sans prouver φ(t) pour aucun terme clos t ; les affirmations d’existence sont alors non constructives et privées de témoin au sein de la théorie. ## Limite Limite S’applique à la prouvabilité dans des systèmes constructifs ou convenablement restreints et dépend de l’adéquation expressive du langage des termes ; elle ne s’étend pas aux théories classiques sauf par des principes produisant des témoins ou des traductions conservatrices. ## Tension sémantique Tension sémantique Tension avec l’existence non constructive obtenue par la logique classique ou par des arguments de compacité : ces preuves non constructives affirment l’existence sans fournir de témoin en terme, ce qui s’oppose directement à la propriété d’existence. ## Synthèse Synthèse La propriété d’existence formalise l’exigence constructive selon laquelle les preuves existentielles soient informatives : si le système prouve une assertion existentielle, il doit identifier, dans le langage du système, un terme qui en est le témoin, permettant l’extraction directe de l’objet revendiqué.