A few comments imply that this introduces the question of P ?= NP, and while it indeed is defining a complexity problem, this is about satisfiability of first order predicates logic, that is formulas with sets and quantifiers, while SAT is about propositional logic.

First order logic was famously proved incomputable by Godel himself, so here he's asking whether we can bound the number of steps given the size of the proof, not the size of the input (formula length), which is the way complexity is usually defined.

In practice, he's saying that tractable theorems must have reasonably sized proofs (to be understood by a human), and there might be an algorithm that is efficient enough in finding short proofs.