"Axiom of Choice in Constructive Set Theory"

Abstract

It was recognized already in the beginning of the 20th century that Axiom of Choice has a somewhat problematic status in Mathematics, because of its excessive "non-constructiveness" even from classical point of view. The situation is even worse in Constructive Set Theory (CZF), where Axiom of Choice implies Restricted Law of Excluded Middle (Diaconescu, 1975), which in turn yields Powerset Axiom and a theory stronger than full 2nd order arithmetic.

However, there are certain forms of the Axiom of Choice, e.g. Axiom of Choice for $\Pi\Sigma$-generated sets, $\Pi\Sigma$-AC, or Dependent Choices Axiom, DC, which are perfectly justified from the constructive point of view. Even more important, they are necessary in order to develop certain parts of Constructive Mathematics.

Starting from Aczel's type-theoretic interpretation, $F |--> |F|$, of Constructive Set Theory, we ask the opposite question: which realizable formulas are actually derivable in CZF? It turns out that in this respect $\Pi\Sigma$-AC plays an important role. The main result is as follows:

Theorem. If $F$ is a set-theoretic formula from a certain class $M$ (which stands for "mathematical" and includes, for example, all closed formulas which can be put into the prenex normal form) and the type $|F|$ is non-empty, then $F$ is derivable in CZF+$\Pi\Sigma$-AC.

This theorem implies disjunction and numerical existence properties for CZF+$\Pi\Sigma$-AC and $F$ from $M$:

Corollary. If $F \lor G$, where both formulas are from $M$, is provable in CZF+$\Pi\Sigma$-AC, then either $F$ or $G$ is provable in that theory, and similarly for $\exists$.

The proof uses knowledge and techniques from each of Constructive Set Theory, Martin-Löf Type Theory and Explicit Mathematics, briefly introduced in the last year series "Spring Lectures in Mathematical Logic": see http://ioc.ee/teated/matlog.html.

This is a joint work with Michael Rathjen.