# Independence of connectives in intuitionistic logic

Consider the intuitionistic propositional logic with $$\neg, \vee, \land, \to$$ as primitive connectives. My question is, can any three of these connectives be used to define the remaining one? So, I am asking for four proofs that the remaining connective can or can't be defined in terms of the other three.

No three intuitionistic connectives can be used to define the fourth one. McKinsey [1] showed this using nigh-trivial semantic proofs: in modern terminology, we would say that he constructs Heyting algebras as counterexamples. Despite its age, the article remains very readable, and answers your question thoroughly.

Here I'll present some proof-theoretic arguments which make use of cut-elimination, and show that in particular disjunction and negation are independent of the other connectives. Unlike semantic proofs, these generalize straightforwardly to the first-order case (in fact, note that the independence of the quantifiers $$\forall$$ and $$\exists$$ follows from my answer to your previous, related question). For the other two connectives (conjunction, implication) I present a variant of McKinsey's proofs: while the independence of conjunction and implication can be shown proof-theoretically as well, the methods I know require quite a bit of symbol-pushing.

We will use the following property of the intuitionistic propositional calculus, which you can prove by induction on (cut-free) derivations (see also [2], Theorem 4.2.4).

• Disjunction property: if $$\Gamma$$ of does not contain any disjunction connectives, and $$\Gamma \vdash M \vee N$$, then we can find a proof of either $$\Gamma \vdash M$$ or $$\Gamma \vdash N$$.

I. Disjunction $$\vee$$ is independent of the other connectives $$\neg, \rightarrow, \wedge$$:

Suppose that we can find a formula $$Q$$ in the the $$\{\neg, \rightarrow, \wedge\}$$ fragment such that $$Q \vdash M \vee N$$ and $$M \vee N \vdash Q$$ holds for the atomic propositions $$M,N$$.

Since $$Q \vdash M \vee N$$ and $$Q$$ does not contain disjunctions, we have either $$Q\vdash M$$ or $$Q\vdash N$$ by the disjunction property.

But of course the same fails for $$M \vee N$$: neither $$M \vee N \vdash M$$ nor $$M \vee N \vdash N$$ are provable for atomic $$M,N$$. (Why? Cut $$M \vee N \vdash M$$ against the usual proof of $$N \vdash M \vee N$$ to obtain a proof of $$N \vdash M$$. By cut-elimination this would also have a cut-free proof, but that's impossible: what would be the last step?!)

Hence the supposed definition $$Q$$ cannot exist.

II. Negation $$\neg$$ is independent of the other connectives $$\rightarrow, \vee, \wedge$$:

The connectives $$\{\rightarrow, \vee, \wedge\}$$ build provable formulas from provable propositional atoms: if $$\vdash A$$ and $$\vdash B$$, then for any formula $$Q$$ made up of $$A,B$$ and the connectives $$\{\rightarrow, \vee, \wedge\}$$ we have $$\vdash Q$$. However, $$\neg$$ can be used to build unprovable formulae from provable atoms: if $$\vdash A$$ and $$\vdash \neg A$$ both hold, then we can extract a proof of $$A \vdash$$ (by looking at the last step of a cut-free proof of $$\vdash \neg A$$), so by cut we'd have a proof of the empty sequent $$\vdash$$. But that is impossible (what would be the last step of its cut-free proof?), so if $$A$$ is provable then $$\neg A$$ is not provable. Hence we cannot express $$\neg$$ in the $$\{\rightarrow, \vee, \wedge\}$$ fragment.

The set of numbers $$\{1,2,3,4,6,9,12,18,36\}$$ forms a Heyting algebra when equipped with the operations $$\gcd$$ (greatest common divisor, interpreting conjunction), $$\mathrm{lcm}$$ (least common multiple, interpreting disjunction), and the following implication operation $$\Rightarrow$$:

=>|  1  2  3  4  6  9 12 18 36
--+---------------------------
1 | 36 36 36 36 36 36 36 36 36
2 |  9 36  9 36 36  9 36 36 36
3 |  4  4 36  4 36 36 36 36 36
4 |  9 18  9 36 18  9 36 18 36
6 |  1  4  9  4 36  9 36 36 36
9 |  4  4 12  4 12 36 12 36 36
12|  1  2  9  4 18  9 36 18 36
18|  1  4  3  4 12  9 12 36 36
36|  1  2  3  4  6  9 12 18 36


All you need to check is that if $$z$$ divides $$x \Rightarrow y$$ then $$\gcd(z,x)$$ divides $$y$$, and vice versa (admittedly, this is the tedious/annoying part of the semantic method, but you can cut this particular verification short using prime factors).

III. Conjunction $$\wedge$$ is independent of the other connectives $$\neg, \vee, \rightarrow$$.

The set $$H = \{1,12,18,36\}$$ is clearly closed under least common multiples. Referring to the table above, we can check that it is closed under $$\Rightarrow$$ as well. Since $$1 \in H$$, it follows that $$H$$ is closed under $$\neg$$ too. So, if conjunction was definable in the fragment $$\{ \neg, \vee, \rightarrow \}$$, then our set would be closed under greatest common divisors as well. But $$\gcd(12,18) = 6 \not\in H$$.

IV. Implication is independent of the other connectives $$\neg, \vee, \wedge$$.

Take the Heyting algebra above. Clearly the set $$S = \{1,6,12,36\}$$ is closed under both $$\gcd$$ and $$\mathrm{lcm}$$. Moreover, it is closed under negation, since $$1 \Rightarrow 1 = 36$$ and $$x \Rightarrow 1 = 1$$ for any $$x > 1$$ in $$S$$. So if implication was definable in the $$\{ \neg, \vee, \wedge \}$$ fragment, it would preserve membership in $$S$$. But $$12 \Rightarrow 6 = 18 \not\in S$$.

[1] J.C.C. McKinsey. Proof of the independence of the primitive symbols of Heyting’s calculus of propositions. The Journal of Symbolic Logic, 4(04), 155–158., 1939. doi:10.2307/2268715

[2] A. S. Troelstra, H. Schwichtenberg: Basic Proof Theory, 2nd edition, 2000. ISBN 9781139168717

edit Simplified the wording of some of the arguments, added links and references