Constructivist Interpretation of a Function

Question

Lets suppose I have an exponential function $a^{x}$, and I desire to show that for any number $n$ in $(0, \infty)$, it is possible to find a value of $x_0$ such that $a^{x_0} = n$. The simplest proof would be to construct a function that does exactly that.

Real findLogarithm(Exponential f, PositiveReal n) {
    Real x_0 = new Real();
    /* ... */
    return x_0;
}

According to the lambda calculus, the type signature of this function would be

$\mathrm{findLogarithm} :: \mathrm{Exponential} \rightarrow (\mathrm{PositiveReal} \rightarrow \mathrm{Real})$

However, an equally valid type signature, in the language of first order logic, would be

$\forall x \forall y \exists ! z (P(z))$,

where P(z) is the desired invariant that results from constructing the function. If so, then can we interpret the function construction operator in the Lambda Calculus as a type of predicate in first-order logic? I am trying to find a motivation for why it is that, out of the 16 possible logical connectives, the lambda calculus gives the logical implication a privileged position.

Answer 1

In general, if $\forall x:X\forall y:Y\exists !z:Z P(x,y,z)$ then by the (higher-type) axiom of choice there exists a unique functional $\Phi\colon X\to (Y\to Z)$ such that $\forall x,y P(x,y,\Phi(x,y))$, and vice-versa. So your two formulations are just different ways of saying the same thing.

However, any restrictions you put on $\Phi$ (e.g. computable, primitive recursive) will correspond to a restriction on the $P$ (e.g. quantifier-free, provable in Peano arithmetic). In fact the precise correspondence between the two formulations is an incredibly deep question in proof theory.

As for your second point: The different logical connectives are largely interchangeable. For instance $A\rightarrow B\Leftrightarrow \neg A\lor B$, and so you could write down the axioms of propositional logic without referring explicitly to $\rightarrow$. What you choose depends on style and presentation to a certain extent. The $\lambda$-calculus is a theory of functionals, and so the underlying logic tends to be presented with an emphasis on $\rightarrow$.