After listening to Wildberger's rants – some of which are very educational and some of which are just rants, I keep thinking that his actual problem is that he doesn't seem to believe in the implications of the axiom of the excluded middle. He goes on about infinities and such, but the deeper issue seems to be that he thinks in a constructive, intuitionistic way whereas the majority of mathematics uses classical logi…
Heck, I know professional logicians (mostly model theorists) who have never seen intuitionistic logic, in any context, ever. That said, Norman does know a fair bit about intuitionistic logic and constructive mathematics, and even some type theory. He does not like the underlying philosophy any more than he likes classical mathematics.
> Gentzen style sequent calculus with the only axiom being modus ponens
Sidenote: a calculus where modus ponens is an axiom is definitely not a Gentzen-style sequent calculus.