Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus
type: Item
instance of: scholarly article
title: Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus
zbMATH Open document ID: 0908.03016
author: Wil Dekkers
author: Martin W. Bunder
author: Henk Barendregt
published in: Archive for Mathematical Logic
publication date: 1999-03-07T00:00:00Z
full work available at URL: https://ro.uow.edu.au/eispapers/1892
review text: The idea of illative combinatory logic ILC -- which has its roots in the pioneering work of Curry and Church in the early thirties -- is to extend usual combinatory logic, which is an equational theory of (self-applicable) operations, with a kind of abstract deducibility relation, in order to represent ordinary logic and even mathematics in ILC. The program of ILC is challenging and not easy to implement: since the early work of the founding fathers Curry and Church, many systems have been proposed and some of them were found inconsistent or too weak, others still need a consistency proof. The present paper is the continuation of the 1993 paper of the authors [\textit{H. Barendregt, M. Bunder} and \textit{W. Dekkers}, ``Systems of illative combinatory logic complete for first-order propositional and predicate calculus'', J. Symb. Logic 58, 769-788 (1993; Zbl 0791.03006)], where they investigate systems of ILC which are well-suited for representing propositional and elementary predicate calculus. The main result concerns completeness theorems for two indirect translations of two systems of ILC (by ``indirect translation'' the authors mean an interpretation which does not exploit the propositions-as-types idea). Roughly, the typical theorem states that if the translation of \(A\) is derivable in a system of ILC from the translation of a set \(X\) of premises, then \(A\) is derivable from \(X\) in predicate (or propositional) logic. It is important to stress that these results imply the consistency of the ILC-systems; they also round off the soundness and completeness theorems for direct and indirect translations. The paper is not self-contained and it can be read only with an adequate acquaintance with the cited 1993 paper. The methods of proofs are syntactical (for instance, cut elimination is applied).
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1210621
zbMATH Keywords: illative combinatory logic
zbMATH Keywords: lambda calculus
zbMATH Keywords: consistency
zbMATH Keywords: completeness
reviewed by: Andrea Cantini
MaRDI profile type: Publication
OpenAlex ID: W2159511425
DOI: 10.1007/S001530050102
description: scientific article; zbMATH DE number 1210621