Is there a pair of function $f$ and $g$ (both $\mathbb{N}\rightarrow\mathbb{N}$ and definable in the language of first-order Peano arithmetic) such that asymptotically $f$ dominates $g$, and $f$ has property X, but $g$ does not? Where property X is:
(a) computable EDIT: Based on the comment, (a) is solved: take an definable but undecidable set, then let $f=2$ and $g$ be the characteristic function on the set. But what about... (b) provably total in Peano arithmetic
Thank you.
Yes, (b) also has an affirmative answer: let $f(x)=17$, and $g(x)=1$ if there is no proof of "$0=1$" in $PA$ of length $\le x$, and $g(x)$ is undefined otherwise. Note that $g$ is not only definable, but computable!
Strictly speaking, in order to claim that $g$ is computable I need to be careful about what notion of length I use for proofs. If I measure the length of a proof by the number of steps, this is bad: there are infinitely many axioms in $PA$, so infinitely many possible proofs of a fixed length. But if I measure the length of a proof by the number of symbols used, then of course there are only finitely many proofs of a given length, so indeed $g$ is computable.