FOM: intuitionism/constructivity

[Harvey Friedman]

I want to suggest a new thread of discussion on the FOM with regard to
intuitionism.

1. What does the usual Heyting propositional calculus have to do with
intuitionism?
2. What does the usual Heybing predicate calculus have to do with intuitionism?
3. What does the usual Heyting arithmetic have to do with intuitionism?

You can also replace "intuitionism" with "constructivity."

I believe, e.g., that no matter what intuitionism means, within reasonable
limits, that Heyting propositional calculus is complete. But I think that
the results on this can be enormously improved, including some of my own.