Gentzen's Hauptsatz (cut elimination theorem) : This is a fundamental result in structural proof theory, and is at the heart of Gentzen's consistency proof of elementary number theory. The techniques underlying it (proof normalisation) are fundamental to much modern machinery in proof theory. It is very funny that the word literally means "main theorem," with no reference to the subject domain, yet it is standard in logic in English to use just the word "Hauptsatz" solely to refer to this single theorem (family of) theorem(s) in proof theory.
|
3 | Cleaned it up a bit, made clear that there are many different cut-elimination theorems | ||
|
|
||||
|
|
2 | added 2 characters in body | ||
|
Gentzen's Haupsatz Hauptsatz (cut elimination theorem) : This is a fundamental result in structural proof theory, and is at the heart of Gentzen's consistency proof of elementary number theory. The techniques underlying it (proof normalisation) are fundamental to much modern machinery in proof theory. It is very funny that the word literally means "main theorem," with no reference to the subject domain, yet it is standard in logic in English to use the word "Haupsatz" Hauptsatz" solely to refer to this single theorem in proof theory. |
||||
|
|
1 | [made Community Wiki] | ||
|
Gentzen's Haupsatz (cut elimination theorem) : This is a fundamental result in structural proof theory, and is at the heart of Gentzen's consistency proof of elementary number theory. The techniques underlying it (proof normalisation) are fundamental to much modern machinery in proof theory. It is very funny that the word literally means "main theorem," with no reference to the subject domain, yet it is standard in logic in English to use the word "Haupsatz" solely to refer to this single theorem in proof theory. |
||||
