Basic Relevant Theories for Combinators at Levels I and II

  • Koushik Pal Department of Mathematics, Indian Institute of Technology Kanpur
  • Robert K. Meyer Automated Reasoning Group, RSISE, Australian National University

Abstract

The system B+ is the minimal positive relevant logic. B+ is trivially extended to B+T on adding a greatest truth (Church constant) T. If we leave ∨ out of the formation apparatus, we get the fragment B∧T. It is known that the set of ALL B∧T theories provides a good model for the combinators CL at Level-I, which is the theory level. Restoring ∨ to get back B+T was not previously fruitful at Level-I, because the set of all B+T theories is NOT a model of CL. It was to be expected from semantic completeness arguments for relevant logics that basic combinator laws would hold when restricted to PRIME B+T theories. Overcoming some previous difficulties, we show that this is the case, at Level I. But this does not form a model for CL. This paper also looks for corresponding results at Level-II, where we deal with sets of theories that we call propositions. We adapt work by Ghilezan to note that at Level-II also there is a model of CL in B∧T propositions. However, the corresponding result for B+T propositions extends smoothly to Level-II only in part. Specifically, only some of the basic combinator laws are proved here. We accordingly leave some work for the reader.

Author Biographies

Koushik Pal, Department of Mathematics, Indian Institute of Technology Kanpur
Robert K. Meyer, Automated Reasoning Group, RSISE, Australian National University
Published
2005-07-08
How to Cite
PAL, Koushik; MEYER, Robert K.. Basic Relevant Theories for Combinators at Levels I and II. The Australasian Journal of Logic, [S.l.], v. 3, july 2005. ISSN 1448-5052. Available at: <https://ojs.victoria.ac.nz/ajl/article/view/1770>. Date accessed: 23 may 2019. doi: https://doi.org/10.26686/ajl.v3i0.1770.