Against my better judgement, I would answer your question in the negative.

My motivation is that even rather strong classical theories cannot prove that

"there is no injection from Cantor space (or: the real numbers using your favourite representation) to the natural numbers" (NIN)

The relevant results due to Dag Normann and myself may be found here:

https://arxiv.org/abs/2007.07560

In particular, the above NIN is not provable in Z$_2^\omega$+QF-AC$^{0,1}$, which consists of

1. Kohlenbach's base theory of higher-order RM (RCA$_0^\omega$, which is classical).

2. Functionals S$_k^2$ that decide all $\Pi_k^1$-formulas (for any $k$)

3. countable choice for quantifier-free formulas (QF-AC$^{0,1}$)

As suggested by its notation, the system Z$_2^\omega$ proves the same second-order sentences as Z$_2$, i.e. second-order arithmetic.

Against my better judgement, I would answer your question in the negative.

My motivation is that even rather strong classical theories cannot prove that

"there is no injection from Cantor space (or: the real numbers using your favourite representation, or: Baire space) to the natural numbers" (NIN)

The relevant results due to Dag Normann and myself may be found here:

https://arxiv.org/abs/2007.07560

In particular, the above NIN is not provable in Z$_2^\omega$+QF-AC$^{0,1}$, which consists of

1. Kohlenbach's base theory of higher-order RM (RCA$_0^\omega$, which is classical).

2. Functionals S$_k^2$ that decide all $\Pi_k^1$-formulas (for any $k$)

3. countable choice for quantifier-free formulas (QF-AC$^{0,1}$)

As suggested by its notation, the system Z$_2^\omega$ proves the same second-order sentences as Z$_2$, i.e. second-order arithmetic.

Against my better judgement, I would answer your question in the negative.

My motivation is that even rather strong classical theories cannot prove that

"there is no injection from Cantor space to the natural numbers" (NIN)

The relevant results due to Dag Normann and myself may be found here:

https://arxiv.org/abs/2007.07560

In particular, the above NIN is not provable in Z$_2^\omega$+QF-AC$^{0,1}$, which consists of

1. Kohlenbach's base theory of higher-order RM (RCA$_0^\omega$, which is classical).

2. Functionals S$_k^2$ that decide all $\Pi_k^1$-formulas (for any $k$)

3. countable choice for quantifier-free formulas (QF-AC$^{0,1}$)

As suggested by its notation, the system Z$_2^\omega$ proves the same second-order sentences as Z$_2$, i.e. second-order arithmetic.

Against my better judgement, I would answer your question in the negative.

My motivation is that even rather strong classical theories cannot prove that

"there is no injection from Cantor space (or: the real numbers using your favourite representation) to the natural numbers" (NIN)

The relevant results due to Dag Normann and myself may be found here:

https://arxiv.org/abs/2007.07560

In particular, the above NIN is not provable in Z$_2^\omega$+QF-AC$^{0,1}$, which consists of

1. Kohlenbach's base theory of higher-order RM (RCA$_0^\omega$, which is classical).

2. Functionals S$_k^2$ that decide all $\Pi_k^1$-formulas (for any $k$)

3. countable choice for quantifier-free formulas (QF-AC$^{0,1}$)

As suggested by its notation, the system Z$_2^\omega$ proves the same second-order sentences as Z$_2$, i.e. second-order arithmetic.