Sign up ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|cite|improve this question
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

1 Answer 1

up vote 3 down vote accepted

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.

The current version of the wikipedia article has some useful information and references.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.