On: Kurt Gödel and the Mechanization of Mathematics

[cscurmudgeon]

But the thing is you are just trading off computability. Aren't you?

> The theory Ordinals is algorithmically inexhaustible

[ProfHewitt → cscurmudgeon]

Excellent question!

Proof checking in the theory Ordinals is algorithmically checkable although theorems are not computationally enumerable because instances of strongly-typed induction axiom are uncountable.

[cscurmudgeon → ProfHewitt]

Thank you! Can't believe I had a conversation with Prof. Carl Hewitt here! Love the actor calculus btw!

[ProfHewitt → cscurmudgeon]

You are very welcome!

Cheers, Carl