10 ms·
Gentzen's Rules for Natural Deduction
- user2994cb 7y agoThe paper referenced also defines Gentzen's sequent calculus, an even nicer formulation of logic: http://www.digizeitschriften.de/download/PPN266833020_0039/PPN266833020_0039___log32.pdf#page=18 http://www.digizeitschriften.de/download/PPN266833020_0039/P...
- user2994cb 7y agoAnd the same volume has his proof of the consistency of arithmetic: http://www.digizeitschriften.de/download/PPN266833020_0039/PPN266833020_0039___log42.pdf http://www.digizeitschriften.de/download/PPN266833020_0039/P...
- laxd 7y agoWhen I click that link in firefox it starts opening like 20-tabs a second. Chrome works.
- user2994cb 7y agoSorry about that, works OK for me (FF 72.0.2/Ubuntu 19.10).
- mjd 7y agoI also linked the PDF directly from my blog article, at https://pic.blog.plover.com/math/logic/lk/Gentzen1934.pdf https://pic.blog.plover.com/math/logic/lk/Gentzen1934.pdf , partly because I found the Digizeitschriften page annoying.
- user2994cb 7y agoIndeed, though that's to the entire volume - I was trying to link directly to the individual Gentzen papers (though by the fairly slow download maybe they are being created dynamically). Thanks for the interesting blog piece though - maybe you could write one about Gentzen's consistency proof?
- asdfafsadfasdf 7y agoA very nice interactive introduction to the sequent calculus is here: http://logitext.mit.edu/tutorial http://logitext.mit.edu/tutorial
- hamad 7y agoanother three good writing from same blog https://blog.plover.com/math/logic/coherence-spaces.html https://blog.plover.com/math/logic/coherence-spaces.html https://blog.plover.com/math/logic/cut-rule.html https://blog.plover.com/math/logic/cut-rule.html https://blog.plover.com/math/IL-contradiction.html https://blog.plover.com/math/IL-contradiction.html
- mjd 7y agoThanks for your kind words.
- RossBencina 7y agoFor comparison, here are the natural deduction rules expressed in modern notation: https://leanprover.github.io/logic_and_proof/nd_quickref.html https://leanprover.github.io/logic_and_proof/nd_quickref.htm...
- chalst 7y agoThe most significant difference between Gentzen's original calculus and the way it is most often given today is that discharge of assumptions are associated with labels in modern calculus, so each discharged assumption is tied to a rule, whereas in Gentzen's calculus, all instances of that proposition are discharged. The innovation is essential to the Curry-Howard correspondence, because this labelling of assumptions matches variable bindings in typed lambda calculus.
- chalst 7y agoA quibble: > Gentzen died at age 35, a casualty of the World War. makes it sound as if GG was a soldier or something. In fact, he was an academic and Nazi party member who worked in Czechoslovakia during the occupation. Wikipedia describes his death so: > Gentzen was arrested during the citizens uprising against the occupying German forces on May 5, 1945. He, along with the rest of the staff of the German University in Prague was subsequently handed over to Soviet forces. Because of his past association with the SA, NSDAP and NSD Dozentenbund, Gentzen was detained in a prison camp, where he died of starvation on August 4, 1945. https://en.wikipedia.org/wiki/Gerhard_Gentzen https://en.wikipedia.org/wiki/Gerhard_Gentzen
- jhfdbkofdcho 7y agoYes, I looked that up too and was similarly uh bummed. But I don’t blame the author. I don’t think he sugar coated it.
- trhway 7y ago>>a casualty of the World War. >makes it sound as if GG was a soldier or something as we're in thread on logic, it worth noting that your statement is logically incorrect. Given that the most casualties of the WWII were civilians, saying that somebody was a casualty of that war means that most probably the person wasn't a soldier or something.
- a1369209993 7y agoPedanticly, "casualty" does actually mean specifically soldiers (or other military personel). Civilian deaths are called "murders" (or "executions"/"resisting capture"/not-at-all if your side is doing it). The term "civilian casualties" is a euphemism that was made up (IIRC during WWII) to obscure/excuse bombing of civilian targets (especially factories). In practice, the euphemism has largely won, though.
- mjd 7y agoNo. See my reply to Charles upthread.
- dwheeler 7y agoVery fun. It turns out that it is easy to implement a natural deduction system using a system based on Hilbert's approach. A discussion on this for metamath's set.mm is here: http://us.metamath.org/mpeuni/mmnatded.html#natural-deduction-metamath http://us.metamath.org/mpeuni/mmnatded.html#natural-deductio... Many steps are an implication phi → ..., and the antecedent mimics the context (Γ) of most ND systems.