What kind of "infinite sets" do constructivists use?

Question

Original question title: "How do constructivists cope with different concepts of infinity?", changed in favor of something less subjective-sounding.

I get that there are reasons for wanting constructive proofs. I have no problem accepting that some people don't accept other kinds of proofs, as in constructivism. What I don't understand however, is how one can firmly believe that Constructivism is "the" choice to go when there are different concepts of infinity which can only be proven as equal with the axiom of choice, which use isn't allowed in constructivism. My reasoning for the subjective version of the question title is that I believe constructivism is tied to some kind of intuition, yet all definitions below seem to intuitively be the same to me.

---

I will now introduce different kinds of infinite sets according to Oliver Deiser's "Einführung in die Mengenlehre" (introduction to set theory) (2nd edition, Springer, 2004). These definition can all be found in chapter 6 "Unendliche Mengen" (infinite sets) (except for "chain" on p.81).

Let $M$ be a set. A chain $C$ of $M$ is a non empty subset of $\mathcal{P}(M)$ such that for all $A,B\in C$ we have $A\subseteq B$ or $B\subseteq A$. $C$ is said to have maximum $B\in C$ if for all $A\in C$ holds $A\subseteq B$.

1. $M$ is said to be Dedekind-infinite if there exists $N\subsetneq M$ and $f:N\to M$ such that $f$ is bijective.
2. $M$ is said to be Dedekind-infinite-1 if there exists $f:A\to A$ such that $f$ is surjective, but not injective.
3. $M$ is said to be Dedekind-infinite-2 if there exists $f:A\to \mathbb N$ such that $f$ is surjective.
4. $M$ is said to be Chain-infinite if there exists a chain $C$ of $M$ with no maximum.
5. $M$ is said to be Tarski-infinite if there exists a $P\subseteq\mathcal{P}(A)$ non empty such that for all $A\in P$ exists a $B\in P$ such that $A\subsetneq B$.
6. $M$ is said to be $\mathbb N$-infinite if there exists no $n\in\mathbb{N}$ and $f:M\to\{0,\ldots,n-1\}$ with $f$ bijective.

Deiser proves that 1.$\Rightarrow$2.$\Rightarrow\ldots\Rightarrow$6. (and 6.$\Rightarrow$5.) can be proven with elementary (constructive) methods, but he needed some kind of choice (non constructive) to show 5.$\Rightarrow$4.$\Rightarrow\ldots\Rightarrow$1. He notes on p.107 that

Um die tatsächliche Notwendigkeit der Auswahlakte zu beweisen, braucht man viel weitergehende Techniken, es könnte ja ein einfacher Beweis übersehen worden sein.

---

To prove the actual necessity of having to use a choice, much more advanced techiques are required, since a simple proof could have been overlooked.

He doesn't explicitly state that this is the case to proof the four cases up, but for this question I'll assume that at least one cannot be done without choice. (Anything else would imply a proof without choice for $|\mathbb N|\leq |A|\iff\forall n\in\mathbb N:|\{0,\ldots,n-1\}|\leq |A|$, which would be interesting in itself.)

---

This begs the question: Is there a "canonical" concept of infinite sets in constructivism or is each concept considered for it's own sake? What kind of "infinite sets" do constructivists use?

Answer 1

There are many kinds of constructivism.

One kind is the non-classical kind, but it seems to me that if a collection is actually well-defined then every possible way to express that it is finite would have a well-defined truth-value as well, philosophically speaking. It may be that different definitions of "finite" are not equivalent, but all the statements involved ought to have classical truth-values if they have well-defined meaning at all.

This does not mean that non-classical logic is pointless. Just for example, intuitionistic logic is tied to programs and modal logic via the BHK interpretation and Kripke frames. But one must not confuse truth with knowledge or constructibility. For example, we know that the halting problem cannot be solved. This is a boolean fact. Yes, there is a computer program that would generate a counter-example (program,input) pair to any given claimed halting oracle, but the mere notion of the halting problem itself requires the (classical) assumption that any program run on an input will either halt or not halt.

Also, from a logic perspective, any reasonable foundational system for logic itself must interpret classical PA (discrete ordered semi-ring axioms plus induction) for even basic syntactic concepts like provability to be meaningful. It is then philosophically justifiable to extend it to ACA, which is nothing more than adding conservative extension plus the full induction schema. It turns out that lots of real analysis can be done within ACA.

One could extend to predicative higher-order arithmetic, by having base sorts $nat$ and $bool$ and a sort $S \to T$ for all functions from $S$ to $T$, for any sorts $S,T$. (Note that a set in ACA can be thought of as a member of $nat \to bool$.) One is permitted to construct an object only if its defining formula quantifies only over $nat$, which is conservative over PA. One also adds the full induction schema (which can be justified meta-logically), which makes it stronger than PA. It suffices for practically all concrete mathematics (though of course it is incomplete).

Within ACA, it is easy to define a set $S$ to be infinite (7) iff $∀x{∈}S\ ∃y{∈}S\ ( \ y>x \ )$. Note that all your six definitions except for Tarski-infinite can be expressed in ACA via appropriate coding. To express Tarski-infinite you need to have at least (predicative) higher-order arithmetic. Side remark: Your definition (4) should say "non-empty chain".

It turns out that when restricted to the language of ACA, all 5 expressible definitions are equivalent, because every set in ACA is a subset of $nat$ and we have well-ordering of $nat$, which eliminates the need for any choice. $ \def\pow{\mathcal{P}} $

We can sort of express Tarski-infinite in ACA in terms of existence of a sequence of sets instead of a set of sets, namely that for each $S⊆nat$ we say that $S$ is Tarski-infinite iff $∃f{∈}nat{→}\pow(S)$ $∀k{∈}nat$ $( \ f(k) \subsetneq f(k+1) \ )$. Note that members of $nat{→}\pow(S) ≅ nat{→}(nat{→}bool)$ can be easily encoded in ACA via currying. This version of Tarski-infinite is equivalent to the others as well.

It is when you want to talk about sets beyond second-order that things get interesting. From the viewpoint of ZFC, higher-order arithmetic has a model with full powersets, and uncountable sets can be very strange. We do not have a well-ordering of the set of subsets of naturals, unless we have some kind of choice axiom.

Choice can be justified easily if the intended model is countable, because then it could be interpreted as using the well-ordering of the intended model. This is why choice is often considered acceptable in constructive type theories (but not intuitionistic type theories). But if the intended model is not countable, such as with ZFC, then it is more difficult to justify choice, unless one literally believes in the platonic existence of full powersets, in which case 'obviously' choice holds.

---

In general, it is true that many mathematical concepts split into multiple variants in constructive foundations. Well-ordering is another one, where the definition ( no strictly decreasing sequence ) is equivalent to ( every non-empty subset has a minimum ) in general only in the presence of a weak form of choice. But it should not be surprising that we do not need choice to prove equivalence for countable well-orderings.

Answer 2

The question is a little vague because the term "constructivism" is not defined properly, and indeed there are several varieties of this. In constructivism according to Errett, the answer to your query is probably simpler than you think: you most likely won't find an occurrence of anything like "$\mathcal P(M)$" here. The only "completed" infinity that's allowed is $\mathbb N$, and real analysis is developed mainly using $\mathbb N$ (you will agree that you don't need more than that to define a sequence). Of course real numbers occur here but not so much the collection thereof.

So the issue of comparing different infinities does not really arise, since none are considered, though there is a constructive version of Cantor's diagonalisation argument.