It’s called Heyting arithmetic, but no, nowhere above do I mean intuitionistic logic when I say constructive. Or I don’t think I do. I recognize Löb’s theorem and am not trying restrict any system’s expressive power to avoid it (i.e. using Dan Willard’s self verifying theories).
Maybe I’ll try to prove some sufficient conditions for a Gödel machine to self modify in a toy universe given this perspective. That should make it more convincing / concrete.
It’s called Heyting arithmetic, but no, nowhere above do I mean intuitionistic logic when I say constructive. Or I don’t think I do. I recognize Löb’s theorem and am not trying restrict any system’s expressive power to avoid it (i.e. using Dan Willard’s self verifying theories).
Maybe I’ll try to prove some sufficient conditions for a Gödel machine to self modify in a toy universe given this perspective. That should make it more convincing / concrete.