Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules

DOI10.1007/S11229-021-03418-8MaRDI QIDQ6180164zbMATH OpenFDO

Authors Nils Kürbis

Publication date 19 January 2024

Published in Synthese (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2110.09921

zbMATH Keywords

harmonystabilityproof theoryintuitionistic logicnormalisationgeneral elimination rulesgeneral introduction rules

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Abstract: This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions in normal form have the subformula property.

Recommendations

• Normalisation and subformula property for a system of classical logic with Tarski's rule
• A normalizing system of natural deduction for intuitionistic linear logic
• An alternative natural deduction for the intuitionistic propositional logic
• scientific article; zbMATH DE number 1406467
• scientific article; zbMATH DE number 3275554

Cites work

• scientific article; zbMATH DE number 1337625 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 819916 (Why is no real title available?)
• scientific article; zbMATH DE number 3285196 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Gentzen's Proof of Normalization for Natural Deduction
• Identity and harmony
• Inversion principles and introduction rules
• Meaning approached via proofs
• Natural deduction with general elimination rules
• Normal derivability in classical natural deduction
• On Inversion Principles
• Proof and falsity. A logical investigation
• Proof-theoretic semantics, a problem with negation and prospects for modality
• Saved from the cellar. Gerhard Gentzen's shorthand notes on logic and foundations of mathematics
• Sequents and trees. An introduction to the theory and applications of propositional sequent calculi
• Structural proof theory. With an appendix by Aarne Ranta
• Subformula and separation properties in natural deduction via small Kripke models
• Validity concepts in proof-theoretic semantics

Cited in

(1)

• Bilateral inversion principles

This page was built for publication: Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6180164)