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

Download options


    Upload a copy of this work     Papers currently archived: 72,805

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

20 (#563,435)

6 months
1 (#386,499)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Semantical Analysis of Modal Logic I. Normal Propositional Calculi.Saul A. Kripke - 1963 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9 (5‐6):67-96.
The Semantics of Entailment — III.Richard Routley & Robert K. Meyer - 1972 - Journal of Philosophical Logic 1 (2):192 - 208.
Concerning Formulas of the Types a →B ∨C, a →(Ex)B(X).Ronald Harrop - 1960 - Journal of Symbolic Logic 25 (1):27-32.
Algebraic Analysis of Entailment I.Robert K. Meyer & Richard Routley - 1972 - Logique Et Analyse 15 (59/60):407-428.

View all 8 references / Add more references

Citations of this work

Ternary Relations and Relevant Semantics.Robert K. Meyer - 2004 - Annals of Pure and Applied Logic 127 (1-3):195-217.
Combinator Logics.Lou Goble - 2004 - Studia Logica 76 (1):17 - 66.
Introduction.Greg Ray - 1999 - Topoi 18 (2):87-92.

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 M. 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.