# Optimality results for Fitch-style natural deduction proofs

Suppose a student submits a Fitch-style natural deduction proof in propositional or predicate logic. Two natural questions arise (beyond correctness):

1. Is the proof as short as can be?
2. Is the proof as shallow as can be (that is, using as few levels of indentation as possible)?

Answering such questions can be difficult, and intuitive approaches are largely ad hoc, highly dependent on the nature of the particular formula to be proved. Are there results in the literature a grader could find helpful in assessing the quality of the student’s proof? Or is there software available guaranteed to find an “optimal” proof, along one or dimensions of optimality?

NB: I’m not a logician.

• Intuitively this sounds like a problem that is distinctly infeasible -- I'd expect it to be at least NP-hard. Commented Oct 12, 2018 at 17:41
• So, essentially Kolmogorov complexity for proofs? Commented Oct 12, 2018 at 17:42
• One possible heuristic might be to convert the proof to a functional program and then analyze that program the way you'd do a code review, e.g. are there unused or unnecessarily duplicated calculations, or are there simple reductions you can perform on the resulting code which improve the readability. Commented Oct 12, 2018 at 17:48
• @HenningMakholm: Does it help at all if we restrict to propositional logic? I haven't thought too hard about this, clearly. But my intuition says there's at least a remote chance such a restriction could help. Commented Oct 12, 2018 at 18:01
• @symplectomorphic: I'm not sure; all I have is hunches, really. What I immediately had in mind was a reduction from SAT that would indeed depend on having quantifiers. But if I had to guess, my bet would be that the propositional case is probably hard too. Commented Oct 13, 2018 at 2:49

I can sort of answer the second question, and say something about the first.

It would be kind of meaningless to ask for the shallowest proof, for two reasons. Firstly, every FOL tautology can be proven within a fixed number of indentation levels. The exact number may depend on the rules. Here is an example of how to collapse two consecutive ⇒-subcontexts into one:

From:

...
...
If A:
...[1]
If B:
...[2]
C.
B ⇒ C.
...[3]
D.
...
...

To:

If A ∧ ( A∧B ⇒ C ):
If B:
A∧B.
C.
B ⇒ C.
A ∧ ( A∧B ⇒ C ) ⇒ ( B ⇒ C ).
...
...
If A∧B:
...[1]
...[2]
C.
A∧B ⇒ C.
If A:
A ∧ ( A∧B ⇒ C ).
B ⇒ C.
...[3]
D.
...
...

Observe that the "...[2]" has been moved one level outward. This already shows that, for any Fitch-style system for PL that supports the above steps, we need at most 2 indentation levels. For FOL, we can similarly 'factor out' subcontext reasoning, but the minimum needed indentation levels would depend on the exact rules.

However, the whole point of Fitch-style is to support subcontext reasoning naturally, so this is the second reason that it is meaningless to minimize the number of levels!

~ ~ ~

As for shortest proofs, in general it is also quite senseless to ask for the shortest, but it is sensible to say that a good proof ought to be no more than twice the length of the shortest solution than anyone can find.