Can we convert existential sentences into functions?

Question

I am trying to grasp the basic ideas of type theory. I understand that universally quantified propositions can be considered as functions, which maps terms to "proof objects". Hence a proposition $$\forall x \;\varphi(x)$$ can be considered as a function which maps a term $u$ to a "proof object" with type $\varphi(u/x)$. Can we do similar things on existential propositions? For example, we add a global function $\tau$ which maps each "proof object" for an existential proposition $\exists x \;\varphi(x)$ to a term, and another global function $\rho$ which maps terms of the form $u = \tau\left(\exists x \;\varphi(x)\right)$ to "proof objects" of type $\varphi(u/x)$.

Answer 1

Let's use untyped $\lambda$-calculus to define functions and rewrite Andreas Blass's ideas.

Notice that what you call "term" and "proof object" are both $\lambda$-terms and that $\forall x \phi(x)$ is the type of all the $\lambda$-terms (or functions) that map $u$ to a proof of $\phi(u)$.

$\exists x \phi(x)$ is the type of a pair $(u,h)$, which may not be unique, where the $\lambda$-term $h$ has $\phi(u)$ as type ($h$ is a "proof" of $\phi(u)$). This pair is the following $\lambda$-term : $$ \lambda f. f u h $$

We can define $\lambda$-terms $\tau$ and $\rho$ (projection functions) which respectively return $u$ and $h$ from a pair $p$ : $$ \tau := \lambda p. p(\lambda a.\lambda b. a) $$$$ \rho := \lambda p. p(\lambda a.\lambda b. b) $$

We can apply those projection functions to our pair and $\beta$-reduce to verify : $$ \tau (\lambda f. f u h) = (\lambda p. p(\lambda a.\lambda b. a)) (\lambda f. f u h) $$$$ \rightarrow_\beta (\lambda f. f u h) (\lambda a.\lambda b. a) $$$$ \rightarrow_\beta (\lambda a.\lambda b. a) u h $$$$ \rightarrow_\beta u $$

And $$ \rho (\lambda f. f u h) = (\lambda p. p(\lambda a.\lambda b. b)) (\lambda f. f u h) $$$$ \rightarrow_\beta (\lambda f. f u h) (\lambda a.\lambda b. b) $$$$ \rightarrow_\beta (\lambda a.\lambda b. b) u h $$$$ \rightarrow_\beta h $$

So $\tau$ and $\rho$ allow us to retrieve $u$ and the proof of $\phi(u)$ from a proof of $\exists x \phi(x)$.