Optimal Solution in Natural Deduction

Question

Does there exist an optimal solution for derivations in natural deduction, which is to say that the derivation in question requires the least amount of steps to arrive at the desired conclusion?

Answer 1

Certainly exists: given a theorem of calculus, we have a set of integers representing the length of the possible deductions and therefore a property of natural numbers always admits a minimum.

Answer 2

You used a philosophy tag :) :) :)

Why do you find the minimum number of steps in a deduction an important measure?
Is it not much more important to have understandable and convincing deductions?

But if you only bother about number of steps, use a derrived rules:
First make a specialised derrived rule that goes directly from the premisses to conclusion.
Then using that rule do it all in one step and you are done, less steps aren't possible.

If you are not allowe to introduce your own derrived rules :
use the TF (Quinne TruthFunctional)
or the FO-Con (Barwise LPL first order Concequence) rule.

But first answer the question:
Why do you find the minimum number of steps in a deduction an important measure?

Answer 3

Yes. The natural numbers form a chain. In other words, for all natural numbers x and y, if x does not equal y, then either

 x<y or y<x.

The number of steps can get measured by a natural number, and consequently, every natural deduction derivation can get done in a minimal number of steps.

However, there does not exist a unique deduction of shortest length in many, if not "almost all", cases. For instance, a derivation of length 4 of Kpq $\vdash$ Kqp is not unique.

Derivation 1:

assumption     1 Kpq
1 K-out left   2 p
1 K-out right  3 q
3, 2 K-in      4 Kqp

Derivation 2:

 assumption     1 Kpq
 1 K-out right  2 q
 1 K-out left   3 p
 2, 3 K-in      4 Kqp

So, although an optimal length of a derivation under some set of rules and/or axioms does exist, such a solution is not an optima in the same sense as a global optima of calculus which by nature qualifies as unique.