Dear Darlthus,

The predicate Halt<aType>[anExpression] is true if and only

if anExpression of type aType halts.

The predicate Halt is inferentially undecidable, that is, it

is not the case that for every expression anExpression of type aType that

|- Halt<aType>[anExpression] or |- ~Halt<aType>[anExpression].

Inferential undecidability does not mean that mathematics

is wrong.

Of course, it is possible to have incorrect

mathematical proofs, such as the incorrect proof in

[Gödel 1931] for the inferential undecidability of Russell's

Principia Mathematica. (There is a correct proof here:

https://papers.ssrn.com/abstract=3603021)