Initial considerations: using natural deduction as a logical system, we're limited to propositional logic, and we have a fixed set of basic rules of inference. Suppose that we cannot use any theorems of logic right away and if we want to use one we have to insert a proof of it in our argument.
Then we construct a proof of an arbitrary statement this way. My question is the following, is there a way to find out whether our proof is the shortest that can be constructed in a given logical system. The shortest means the one with the least number of steps, where every step corresponds to the one of basic rules or premise introduction.
Let $N$ be the number of steps of the proof of your statement. Now look at the set of all proofs of length $< N$. This is a finite set of proofs. One can program a computer to enumerate all the proofs of lengths between $1$ and $N-1$, to list out the statements that each of them prove, and then to search through that list to see whether your statement occurs. Whatever the outcome of this search, you will have determined one way or another whether a shorter proof of your statement exists.