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.

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

• However, basic rules are placed in a natural deduction's calculus, those derived are, in fact, derived. It does not seem so simple always make deductions of unit length. (philosophy-index.com/logic/forms/rules.php) – Bento Sep 12 '13 at 12:29
• different books have different basic rules, there is no standard set of basic rules, and you haven't answered my question – Willemien Sep 12 '13 at 16:59
• I am not the question's author.. he is user94284 :-) In my opinion the problem is a bit trivial: if I have a deduction there are two possibilities: there is one shorter, or there is not; and since 1 is the minimum ... Can't you understand the reason for such an interest? Even to me it is not clear – Bento Sep 14 '13 at 12:52
• "Why do you find the minimum number of steps in a deduction an important measure?" Number of steps, like the length of a shortest axiom, comes as fairly easy objective metalogical property (at least if counting comes as fairly easy). "Understandable" and "convincing" concern psychology and may not qualify as metalogical at all. – Doug Spoonwood Oct 1 '13 at 3:06