Normal derivations and sequent derivations
type: Item
instance of: scholarly article
title: Normal derivations and sequent derivations
zbMATH Open document ID: 1207.03070
author: Mirjana Borisavljevi
published in: Journal of Philosophical Logic
publication date: 2009-07-13T00:00:00Z
review text: Normal proofs in natural deduction systems for intuitionistic logic roughly correspond to cut-free sequent derivations. This article elaborates on this correspondence. First, a system \(\mathcal{N}\) for natural deductions and a system \(\mathcal{S}\) for sequent derivations are introduced. Then, functions \(\phi\) and \(\varphi\) are defined that map natural deductions of \(\mathcal{N}\) to sequent derivations of \(\mathcal{S}\) and vice versa, so that \(\varphi\circ\phi\) is the identity on natural deductions, and further, the following relationship holds true: If \(\mathcal{D}\) is a sequent derivation without maximum cuts (i.e. cuts that correspond to maximum segments from natural deductions), then \(\varphi\mathcal{D}\) is a normal derivation, and, conversely, if \(\varphi\mathcal{D}\) is a normal derivation, then \(\mathcal{D}\) is a sequent derivation without maximum cuts. The author concludes that therefore sequent derivations without maximum cuts and normal derivations ``are the same''.
reviewed by: D. Probst
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 5577835
zbMATH Keywords: cut elimination
zbMATH Keywords: normalization
MaRDI profile type: Publication
full work available at URL: s10992-008-9084-4
OpenAlex ID: W2047037379
cites work: Extended Natural Deduction Images of Conversions from the System of Sequents
cites work: A connection between cut elimination and normalization
cites work: Minimum segments in sequent derivations
cites work: Q4397029
cites work: Natural deduction with general elimination rules
cites work: Normalization as a homomorphic image of cut-elimination
cites work: Q5559220
cites work: Q5632554
cites work: Q4716271
cites work: The correspondence between cut-elimination and normalization
DOI: 10.1007/S10992-008-9084-4
description: scientific article; zbMATH DE number 5577835