Independence of connectives in intuitionistic logic

Question

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.

Answer 1

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

Answer 2

Short answer: No. The only minimally functionally complete operator sets of intuitionistic logic are {¬, ↔, ∧} and {⊥, ↔, ∨}. But, since normally (A↔B) := (A→B)∧(B→A), you basically have to have them all.

For the second operator set, the minimally functional equivalencies are as follows:

$$¬A ↔ (A↔⊥)$$ $$(A∧B) ↔ (((A∨B)↔B)↔A)$$ $$(A→B) ↔ ((A∨B)↔B)$$