Open Access. Powered by Scholars. Published by Universities.®
Science and Technology Studies Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 3 of 3
Full-Text Articles in Science and Technology Studies
Intersection Type Systems And Logics Related To The Meyer-Routley System B+, Martin W. Bunder
Intersection Type Systems And Logics Related To The Meyer-Routley System B+, Martin W. Bunder
Faculty of Engineering and Information Sciences - Papers: Part A
Some, but not all, closed terms of the lambda calculus have types; these types are exactly the theorems of intuitionistic implicational logic. An extension of these simple (→) types to intersection (or →∧) types allows all closed lambda terms to have types. The corresponding →∧ logic, related to the Meyer–Routley minimal logic B+ (without ∨), is weaker than the →∧ fragment of intuitionistic logic. In this paper we provide an introduction to the above work and also determine the →∧ logics that correspond to certain interesting subsystems of the full →∧ type theory.
The Strong Relevance Logics, Martin W. Bunder
The Strong Relevance Logics, Martin W. Bunder
Faculty of Engineering and Information Sciences - Papers: Part A
The tautology p - q - p is not a theorem of the various relevance logics (see Anderson and Belnap [1]) because q is not considered to be relevant in the derivation of final p. We can take this lack of relevance to mean simply that p-q-p could have been proved without q and its -, i.e., p-p. By the same criterion we could say that in ((p-p) -q) -q p-p is not relevant. In general we will say that any theorem A of an implicational logic is strongly relevant if there is no subpart B ! which can be …
Classical Versions Of Bci, Bck And Bciw Logics, Martin W. Bunder, John K. Slaney
Classical Versions Of Bci, Bck And Bciw Logics, Martin W. Bunder, John K. Slaney
Faculty of Engineering and Information Sciences - Papers: Part A
The question is, is there a formula X, independent of B,C,K1, I and W that creates distinct subclassical logics BCIX,BCKX and BCIWX, while BCKWX is the full classical implicational logic TV?