Resource Metalogic: Proving that a theorem can (not) be deduced from given axioms in a certain number of steps

Question

One of the reasons automated theorem proving systems haven't caught up with humans yet might be that they have no intuition about resource exploration vs exploitation and other evolved heuristics, due to our physical limitations.

Certain programming languages restrict programs to non-turing complete and provably finite execution semantics, which allows one to reason about the number of steps/instructions it uses in the worst case. Even in systems which are not provably finite in all cases, some programs can still be proven to halt.

Via the Curry-Howard-Correspondence, the same possibilities and limitations seem to exist with proofs. So is it possible to create non-exhaustive proofs about resource requirements of mathematical proofs?

E.g. "Fermat's last theorem can not be proved in less than 1 million deduction steps from the ZFC axioms and inference rules"

Answer 1

Sure it is. Run a theorem prover, starting from ZFC axioms and inference rules, and produce all proofs having no more than 1 million steps. Sift through the output to see if Fermat's Last Theorem ever came up as one of the steps proved. If so, it was proved. If not, it was not proved.

Answer 2

Unless you have a proof system that generates most general proofs, you need not only to limit the proof length, but also the size of invented formulas and terms. For example already modus ponens invents a formula A in backward chaining:

   A       A  ->  B
 -------------------- (Modus Ponens)
          B

If you don't have a proof system that generates most general proofs, each axiom schema needs to be instantiated with a formula free of meta variables. If you don't limit this size as well, then you have infinitely many proofs with 1 million steps, and you

cannot decide whether FLT is among them. Most general proofs are not possible if higher order unification is involved, the unification itself might generate infinitely many solutions. Didn't have demonstrations available, until I read about Goldfarb numbers:

Example:

F(f(a,b)) = f(F(a),b) ?

F ↦ λx. f(...f(x,b),...b)