Skip to main content
2 of 2
added googling advice

If you want your logic to be classical (i.e. to validate principles like the law of double negation), then as Emil Jeřábek says in comments, you can derive disjunction in terms of implication as $\varphi \lor \psi := (\varphi \to \psi) \to \psi$. Generally, in classical logics, there are so many ways to interdefine the connectives that it’s hard to give a not-too-weak system that doesn’t imply the full usual system.

On the other hand, if you are happy for your logic to end up constructive/intuitionistic (i.e. not be able to prove the law of double negation, excluded middle, etc), then yes, logics of this sort have been studied.

The two I’m most familiar with that omit disjunction are regular logic and the fragment of Martin-Löf Type Theory valid in any LCCC (see Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories), i.e. with just function types and product types.

However, both of these sound like overkill for your case — what you outline sounds more like the conjunction-implication fragment of intuitionistic logic. The sequent caluclus presentation nicely separates the rules for the various connectives, so that each one still works fine in the absence of the others. I don’t know anywhere that this specific fragment has been studied/discussed, I’m afraid, though I would guess that it has been.

Edit. Googling various groupings of the keywords conjunction, implication, fragment, intuitionistic, logic turns up quite a few papers working with such systems, though I can’t find any single paper taking the system itself as its object of study.