2 ms·
You get this for free in (2). You couldn't "reason about programs" if F were inconsistent, nor would the halting problem make any sense in an inconsistent syste
by dvt 4y ago
You get this for free in (2). You couldn't "reason about programs" if F were inconsistent, nor would the halting problem make any sense in an inconsistent system.
- tybug 4y agoI would argue "reasoning about programs" formally means "can prove P Q R ..." (with appropriate choices for P Q R) and doesn't implicitly carry an assumption of consistency. But, fair enough.
- dvt 4y agoYou make a good point, and on the other hand you're right that "reasoning about programs" is not a term of art, so who knows what it means. Given how Lean is used in the article, I took it as basically being some kind of Turing-complete language (lambda-calculus or some variant or what-not).