The Semantics of Entailment Omega

Notre Dame Journal of Formal Logic 43 (3):129-145 (2002)
This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL
Keywords minimal relevant logic   intersection type theory   lambda model   Curry-Howard isomorphism   Harrop Formulas
Categories (categorize this paper)
DOI 10.1305/ndjfl/1074290712
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 37,100
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Ternary Relations and Relevant Semantics.Robert K. Meyer - 2004 - Annals of Pure and Applied Logic 127 (1-3):195-217.

Add more citations

Similar books and articles

Neighborhoods for Entailment.Lou Goble - 2003 - Journal of Philosophical Logic 32 (5):483-529.
General Models and Entailment Semantics for Independence Logic.Pietro Galliani - 2013 - Notre Dame Journal of Formal Logic 54 (2):253-275.
Syntax and Semantics of the Logic $\Mathcal{L}^\Lambda_{\Omega\Omega}$.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
The Semantics of Entailment—II.Richard Routley & Robert K. Meyer - 1972 - Journal of Philosophical Logic 1 (1):53 - 73.
The Semantics of Entailment — III.Richard Routley & Robert K. Meyer - 1972 - Journal of Philosophical Logic 1 (2):192 - 208.
Almost Everywhere Domination.Natasha L. Dobrinen & Stephen G. Simpson - 2004 - Journal of Symbolic Logic 69 (3):914-922.
A Natural Deduction System for First Degree Entailment.Allard Tamminga & Koji Tanaka - 1999 - Notre Dame Journal of Formal Logic 40 (2):258-272.
Limits for Paraconsistent Calculi.Walter A. Carnielli & João Marcos - 1999 - Notre Dame Journal of Formal Logic 40 (3):375-390.
An Ordinal Partition Avoiding Pentagrams.Jean A. Larson - 2000 - Journal of Symbolic Logic 65 (3):969-978.
Game Theoretical Semantics and Entailment.D. E. Over - 1981 - Studia Logica 40 (1):67 - 74.
Gts and Interrogative Tableaux.Stephen Harris - 1994 - Synthese 99 (3):329 - 343.
Models with the Ω-Property.Roman Kossak - 1989 - Journal of Symbolic Logic 54 (1):177-189.


Added to PP index

Total downloads
13 ( #456,730 of 2,308,306 )

Recent downloads (6 months)
1 ( #447,932 of 2,308,306 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature