How to find the shortest proof of a provable theorem?

Roughly speaking, there are some fundamental theorems in mathematics which have several proofs (e.g. Fundamental Theorem of Algebra), some short and some long. It is always an interesting question whether there is a shorter proof for this theorem or not? Surely there is a unique natural number which represents the length of the shortest possible proof of this provable theorem which certainly exists. But how to calculate this natural number? How to find a proof of this length for our theorem?

Of course these questions depends on the logical context which you choose so let me to be more precise:

Question 1: Consider the first order logic and pick a particular language $\mathcal{L}$ and an $\mathcal{L}$-theory $T$ together with a fixed $\mathcal{L}$-sentence $\sigma$ which we know is provable from $T$. Is there any algorithm to calculate the length of least possible proof for $\sigma$? Is there any algorithm to find a proof of the least length for $\sigma$?

Question 2: Is there any non-trivial theorem of ZFC (e.g. Cantor's Theorem: $2^{\aleph_0}>\aleph_0$) which the length of its shortest formal proof is known or at least we have some non-trivial bounds for the size of its shortest proof?

Solution 1:

Start will all one-character strings. Check for each "Is this a proof of my theorem?" Then check the two character strings. Are any of these proofs of my theorem? Repeat for each length $n$ until you find a proof of your theorem.

The question, "Is this string a proof of my theorem?" is decidable, so you are done.

Solution 2:

The notion of "length" matters here. If you mean "length in bits" then the answer is yes, as Thomas Andrews explained.

If you mean "length in steps of the proof", the answer is no. It is easy to come up with an r.e. theory with a set of formulas $A = \{A_n : n \in \mathbb{N}\}$, each of which is provable in three steps (i.e. two axioms and one application of modus ponens), so that if $B$ is the subset of $A$ consisting of formulas that are provable in one step (e.g. are axioms of the theory) then $B$ computes a solution to the halting problem. So, for this theory, you cannot effectively decide how many steps it takes to prove a formula.

It may seems as if we are leveraging the fact that the axioms can be r.e. but not computable. Actually, the undecidability of the axioms is not needed. The same thing can happen even if the set of axioms is decidable.

Let $f\colon \mathbb{N} \to \mathbb{N}$ be a computable function. We work in propositional logic alone; let our language have propositional variables $X_n$, $Z_n$, and $A_n$ for all $n \in \mathbb{N}$. Take as axioms:

1. For each $n$: $X_n$ and $X_n \to Z_n$ are axioms
2. If $f(m) = n$ then $A_m \land Z_n$ is an axiom.

Note that each $Z_n$ is provable in $3$ steps:

• $X_n$ (axiom)
• $X_n \to Z_n$ (axiom)
• $Z_n$ (modus ponens)

But, if $n$ is in the range of $f$, then $Z_n$ is provable in $2$ steps. Say $f(m) = n$.

• $A_m \land Z_n$ (axiom)
• $Z_n$ (conjunction elimination)

If $n$ is not in the range of $f$ then $Z_n$ is not provable in $2$ steps. So $$B = \{ n : Z_n \text{ is provable in 2 steps}\}$$ is exactly the range of $f$. For some computable functions $f$, the range is a Turing-complete set (e.g., let $f$ just enumerate a Turing-complete r.e. set). This means that $B$ is not computable in general, even when $T$ has a computable set of axioms.