Logic without disjunction

Question

I'm working on a small proof system, which in principle only has equality as predicate. This equality has some axioms which make them sort of a structural equality: two terms are equal iff their constructors coincide and every subterm is equal too. Apart from equality, there's also conjunction and implication.

Currently, I'm trying to add negation to the language to make it more expressive. Right now, I've introduced a new "not equal" predicate, with some structural rules too: two terms with different constructors are "not equal", and if two subterms are "not equal" then two terms containing them in the same position are "not equal".

The problem comes with implication. In principle, if I have a = b => F a b = G, I can build a contrapositive implication F a b != G => a != b. The problem is that, if I have conjunction, I cannot directly build the contrapositive implication, like in a = b and a = c => F a b c = G, bcause my system doesn't contain disjunction.

Are there any references on logic with this property? Is there any account of the expressiveness I loose by omitting disjunction altogether?

Answer 1

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.

Answer 2

I am too removed from the subject these days, so my answer might be not very insightful (but I hope experts will help here). If you are willing to admit quantifiers (which appear in some proof systems), you may end up with an equivalential calculus resembling Leśniewski's protothetics (you might want to check his mereology and ontology as well, as you are interested in equality of terms whose "constructors" coincide). Quoting from the Stanford Encyclopedia of Philosophy, http://plato.stanford.edu/entries/lesniewski/

“Leśniewski’s preference for an axiom system, based in part on the success of Ontology, and also on considerations about the nature of definition, was to base a logical system on the single connective of material equivalence, together with the universal quantifier. He was held up for some time in doing this for Protothetic by his inability to see how to eliminate the connective of conjunction in terms of equivalence. Given quantification and equivalence, negation is easy to define, in a way Russell once suggested to Frege:

$\text{Def. }\sim: \forall p\,\ulcorner {\sim} p \leftrightarrow (p \leftrightarrow \forall r \,\ulcorner r\urcorner)\urcorner$

The solution was found for Leśniewski by his 21-year-old doctoral student Alfred Teitelbaum, later renowned under his adopted name as Alfred Tarski. It consisted in quantifying not just sentences but sentential functions or connectives:

$\text{Def. }\wedge: \forall pq\,\ulcorner p \wedge q \leftrightarrow \forall f\,\ulcorner p \leftrightarrow (f(p) \leftrightarrow f(q))\urcorner \urcorner$

in this case, quantifying one-place connectives. Assuming there are just four of these connectives, assertion, negation, Verum (tautology) and Falsum (contradiction), it is straightforward to show that the right-hand side is equivalent to the conjunction of $p$ and $q$. Tarski's doctoral dissertation centres around this result.

As to axiomatization, Leśniewski knew that the pure theory of equivalence could be based on two axioms stating skew-transitivity and associativity:

$P1 \quad ((p \leftrightarrow r)\leftrightarrow (q \leftrightarrow p)) \leftrightarrow (r \leftrightarrow q)$

$P2 \quad (p \leftrightarrow (q\leftrightarrow r)) \leftrightarrow ((p \leftrightarrow q) \leftrightarrow r)$.

Pure equivalential calculus has the quaint property, shown by Leśniewski, that a formula is a theorem if and only if every propositional variable in it occurs an even number of times.”

I make this CW, first because I am not an expert; second, because it seems I could use some help on TeX, which is acting up...