12 ms·

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

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 logic and even accept the axiom of choice. 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?) If you stop thinking of axioms as value judgements and instead as definitions of formal systems (or adopt a more general system that encompasses others, such as Gentzen style sequent calculus with the only axiom being modus ponens), you achieve a piece of mind. But obviously his beef is not only that; he would like other people to admit the value of the thinking he prefers. And I agree with that.

theaeolist 8y ago
While reading his rant I kept thinking it's a pitch for HOTT or Univalent Math. Many of the motivations are similar.
posterboy 8y ago
In what way can kinds of constructive logic play a role in linguistics, in your opinion?
ZoltanAK 8y ago
> 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.

theaeolist 8y ago

While reading his rant I kept thinking it's a pitch for HOTT or Univalent Math. Many of the motivations are similar.

posterboy 8y ago

In what way can kinds of constructive logic play a role in linguistics, in your opinion?

ZoltanAK 8y ago

> 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.