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

DOI10.1007/S11229-021-03418-8zbMATH Open1528.03090arXiv2110.09921MaRDI QIDQ6180164FDOQ6180164

Authors: Nils Kürbis 

Publication date: 19 January 2024

Published in: Synthese (Search for Journal in Brave)

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.

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

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

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)

Cites Work

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

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)