Jaśkowski is (as discussed in class) one of the founders of natural deduction, which he described completely independently from Gerhard Gentzen in the 1930s.
Wikipedia says that Gentzen's approach initially became more popular with logicians because it could be used to prove the cut-elimination theorem. But Jaśkowski's is closer to the way that proofs are done in practice.
This doesn't ring true to me (Valeria). I think only later logicians got interested in cut-elimination and that Jaśkowski's natural deduction system, which later came to be known as Fitch-style natural deduction, is easier to typeset and hence more adaptable to textbooks.
But at least least his original paper is available from Wikipedia (On the Rules of Suppositions in Formal Logic Studia Logica 1, 1934 pp. 5–32; reprinted in: Storrs McCall (ed.), Polish logic 1920-1939, Oxford University Press, 1967 pp. 232–258) and young logicians can compare his article with Gentzen's.
Another major controversy in the earlier years of Natural Deduction was the one about the exact rules for the quantifiers in first-order logic. Much ink was spilled on that one too.
For my part I am much more interested in the issue of the trade-offs that one must make to extend Natural Deduction to Modal Logics and to substructural logics. Some incipient discussion can be found in Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic (G. Bellin, V. de Paiva and E. Ritter), In Methods for Modalities 2001, Amsterdam, November 2001. (pdf).
Need to add the reference to Jaśkowski's paper and to von Neumann's discussion to our bibliography. Also need to read these, thanks for the historical insights Luiz Carlos. Here are the slides from the first lecture of the course.
No comments:
Post a Comment