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?
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.
> 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.
>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.
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.
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:
19 comments
[ 0.35 ms ] story [ 819 ms ] threadhttp://www.digizeitschriften.de/download/PPN266833020_0039/P...
http://www.digizeitschriften.de/download/PPN266833020_0039/P...
Thanks for the interesting blog piece though - maybe you could write one about Gentzen's consistency proof?
https://leanprover.github.io/logic_and_proof/nd_quickref.htm...
The innovation is essential to the Curry-Howard correspondence, because this labelling of assumptions matches variable bindings in typed lambda calculus.
> 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
>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.
Cf. https://en.wikipedia.org/wiki/Flight_and_expulsion_of_German...
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.