Estimating meta-mathematical properties of conjectures

Question

Given a formalized system of mathematics (a set of axioms and deduction rules), is it possible to estimate meta-mathematical properties of conjectures in this system such as the number of deduction steps from the axioms before attempting their proof?

Can a mathematical system have itself sufficiently analyzable structure that permits such heuristics?

It seems that, via the Curry–Howard correspondence, the general problem might be NP-complete, and proving the existence of a proof (within limits) would be likely as hard as the halting problem. So heuristics might be limited to very simple formal systems.

I'm asking this for two reasons:

• i'm wondering if mathematical intuition can be formalized
• i'm not aware of such mechanisms in automated theorem provers

tldr:

Given a set of proofs, is it possible to estimate the deduction distance and other properties of yet unproven statements, saving resources during the proof search?

Answer 1

The question of whether $p$ is a theorem of $T$ is equivalent to the halting problem as soon as $T$ is (computably axiomatizable, consistent, and) strong enough to implement "basic arithmetic" - this is basically immediate from part of the proof of Godel's incompleteness theorem (the representability of all computable functions in $T$).

And "implement "basic arithmetic"" is a very weak requirement - Robinson arithmetic, which can't even prove that every number is either even or odd(!), is already enough. Even for "simple" decidable theories like Euclidean geometry or arithmetic with only addition this problem is quite difficult (see here and here respectively).

All of this points to a general negative answer to your question. However, your question is too broadly phrased to have an airtight answer, so there's still an element of subjectivity here. But I would hazard:

For all but the simplest systems and properties, the problem of telling whether a formula has that property with respect to that system is undecidable; and even for very simple systems and properties, this problem is almost always computationally infeasible.

Note that the Curry-Howard correspondence doesn't really play a role here: to get "lower bound" results we just need to embed computational processes in formal systems, and this is pretty easy in many situations.