4 ms·
> But the same reasoning can be applied to any formal system F, with fairly minimal assumptions: Strictly speaking, F has to be satisfiable/consistent as well.
by tybug 4y ago
> But the same reasoning can be applied to any formal system F, with fairly minimal assumptions:
Strictly speaking, F has to be satisfiable/consistent as well. {P, ~P} is a trivially recursively enumerable, complete theory which contains Q.
- dvt 4y agoYou 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).