These are the answers by logician Russell O'Connor to the ten questions about intuitionism:
Yes.
Yes.
Here I am taking “does not hold” to mean “one cannot prove” rather than “is not true”.
No.
I understand that we can prove ℕ, ℕ ⇒ ℕ, (ℕ ⇒ ℕ)⇒ ℕ, … all have different cardinalities, even if the representitives of these types are all memebers of the countable set of some formal language.
Mu.
I don’t know the answer to this. The statement would be, “does ℕ ⇒ ℕ have the same cardinality as the least uncountable ordinal”. I’m not sure if least uncountable ordinal is meaningful. If it is meaningful, then it has a definite truth value.
Yes.
I taking inaccessible cardinal to mean inaccessible ordinal. I’m not certain about my answer here, but I am (more or less) in favour of large ordinals that give us lots of induction to prove functions terminate. Bigger ordinals are better, even if they are impractical, so long as they are actually well founded.
No
For any given mathematical statement is may not be easy to build a machine such that if the mathematical statement is true then the yes light lights up. For any given mathematical statement if the statement is true it is easy to build a machine such that if the yes light lights up.
No.
Yes.
In general theorems are what give insights, and proofs give no insights. But sometimes proofs give insights, and even more rarely constructive proofs give more insight than classical proofs.
No.
I cannot think of any situation where construtive mathematics is not the most appropriate to be using; however I am open to the possibility that there are some.
No.
All truths are equally true.