Cardinal Arithmetic, foundations and constructive math

This is not my area but a question occurred to me that I can not find the answer to. There is a very strong axiom of constructibility which ironically gives us highly non-constructive math (GCH is one of its implications). What would be an equally strong axiom in the opposite direction? And I mean direction in a philosophical sense, so what would be the strongest axiom that constructivists/intuitionists would approve of?

My first idea was to find the largest $\kappa$ such that $2^{\aleph_0} = \aleph_{\kappa}$ is consistent with ZF but this set is unbounded ($\kappa$ can be any finite number) and $2^{\aleph_0} < \aleph_{\omega}$. Which brings up the question, how much fundamental difference are there between CH and $2^{\aleph_0} = \aleph_{118}$ for example?

-
$2^{\aleph_0}$ need not be smaller than $\aleph_\omega$. You may be thinking of the theorem that it cannot be equal to $\aleph_\omega$, but it might well be larger. –  Andreas Blass Nov 4 '12 at 3:47
How does the axiom of constructibility give us non-constructive math? $\:$ –  Ricky Demer Nov 4 '12 at 3:55
Building off of Ricky's comment, I'd argue that in fact the presence of GCH is actually a reasonably constructive consequence of the axiom of constructibility (V=L). The reason that GCH holds assuming V=L is that from V=L we can actually define a precise well-ordering of the reals (in fact, of the entire universe, but that's a separate issue) and show that this well-ordering has order type $\omega_1$. This basically requires us to (1) determine the real number satisfying some first-order property, and (2) iterate that procedure through all the countable ordinals. (cont'd) –  Noah S Nov 4 '12 at 5:47
I'm not sure what you mean by "constructive," since that word can have many different meanings, but certainly this reason for GCH holding (in fact, all of V=L) seems fairly constructive, at least relative to what set theory tends to involve. –  Noah S Nov 4 '12 at 5:50
@Najdorf: Your last comment adds some urgency to Noah's request that you explain your terminology. You have said that a certain countable set of sentences ("the theory itself") is "much bigger" than a certain proper class ("the model for $V=L$ done by Gödel"). You have also applied the word "constructive" to two things of very different types, a theory and a model, which leads me to think you have (at least) two meanings in mind for this word. –  Andreas Blass Nov 4 '12 at 14:42

Cardinal arithmetic is the wrong thing to think about, constructively speaking. Here are some facts about constructive mathematics (when I say "may" that means there is a model validating the fact):

• Cardinals cannot be shown to be linearly ordered.
• The ordinals may form a set.
• A subset of a finite set need not be finite.
• A subset of a countable set need not be countable.
• It is conistent to assume that there is an embedding $\mathbb{R} \to \mathbb{N}$.
• It is consistent to assume that every set is a quotient of a subset of $\mathbb{N}$, for example $\mathcal{P}(\mathcal{P}(\mathbb{N}))$.

So, I think you're going in the wrong direction. Size is simply not measured the same way intuitionistically. "Extra" axioms considered by constructive mathematics can broadly be divided into several groups:

1. Fragments of the law of excluded middle, such as Limited Principle of Omniscience and Markov Principle, which bring us closer to classical mathematics.
2. Choice principles, such as countable choice, dependent choice, function choice, which bring in some amount of the axiom of choice. Another such axiom is Aczel's presentation axiom, which states that every set is covered by one for which choice holds.
3. Continuity principles, such as "every function between complete separable spaces is continuous", which are typically incompatible with the law of excluded middle. Another such axiom is the Fan principle, whose important consequence is that the closed interval is compact .
4. Induction principles, which guarantee existence of sets defined by various induction schemata.
5. Computability principles, stating that "everything is computable" in some form. The best known such principle is the formal Church's thesis.

The induction principles vaguely correspond to large cardinal axioms, and so they are perhaps closest to what you are asking for. A predicative constructivist will worry about existence of powersets, so he is going to consider various other axioms that bring in powersets in a limited form, but let us not get into that.

-
Under what assumptions do the ordinals form a set? –  David Roberts Nov 4 '12 at 7:21
Alright that was helpful but I still have some issues: (1) When you say there are models for your first list of statements, what is the base system of constructive math you are working with? (2) Throughout the whole discussion I am assuming a degree of reasonableness, an axiom stating the fact that a finite set can have non-finite subsets or that we have an embedding $\mathbf{R} \to \mathbf{N}$ are not resonable (3) I might be mistaken but I thought that intuitionists did not like Church's thesis ... –  Najdorf Nov 4 '12 at 11:01
@Najdorf: (1) the base system does not matter so much, it could be higher-order intuitionistic logic (i.e., the internal language of a topos), or some variant of intuitionistic set theory. (2) I agree that having an embedding $\mathbb{R} \to \mathbb{N}$ is unreasonable, but it is unavodiable that a finite set should have non-finite subsets. In fact, the statement "every subset of a singleton is finite" implies excluded middle. –  Andrej Bauer Nov 4 '12 at 14:52
@Najdorf: the same criticism applies to classical mathematics. We are not forming any strange subsets, only ones that classical mathematicians do too. You keep changing the rules of the game every time we tell you something you do not like. It does not work that way, we are not cheating, that is how things are. Lastly, statements like "your subset is different things in the future, it is essentially a random variable" do not mean anything. You have to make them mathematically precise. I was not basing my arguments on a notion of time or randomness. My proof is water tight. –  Andrej Bauer Nov 4 '12 at 23:44
@Najdorf: only you can know whether the thing you call "real subset" can be formalized. I suspect you means something like "decidable subset". That is insufficient to do mathematics. Let me give you an example which should worry you. Let $p : \mathbb{R} \to \mathbb{R}$ be a polynomial. Consider the set of its zeroes $Z = \lbrace x \mid p(x) = 0\rbrace$ and then the intersection $Z \cap \lbrace 0 \rbrace$. It is a subset of $\lbrace 0 \rbrace$. It is unprovable intuitionistically that $Z \cap \lbrace 0 \rbrace$ is finite. So, in your view that set must not be "real". But then what is left? –  Andrej Bauer Nov 5 '12 at 13:49