Can proofs be arbitrarily long?

Question

Suppose that I have a set of starting logical formulas (axioms) and some inference rules that produce new formulas from old ones. I am curious if there is an upper bound to the number of steps (number of times an inference rules has to be used) in the shortest proof of some decidable statement. Let $L$ be the function mapping formulas to minimal-proof-lengths.

Obviously, there can't be any computable function $g$ that maps each decidable formula $P$ to an upper bound for the minimum number of steps ($L(P) \leq g(P)$), because in that case an algorithm that would attempt to find proofs through brute force and stop when that maximum number of steps is exceeded would make it computable to verify if a statement is decidable, contradicting Godel's incompleteness theorem.

Instead, I am looking for a constant $c$ and a computable function $f$ (mapping all formulas to reals) such that $L(P) \leq cf(P)$ for all decidable $P$.

Edit: $c$ would be uncomputable

Does such a function exist?

Answer 1

No, it does not exist. Consider the halting problem for a Turing machine $T$. Express the statement "$T$ halts" as a formula $P$. If $T$ does halt, this is decidable (by simulating $T$ for a certain number of steps). So look through all possible proofs of at most $c f(P)$ steps. If you don't find a proof that $T$ halts, you can conclude that it does not halt. Thus you will have an algorithm for the halting problem.

Answer 2

First of all, if $c$ is an integer then the function $c\cdot f$ is computable if $f$ is. Moreover, any constant at all is bounded by an integer, so regardless of what $c$ is, there is some computable function $h$ with $cf(x)\le h(x)$ for all $x$. So we might as well forget about $c$. (That is: to get a fast-growing function, you need to do more than just scale a computable function by a constant factor.)

It turns out that broadening the domain doesn't help in this case (although it does sometimes). Suppose such an $f$ existed. Then given a sentence $P$, I'll search for a proof or disproof of $P$ of length $\le f(P)$. If I find one, I've decided $P$; if I don't, then I know that $P$ is undecidable.