Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus (Q1267843): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(4 intermediate revisions by 3 users not shown) | |||
Property / author | |||
Property / author: Martin W. Bunder / rank | |||
Property / author | |||
Property / author: Hendrik Pieter Barendregt / rank | |||
Property / reviewed by | |||
Property / reviewed by: Andrea Cantini / rank | |||
Property / author | |||
Property / author: Martin W. Bunder / rank | |||
Normal rank | |||
Property / author | |||
Property / author: Hendrik Pieter Barendregt / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Andrea Cantini / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2159511425 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 01:49, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus |
scientific article |
Statements
Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus (English)
0 references
7 March 1999
0 references
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).
0 references
illative combinatory logic
0 references
lambda calculus
0 references
consistency
0 references
completeness
0 references