# Intuitionistic logic and explicit existence proofs

I have read that to intuitionistically prove a statement of the form $\exists x.\varphi,$ we have to actually describe such an $x$ as an explicit expression (with free variables from $\varphi$, excepting $x$).

Is this just a fluffy heuristic, or can we actually formalize and prove this claim?

-
I would say that this is just a fluffy heuristic, however, I think you could attempt to prove something like "if there is a proof of $\exists x.\ \varphi$, then there is a way of extracting an explicit expression for $x$ from it". Unfortunately, I have not enough experience to help you with this. – dtldarek Mar 29 '14 at 8:15
There is a precise statement, but I do not remember it. Obviously, there are hypotheses – for instance, if the existence statement you are interested in is an axiom, then you can't possibly get an explicit witness. – Zhen Lin Mar 29 '14 at 11:24

One of the characteristics of many constructive theories is that they have the "term existence property": if a statement $(\exists x)\phi(x)$ is provable, then there is a term $t$ such that $\phi(t)$ is provable. Moreover, usually $t$ can be extracted algorithmically from a formal proof of $(\exists x)\phi(x)$.
The term existence property is exactly a rigorous way to say that, if an existential statement is provable, then it is possible to explicitly describe a witness. Many constructive theories have this property or restricted version of it. The restriction to the case where the $(\exists x)$ quantifies over natural numbers is usually of particular interest.