Propriété D'Existence

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.