[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