History of Natural Deduction
I have been reading “A Brief History of Natural Deduction” by Francis Jeffry Pelletier (1999) to understand the history of natural deduction better. It outlines four different historically significant systems of natural deduction:
- Jaśkowski’s Tables (1934)
- Jaśkowski’s Indented Lists (1934)
- Suppes Dependency Set (1967)
- Gentzen’s Trees (1934)
These looked like curious inventions and I went looking for the original papers they were introduced in and there were a few surprises along the way.
First up was the Jaśkowski’s paper that kick started this. It is interesting to note here that Jaśkowski discovered these ideas in 1926 and communicated them in 1929 through Lindenbaum. Surprisingly there is no original Polish version of this online! The only available copy seems to be the McCall’s edition of The Polish Logic (1920-1939) from 1967. There were two different models introduced by Jaśkowski in this paper.
Jaśkowski Tabular Model (1934)
The tabular representation seems to be a visual aid to understand his textual indented list representation shown below.
Jaśkowski’s Indented Lists (1934)
Second method of Jaśkowski was to use indented lists for the proof steps.
Suppes Dependency Set (1967)
Suppes introduced a method of using the line numbers of the assumptions which any given line in the proof depended upon. In this method, when an assumption is made, its line number is put in set braces to the left of the line (its dependency set).
Gentzen’s visualization (1934)
Fourth method was introduced by Gentzen. Proofs in the N Calculi (Natural Deduction Calculi) are given in a tree format with sets of formulas appearing as tree nodes. The root of the tree is the formula to be proved and suppositions are the leaves of the tree.
Most of this history is based on reading just Pelletier’s work. But after going a bit further into other papers on this topic, I am starting to see that there might be some hidden gems and peculiar systems that are not featured in the mainstream recollection of the history of natural deduction. For example, the Charles Peirce school might have been upto something as indicated in Irving Anellis’ recollection. I wouldn’t be suprised if I find an even earlier instance of natural deduction somewhere before Jaśkowski and Gentzen.
