Gentzen's Rules for Natural Deduction | Hacker News Reader

Gentzen's Rules for Natural Deduction

blog.plover.com

46 pointsweinzierl19 comments

Open articleView on HN

The paper referenced also defines Gentzen's sequent calculus, an even nicer formulation of logic:

http://www.digizeitschriften.de/download/PPN266833020_0039/P...

And the same volume has his proof of the consistency of arithmetic:

http://www.digizeitschriften.de/download/PPN266833020_0039/P...

A very nice interactive introduction to the sequent calculus is here: http://logitext.mit.edu/tutorial

When I click that link in firefox it starts opening like 20-tabs a second. Chrome works.

I also linked the PDF directly from my blog article, at https://pic.blog.plover.com/math/logic/lk/Gentzen1934.pdf , partly because I found the Digizeitschriften page annoying.

Indeed, 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?

Sorry about that, works OK for me (FF 72.0.2/Ubuntu 19.10).

For comparison, here are the natural deduction rules expressed in modern notation:

https://leanprover.github.io/logic_and_proof/nd_quickref.htm...

The 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.

Very 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-deductio...

Many steps are an implication phi → ..., and the antecedent mimics the context (Γ) of most ND systems.

another three good writing from same blog https://blog.plover.com/math/logic/coherence-spaces.html https://blog.plover.com/math/logic/cut-rule.html https://blog.plover.com/math/IL-contradiction.html

Thanks for your kind words.

A 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

>>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.

Pedanticly, "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.

No. See my reply to Charles upthread.

The word “casualty” has been used since at least the 17th century to mean a person killed by an accident, mishap, or disaster. They do not have to be a soldier or something. For example, try a Google search for “earthquake casualty”.

Sure. But was he a casualty of the war or a casualty of the Soviet and East European retribution against the Nazis, which continued until 1950 or so? The dates are ambiguous, but the profile fits the latter very well.

Cf. https://en.wikipedia.org/wiki/Flight_and_expulsion_of_German...

Yes, 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.

Reply on news.ycombinator.com