Types of I-free hereditary right maximal terms
type: Item
instance of: scholarly article
title: Types of I-free hereditary right maximal terms
zbMATH Open document ID: 1089.03011
author: Katalin Bimbó
published in: Journal of Philosophical Logic
publication date: 2006-01-23T00:00:00Z
review text: By the formulas-as-types (or Curry-Howard) isomorphism, for every closed \(\lambda\)-term there is a theorem of the implicational intuitionistic logic \(H_\to\), which is its type. Also, every such theorem is the type of a \(\lambda\)-term which represents a natural deduction style proof of the theorem. The theorems of weaker logics than \(H_\to\) have subsets of the closed lambda terms as their sets of proofs/inhabitants. Such subsets of the closed lambda terms were identified by \textit{P. Trigg, J. R. Hindley} and \textit{M. W. Bunder} [``Combinatory abstraction using \(B, B'\) and friends'', Theor. Comput. Sci. 135, 405--422 (1994; Zbl 0838.03012)] for a large number of logics including the implicational fragment \(T_\to\) of Ticket Entailment. Other work on this appears in the reviewer's chapter ``Combinators, proofs and implicational logics'' [in: D. M. Gabbay and F. Guenthner (eds.), Handbook of philosophical logic. Vol. 6. 2nd ed. Dordrecht: Kluwer, 229--286 (2002; Zbl 1065.03002)]. The current paper also identifies the class of \(\lambda\)-terms representing the proofs of \(T_\to\) and finds a Fitch-style formulation for \(T_\to\).
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B47
zbMATH DE Number: 5000205
zbMATH Keywords: Combinatory logic
zbMATH Keywords: decidability
zbMATH Keywords: lambda calculus
zbMATH Keywords: natural deduction
reviewed by: Martin W. Bunder
MaRDI profile type: Publication
full work available at URL: s10992-005-2831-x
OpenAlex ID: W1969075264
cites work: Q4085699
cites work: Q4297115
cites work: Q5547552
cites work: Combinatory logic. With two sections by William Craig.
cites work: Combinatory logic. Vol. II
cites work: Q4342081
cites work: A mathematical introduction to logic.
cites work: Completeness of the normal typed fragment of the \(\lambda\)-system \(U\)
cites work: Q4722037
DOI: 10.1007/S10992-005-2831-X
description: scientific article; zbMATH DE number 5000205