That’s a nice question, but it seems to be about a different formalism, not the one talking about programs. How do you encode “every Goodstein sequence terminates at 0” as a program?
That’s a nice question, but it seems to be about a different formalism, not the one talking about programs. How do you encode “every Goodstein sequence terminates at 0” as a program?