# 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?

• I'm not competent to give an actual answer, but it feels relevant to point out that this doesn't mean that you can argue that the usual set-theoretic axiom of choice follows from first-order ZF simply by using intuitionistic (higher-order) logic. At best what you would get is a choice function as a higher-order object, but reifying that as an individual "set" at the base level is a different and stronger demand. Oct 23, 2018 at 11:07

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.)