Suppose a student submits a Fitch-style natural deduction proof in propositional or predicate logic. Two natural questions arise (beyond correctness):
- Is the proof as short as can be?
- 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.
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.