NDLI: Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Please wait, while we are loading the content...

Archive for Mathematical Logic : Volume 56

Archive for Mathematical Logic : Volume 55

Archive for Mathematical Logic : Volume 54

Archive for Mathematical Logic : Volume 53

Archive for Mathematical Logic : Volume 52

Archive for Mathematical Logic : Volume 51

Archive for Mathematical Logic : Volume 50

Archive for Mathematical Logic : Volume 49

Archive for Mathematical Logic : Volume 48

Archive for Mathematical Logic : Volume 47

Archive for Mathematical Logic : Volume 46

Archive for Mathematical Logic : Volume 45

Archive for Mathematical Logic : Volume 44

Archive for Mathematical Logic : Volume 43

Archive for Mathematical Logic : Volume 42

Archive for Mathematical Logic : Volume 41

Archive for Mathematical Logic : Volume 40

Archive for Mathematical Logic : Volume 39

Archive for Mathematical Logic : Volume 38

Archive for Mathematical Logic : Volume 37

Archive for Mathematical Logic : Volume 37, Issue 8, November 1998

Archive for Mathematical Logic : Volume 37, Issue 7, October 1998

Archive for Mathematical Logic : Volume 37, Issue 5-6, July 1998

Editorial Logic Colloquium '95, Haifa, Israel : Invited papers on proof theory

A proof-theoretic analysis of collection

Note on generalizing theorems in algebraically closed fields

Planar and braided proof-nets for multiplicative linear logic with mix

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Lebesgue numbers and Atsuji spaces in subsystems of second-order arithmetic

Elimination of Skolem functions for monotone formulas in analysis

The $\mu$ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals

Normal deduction in the intuitionistic linear logic

Bounding derivation lengths with functions from the slow growing hierarchy

Archive for Mathematical Logic : Volume 37, Issue 4, June 1998

Archive for Mathematical Logic : Volume 37, Issue 3, April 1998

Archive for Mathematical Logic : Volume 37, Issue 2, March 1998

Archive for Mathematical Logic : Volume 37, Issue 1, December 1997

Archive for Mathematical Logic : Volume 36

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Content Provider	Springer Nature Link
Author	Dekkers, Wil Bunder, Martin Barendregt, Henk
Copyright Year	1998
Abstract	Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of $\lambda$ -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent).
Starting Page	327
Ending Page	341
Page Count	15
File Format	PDF
ISSN	09335846
Journal	Archive for Mathematical Logic
Volume Number	37
Issue Number	5-6
e-ISSN	14320665
Language	English
Publisher	Springer-Verlag
Publisher Date	1998-07-01
Publisher Place	Berlin Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Philosophy Logic

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus (1995).

Systems of illative combinatory logic complete for first-order propositional and predicate calculus

Systems of illative combinatory logic complete for first-order propositional and predicate calculus (1993).

Systems of illative combinatory logic complete for first order propositional and predicate calculus (1993)

Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic (1997).

A semantic approach to illative combinatory logic ∗.

Semantical Completeness of First-Order Predicate Logic and the Weak Fan Theorem

Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic

Hilbert System for Predicate Logic 1 Completeness Theorem for First Order Logic 1.1 Compactness Theorem for Propositional Logic

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus

Similar Documents

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus (1995).

Systems of illative combinatory logic complete for first-order propositional and predicate calculus

Systems of illative combinatory logic complete for first-order propositional and predicate calculus (1993).

Systems of illative combinatory logic complete for first order propositional and predicate calculus (1993)

Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic (1997).

A semantic approach to illative combinatory logic ∗.

Semantical Completeness of First-Order Predicate Logic and the Weak Fan Theorem

Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic

Hilbert System for Predicate Logic 1 Completeness Theorem for First Order Logic 1.1 Compactness Theorem for Propositional Logic

Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus