Gentzenizing Schroeder-Heister's natural extension of natural deduction (Q923083)

From MaRDI portal





scientific article; zbMATH DE number 4170904
Language Label Description Also known as
default for all languages
No label defined
    English
    Gentzenizing Schroeder-Heister's natural extension of natural deduction
    scientific article; zbMATH DE number 4170904

      Statements

      Gentzenizing Schroeder-Heister's natural extension of natural deduction (English)
      0 references
      0 references
      1990
      0 references
      The author provides an example of how the use of the Gentzen-type sequential calculus simplifies a complex natural deduction formalism by giving the Gentzen-type version to the natural deduction system of Schroeder-Heister. The notions of the natural deduction system that are difficult to handle become redundant, so that the complex normalization proof can be replaced by a standard cut-elimination proof. The resulting Gentzen system is essentially the same as the intuitionistic one, which therefore sheds new light on the connection between Schroeder-Heister's higher-order rules and intuitionistic implication.
      0 references
      Gentzen-type sequential calculus
      0 references
      natural deduction system of Schroeder- Heister
      0 references
      normalization
      0 references
      cut-elimination
      0 references
      higher-order rules
      0 references
      intuitionistic implication
      0 references
      0 references

      Identifiers