Permutability of Proofs in Intuitionistic Sequent Calculi

Roy Dyckhoff; L Pinto

doi:10.1016/S0304-3975(98)00138-8

Permutability of Proofs in Intuitionistic Sequent Calculi

Roy Dyckhoff, L Pinto

School of Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3) are inter-permutable (using a set of basic "permutation reduction rules" derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. (C) 1999-Elsevier Science B.V. All rights reserved.

Original language	English
Pages (from-to)	141-155
Number of pages	15
Journal	Theoretical Computer Science
Volume	212
Issue number	1-2
DOIs	https://doi.org/10.1016/S0304-3975(98)00138-8
Publication status	Published - 6 Feb 1999

Keywords

intuitionistic logic
proof theory
natural deduction
sequent calculus
LOGIC

Access to Document

10.1016/S0304-3975(98)00138-8

Cite this

@article{316445cdce694e1daee5f93849295cf8,

title = "Permutability of Proofs in Intuitionistic Sequent Calculi",

abstract = "We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3) are inter-permutable (using a set of basic {"}permutation reduction rules{"} derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. (C) 1999-Elsevier Science B.V. All rights reserved.",

keywords = "intuitionistic logic, proof theory, natural deduction, sequent calculus, LOGIC",

author = "Roy Dyckhoff and L Pinto",

year = "1999",

month = feb,

day = "6",

doi = "10.1016/S0304-3975(98)00138-8",

language = "English",

volume = "212",

pages = "141--155",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier Science BV",

number = "1-2",

}

TY - JOUR

T1 - Permutability of Proofs in Intuitionistic Sequent Calculi

AU - Dyckhoff, Roy

AU - Pinto, L

PY - 1999/2/6

Y1 - 1999/2/6

N2 - We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3) are inter-permutable (using a set of basic "permutation reduction rules" derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. (C) 1999-Elsevier Science B.V. All rights reserved.

AB - We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3) are inter-permutable (using a set of basic "permutation reduction rules" derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. (C) 1999-Elsevier Science B.V. All rights reserved.

KW - intuitionistic logic

KW - proof theory

KW - natural deduction

KW - sequent calculus

KW - LOGIC

U2 - 10.1016/S0304-3975(98)00138-8

DO - 10.1016/S0304-3975(98)00138-8

M3 - Article

SN - 0304-3975

VL - 212

SP - 141

EP - 155

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1-2

ER -

Permutability of Proofs in Intuitionistic Sequent Calculi

Abstract

Keywords

Access to Document

Fingerprint

Cite this