Take the 2-minute tour ×
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|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 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 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|improve this answer
    
Thanks, that is one of the clearest wikipedia articles I have ever read. –  goblin Mar 29 at 13:28

Your Answer

 
discard

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.