> 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. [...] I wonder why he never talks about this – surely as a mathematician he should be aware of intuitionistic logic? (Or is it that as a computer science and linguistics wannabe, I am aware of it but many mathematicians aren't bothered to take a look?)
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.
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.