Gentz type calculus
Under Gentz type calculi is understood logic calculi of a particular type. They are named after the mathematician and logician Gerhard Gentzen because these calculi are similar to his sequential calculi .
Specifically, these are the sequential calculi LJ and LK , the systems of natural inference NJ and NK (J is the intuitionist and K is the classical calculus), the Beth tree calculus (tableaux) and the dialogic logic .
Unlike logic calculus of Hilbert type is established in the Gentz type calculi Gentzensche law , which states that the cut rule in the respective calculus permitted is. This means that the cutting rule does not have to be added to the calculation rules.
Web links
- Gerhard Gentzen: Investigations into logical reasoning. Mathematical Journal 39 (1934). Reprinted in: Karel Berka , Lothar Kreiser: Logic Texts , Berlin (East) 1986. Part 1 and Part 2
- Sequent Calculus by Alex Sakharov MathWorld