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

DOI10.1007/s11229-021-03418-8zbMath1528.03090arXiv2110.09921MaRDI QIDQ6180164

Nils Kürbis

Publication date: 19 January 2024

Published in: Synthese (Search for Journal in Brave)

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)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Natural deduction with general elimination rules
• Sequents and trees. An introduction to the theory and applications of propositional sequent calculi
• Meaning approached via proofs
• Validity concepts in proof-theoretic semantics
• NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION
• Proof and Falsity
• Gentzen's Proof of Normalization for Natural Deduction
• On Inversion Principles
• SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS
• Identity and harmony
• Inversion Principles and Introduction Rules

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