[philip-b]

I think there's either a mistake or a very very large omission here. It starts here:

>This is looking better! We have an amazing function, is_statement_true, that can tell us whether anything is true or false, given enough time!

>Read it through, and try to prove to yourself that is_collatz_true really does eventually return the truth of the Collatz conjecture.

Namely, I think the author confuses Lean theorems and metatheory theorems, where when I say metatheory, I mean the language and the system we use to talk about lean, about Godel's incompleteness theorem, and everything else - basically, the English-math language in which the chapter is written. Hence, it's wrong to say that is_statement_true can tell us whether any statement is true - it can merely tell us which of the two options it is: the statement is a theorem of Lean or its negation is a theorem of Lean. Same for is_collatz_true - sure, it must tell us what Lean thinks about the Collatz conjecture but doesn't tell us anything about the truth or falsity of the Collatz conjecture.

And finally, in the very end of Chapter 2, this problem arises as well. The chapter says that if Lean is sound and complete, then we can define a function which, for any Turing machine, returns one of two options: Lean thinks it halts, or Lean thinks it doesn't halt. But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.

[auggierose]

He skips connecting it with model theory by choosing statements where it is clear what they mean (collatz conjecture, halting problem). I think that's OK.

[puffoflogic]

It's not clear to me that model theory has much to say about Lean; do you have any resources on this? plato.stanford.edu does hedge that while modern model theory focuses on first-order logic, there's a broader sense of model theory which can be used to study even natural languages. But if you try to study type theory as natural language statements you aren't going to get much out of it. Going about it that way, the models you'll come up with are going to be of the form "doing some formal symbol manipulation X has certain formal symbol results Y" which will be neither illuminating nor useful. I did find an abstract[0] which claims that model theory has historical roots in type theory but I'm doubtful I have any way to access it.

[0] https://www.cambridge.org/core/journals/bulletin-of-symbolic...

[auggierose]

First you have to see that the tutorial uses Lean basically as a blackbox. All that is needed is that you can express proofs in it, that applying lean to proofs yields lean theorems, that proofs are enumerable, and that Lean is powerful enough to express the collatz conjecture and the halting problem. So you can replace Lean by any other such blackbox B, for example B = (first-order logic + ZFC), and the argument in the tutorial goes the same way. Therefore type theory or not is not an issue here.

What IS an issue is that to fully explain what "express the collatz conjecture in B" means, you need model theory. You are right, type theory often doesn't come with model theoretic semantics, but it can be done in a natural way even for type theories.

The paper you are referencing is on sci-hub, by the way: http://sci-hub.wf/10.1017/S1079898600010568

[MatthiasPortzel]

> But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.

Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.

But the halting problem, and the Collatz conjecture, and all mathematical truth, is fundamentally embedded inside of systems of formal logic. Gödel's Incompleteness Theorem doesn't say anything about systems of truth outside of formal mathematical logic. So this result isn't relevant to Physics, for example.

However, Gödel's Theorem, and this proof, don't rely on any particular qualities of the formal system, other than the ability to enumerate proofs (and other things that we think of as inherit to logic). So this proof applies not just to Lean, but also to every method of proving things in math.

[lmm]

> Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.

This is wrong - see Dyson's eternal intelligence.