> that would require that it be able to derive such a fact from a core understanding of what addition and division mean
Yes, and that's the part that's not possible in general, only for specific cases. For example, you can prove that:
f(P: int -> boolean, x: int) => P(x) ? f(x + 1) : halt
will halt for any x IFF there are an infinite number of integers that have the property P, so f will halt if P is "is an even integer" because there are an infinite number of even integers (which, obviously, you can also prove).
And with that in mind, you might want to go take another look at:
Yes, and that's the part that's not possible in general, only for specific cases. For example, you can prove that:
f(P: int -> boolean, x: int) => P(x) ? f(x + 1) : halt
will halt for any x IFF there are an infinite number of integers that have the property P, so f will halt if P is "is an even integer" because there are an infinite number of even integers (which, obviously, you can also prove).
And with that in mind, you might want to go take another look at:
https://news.ycombinator.com/item?id=17465542