Classical logic, intuitionistic logic, and the Peirce rule
type: Item
instance of: scholarly article
title: Classical logic, intuitionistic logic, and the Peirce rule
zbMATH Open document ID: 0768.03034
author: Henry Africk
published in: Notre Dame Journal of Formal Logic
publication date: 1993-02-22T00:00:00Z
review text: In Gentzen's sequent formalization of first-order logic, the essential difference between the classical system LK and the intuitionistic system LJ is that sequents \(A_ 1,\dots,A_ m\to B_ 1,\dots,B_ n\) are restricted to \(n\leq 1\) for the intuitionistic system LJ. Adjoining the Peirce rule \[ {A\Longrightarrow B, \Gamma\longrightarrow A\over\Gamma\longrightarrow A} \] to the system LJ makes it as strong as LK. Therefore it is possible to translate all LK proofs into the system \(\text{LJ}+\text{Peirce}\) rule. A simple algorithm for this purpose, translating an LK proof into the system \(\text{LJ}+\text{Peirce}\) rule, is presented in the paper. A consequence of this result is a primitive recursive cut-elimination operator for \(\text{LJ}+\text{Peirce}\) rule, which exploits the cut- elimination theorem for LK.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B10
zbMATH DE Number: 120388
zbMATH Keywords: Gentzen calculus
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: proof transformation algorithm
zbMATH Keywords: Peirce rule
zbMATH Keywords: primitive recursive cut-elimination operator
reviewed by: Hans Jürgen Ohlbach
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1093636101
OpenAlex ID: W2061477295
DOI: 10.1305/NDJFL/1093636101
description: scientific article; zbMATH DE number 120388