Although PA doesn’t prove that the evaluation of f_α(n) terminates at an integer, it does prove that if the evaluation of f_α(n) terminates, then it terminates at an integer. That’s sufficient to prove that your program doesn’t terminate.

@AndersKaseorg I also just realized that if f_α(n) doesn't terminate, then the whole program doesn't terminate. i.e. the program won't terminate regardless of the totality of f_α(n).

@AndersKaseorg Could you elaborate on how what you mentioned would prove my program doesn't terminate though? I am curious how you verify the "if the evaluation of f_α(n) terminates" part.

It’s nothing complicated. Suppose the evaluation of f_α(n) terminates. Then there’s some finite sequence of intermediate computations f_α₀(n₀), f_α₁(n₁), f_α₂(n₂), …, f_α(n) where each result is a simple integer function of the previous results. By strong induction, each result (including the final one) is an integer.

"Suppose the evaluation of f_α(n) terminates." For all natural n? Or for one particular n?

For one particular α and n.

Then how does that prove f_α(k) terminates for every k > n?

Like I said, it doesn’t.

Stepping back to top level: we wish to prove your program doesn’t terminate. Suppose it does terminate. Then it must have broken out of the loop. It only breaks out of the loop it it finds an n such that the evaluation of f_α(n) does terminate, and the result is a non-integer.

We have shown in PA that this is impossible.

Heyo

Hi!

@AndersKaseorg :P Well unfortunately f_α(n) won't terminate if the result is non-integer.

Anywho, I'll be deleting my answer now.

If you agree that it’s absurd for f_α(n) to terminate with a non-integer result, then you should agree that we’ve reached the desired contradiction in the proof by contradiction.

@AndersKaseorg Btw, you happened to answer this question.

So you might be interested in this question.

Hmm, perhaps the small Veblen notation from my answer could work for that. I’ll try it later. Thanks!

@AndersKaseorg TREE(n) is slightly past the small Veblen ordinal.

If small-veblen-ordinal = φ(1,...,0,0,0), then TREE(n) ≈ φ(ω,...,0,0,0).

Ah, okay, that would take some work then.

:P

Tad bit bigger

One of my slow side projects has been to understand arxiv.org/abs/1610.04633, which claims to go beyond the ordinal for Zermelo set theory.

(Conjecturally.)

Gud day @PyRulez

Hi

Your answer would have worked if the question was "write a program such that PA can't prove that it halts for all inputs" or something like that.

For a single input though, PA can prove that any halting Turing machine halts, so you need instead a non-halting Turing machine that PA can't prove doesn't halt.

Well yeah, ofc

PA can prove TREE(3) is finite, though the proof would be about TREE(3) axioms long.

"write a program such that PA can't prove that it halts for all inputs" would be interesting though

I'd think so