Suppose it is possible to test whether a statement is an axiom in our theory (this is true for finite sets of axioms, or computable infinite sets, i.e. pretty m

Suppose it is possible to test whether a statement is an axiom in our theory (this is true for finite sets of axioms, or computable infinite sets, i.e. pretty much all sets of axioms used in reality). Suppose there is a finite number of derivation rules (probably will work for computable set of derivation rules). Then it is possible to check whether a statement is derived from axioms in one step, i.e. the set of such statements is computable. By the same reasoning, the set of statements that are derivable in two steps is also computable. And so on. Thus the problem of whether the statement is derivable in less than M steps (if M steps is the shortest known proof) is decidable.