# Optimal Solution in Natural Deduction

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?

• Oops, earlier posted a really stupid answer while my mind was on other things. Thanks to Arthur Fischer for noting the beginner's error! Off to stand in the dunces corner for a while ... – Peter Smith Sep 11 '13 at 15:53
• @Smith,I saw that you deleted the answer .. by chance, is it the fact that from the very first step, the method does not stop? at first glance (without carefully thinking), it seemed to me right.. I even gave you a +1... – Bento Sep 11 '13 at 18:22

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.

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.

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.