Strong normalization of a symmetric lambda calculus for second-order classical logic
type: Item
instance of: scholarly article
title: Strong normalization of a symmetric lambda calculus for second-order classical logic
zbMATH Open document ID: 1022.03007
author: Yoriyuki Yamagata
published in: Archive for Mathematical Logic
publication date: 2003-09-16T00:00:00Z
review text: We extend \textit{F. Barbanera} and \textit{S. Berardi}'s symmetric lambda calculus [Inf. Comput. 125, 103-117 (1996; Zbl 0853.68159)] to second-order propositional logic and prove its strong normalizability. The proof proceeds by extending Barbanera and Berardi's construction of reducibility to infinitary propositional logic, and reducibility candidates are defined as the class closed under such construction. A similar proof was found independently by \textit{M. Parigot} [Lect. Notes Comput. Sci. 1974, 442-453 (2000)].
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 1982463
zbMATH Keywords: second-order logic
zbMATH Keywords: symmetric lambda calculus
zbMATH Keywords: strong normalizability
zbMATH Keywords: infinitary propositional logic
zbMATH Keywords: reducibility candidates
MaRDI profile type: Publication
full work available at URL: s001530200007
OpenAlex ID: W2092082919
DOI: 10.1007/S001530200007
description: scientific article; zbMATH DE number 1982463