Gerhard Gentzen’s sequent calculus. Here the falsum is the sequent ” ->”, which can be obtained by the usage of some cut-rules only (the rule in the box). But if we eliminate the cut-rule, the sequent calculus we gain in this way is deductively equivalent with the original one. So it is consistent. Voila.
The formulae are from Gerhard Gentzen: Recherches Sur La Déduction Logique
Nincsenek megjegyzések:
Megjegyzés küldése