Can the axiom of choice be explicitly proved in (intuitionistic) predicate logic, or is something like intuitionistic type theory necessary?

In intuitionistic mathematics, an axiom of choice of the form

$$
\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x, fx)

$$

is valid by the meaning of the quantifiers (comp. Dummett, Elements of Intuitionism, 2000).

In intuitionistic type theory, it is possible to actually prove the axiom of choice. For example,

$$
(\lambda z)((\lambda x) p_{left}(z(x)),(\lambda x)p_{right}(z(x)))
$$

is a proof-object for an axiom of choice of the form

$$
(\Pi x:A)(\Sigma y:B)R \rightarrow (\Sigma f :(\Pi x:A)B)(\Pi x:A)R(f(x)/y),
$$
where $p_{left}$ and $p_{right}$ are the projection-functions (comp. Martin-Löf, "Constructive Mathematics and Computer Programming", 1982).

What I am interest in is the precise relationship between predicate logic and type theory. Can the axiom of choice be proved in the former, or is the more expressive language of type theory necessary, which can refer to proof-objects and constructions directly? According to Dummett, in intuitionistic logic, the axiom of choice is true due to the constructivist meaning of the quantifiers. But this does not correspond to a formal proof within the system, but a meta-theoretical result.

Now, my feeling is the following: predicate logic cannot properly represent constructions or proof-objects. But in Martin-Löf's proof of the choice axiom, proof-objects are directly operated on. Therefore, while in intuitionistic predicate logic, the axiom of choice is an axiom properly so-called, i.e. an unprovable principle that we accept due to our informal understanding, it becomes provable in the more expressive system of intuitionistic type theory. Am I correct here, or is this a misunderstanding?

Answer

I think that you're basically correct. The key difference here is the difference in languages. In the very simplest kinds of intuitionistic higher-order predicate logic, we don't have the ability to create new functions "internally to the logic" by using lambda terms.

In slightly more complicated versions, there are term-forming operators that allow for lambda abstraction, but these systems still do not prove the axiom of choice. This is because the system don't see $(\forall x)(\exists y)R(x,y)$ as expressing a function.

In these settings, we can sometimes prove the axiom of choice as a kind of metatheorem, that if $(\forall x)(\exists y)R(x,y)$ is provable then $(\forall x)R(x,tx)$ is provable for some term $t$. This kind of metatheorem gives a precise interpretation of comments like the one by Dummett. It also shows how these systems align with the BHK interpretation of constructive reasoning, although the alignment is only visible in the metatheory.

Intuitionistic type theory is quite different from predicate logic, not only because the quantifiers $\forall$ and $\exists$ are often ignored, and the internal type operations $\Sigma$ and $\Pi$ are studied instead. In this way, type-theoretic systems mix the metatheory and object theory more than predicate logic does. (It takes some work, actually, to avoid inconsistency, which strong type theories are vulnerable to via Curry's paradox and similar issues.)

Systems like Martin-Löf type theory manage to internalize enough of the BHK interpretation to prove analogues of the axiom of choice (again, with quantifiers replaced by type constructors) without internalizing enough to become inconsistent.