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

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

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

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

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

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

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

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