Notice that the argument still works just as well if we could compute some g which had the property that g(n)<f(n) for only finitely many n, so this proves that in fact f must grow faster than any computable function!
Not quite. It is true that f must grow faster than any computable function, but what you’ve shown is just that there’s no computable function growing at least as fast as f. It’s possible for functions to have incomparable growth rates, by taking turns for which is bigger infinitely many times.
In first-order logic (or any other complete logic) we have some guarantee that “every true statement is provable”
Not exactly. Every statement that’s true of every model of the axioms is provable from the axioms. If you have a particular model in mind for your axioms, then there can be statements that are true in that model but not provable from the axioms. The trouble is just that the axioms can’t fully specify the model.
Not quite. It is true that f must grow faster than any computable function, but what you’ve shown is just that there’s no computable function growing at least as fast as f. It’s possible for functions to have incomparable growth rates, by taking turns for which is bigger infinitely many times.
True. I overlooked this for some reason, but it’s not hard to give an argument for why f must grow faster than any computable function, so it’s not a major problem. I’ve edited the post to fix this.
Not exactly. Every statement that’s true of every model of the axioms is provable from the axioms. If you have a particular model in mind for your axioms, then there can be statements that are true in that model but not provable from the axioms. The trouble is just that the axioms can’t fully specify the model.
That isn’t different from what I said. Keep in mind that I tried to keep the post as simple as possible, and if I had to define the concept of model for people to make sense of this statement it wouldn’t fit well with that attitude.
Not quite. It is true that f must grow faster than any computable function, but what you’ve shown is just that there’s no computable function growing at least as fast as f. It’s possible for functions to have incomparable growth rates, by taking turns for which is bigger infinitely many times.
Not exactly. Every statement that’s true of every model of the axioms is provable from the axioms. If you have a particular model in mind for your axioms, then there can be statements that are true in that model but not provable from the axioms. The trouble is just that the axioms can’t fully specify the model.
True. I overlooked this for some reason, but it’s not hard to give an argument for why f must grow faster than any computable function, so it’s not a major problem. I’ve edited the post to fix this.
That isn’t different from what I said. Keep in mind that I tried to keep the post as simple as possible, and if I had to define the concept of model for people to make sense of this statement it wouldn’t fit well with that attitude.