Re:Roger Penrose – Is Mathematics Invented or Discovered? [v...
by analbumcover on Friday April 17, 2020 @09:43AM
(#22898900)
It's the other way around, classical logic is a restriction of intuitionistic logic that arises when you affirm the Law of Excluded Middle.
[ Parent
| on HN ]
Re:Roger Penrose – Is Mathematics Invented or Discovered? [v...
by ironSkillet on Friday April 17, 2020 @10:06AM
(#22899052)
I think you're both right in a certain sense. The set of provable statements in intuitionist logic is a subset of what is provable in classical logic, which is what I believe the parent was referring to.
Re:Roger Penrose – Is Mathematics Invented or Discovered? [v...
by analbumcover on Friday April 17, 2020 @11:14AM
(#22899713)
You're certainly right that any constructively provable statement is classically provable, that follows from intuitionism/constructivism generalizing classical logic. But I don't see how we could interpret the following to mean that.
> you can do intuitionist mathematics in classical mathematics