# Is $\lor$ definable in intuitionistic logic?

The Wikipedia page mentions that $\{\lor,\leftrightarrow,\bot\}$ and $\{\lor,\leftrightarrow,\neg\}$ are complete sets of operators for intuitionistic logic, and also gives a few equivalences for other operators in terms of $\lor$, but there are no equivalences listed for $\lor$ itself. So my question is whether it is possible to define an expression in $\{\land,\to,\neg\}$ (which also includes $\leftrightarrow,\bot$) that is intuitionistically equivalent to $\lor$ in the sense that it satisfies the "definition"

$$((A\lor B)\to C)\iff((A\to C)\land(B\to C)).\tag{1}$$

(I suspect the answer is no, but I'd like a proof.) This question extends to the classification of all minimal complete operator subsets of $\{\land,\lor,\to,\leftrightarrow,\neg,\top,\bot\}$. Depending on the answer to this question, it seems that we have

$$\{\lor,\leftrightarrow,\neg\},\{\lor,\leftrightarrow,\bot\},\{\lor,\land,\to,\neg\},\{\lor,\land,\to,\bot\}$$

if it is true, otherwise

$$\{\land,\to,\neg\},\{\land,\to,\bot\},\{\land,\leftrightarrow,\neg\},\{\land,\leftrightarrow,\bot\},\{\lor,\leftrightarrow,\neg\},\{\lor,\leftrightarrow,\bot\},\{\to,\leftrightarrow,\neg\},\{\to,\leftrightarrow,\bot\}.$$

• What exactly do you mean "define an expression that satisfies the definition"? Certain values of $A,B,C$ may satisfy that expression you gave at the end of the question. Did you mean, in short, if we can replace the $\vee$ with $\wedge,\rightarrow,\neg$ while keeping the expression correct? If yes, then what's wrong with replacing $(A \vee B)$ with $\neg(\neg A \wedge \neg B)$? – barak manos Feb 1 '15 at 6:38
• If anything, I would guess that $(A \lor B) \iff ((A \to B) \leftrightarrow B)$ would fit the bill, but I have not idea whether that would be a conservative extension to intuitionistic logic based on $\{\land,\to,\neg\}$. I "derived" this by taking (ϕ→ψ)↔((ϕ∨ψ)↔ψ) from the Wikipedia page, and applying associativity of $\leftrightarrow$, which is not intuitionistically valid. – MarnixKlooster ReinstateMonica Feb 1 '15 at 6:56
• The definition has to be intuitionistically valid, meaning that it does not imply any statements not implied by usual intuitionistic logic including $\lor$. Of course my first try was $(A\lor B)\iff((A\to B)\to B)$, but I think you can get Peirce's law from the assumption that it satisfies the equation (1). – Mario Carneiro Feb 1 '15 at 7:14
• @barakmanos Here is the intutionistic logic, and using truth-table is valid for classical logic only. In intutionistic logic, we cannot prove $p\lor q$ from $\lnot(\lnot p\land \lnot q)$. – Hanul Jeon Feb 1 '15 at 7:34
• @barakmanos Sorry, but there is no finite-valued faithful interpretation of intuitionistic logic. (See the part of the wiki article about Heyting algebras.) – Mario Carneiro Feb 1 '15 at 7:34

I will give the proof of undefinability of $\lor$ using $\land$, $\to$, $\lnot$ in propositional intutionistic logic. Notice that I referred the exercises 2.24 - 2.26 in "Lectures on the Curry-Howard isomorphism" by Morten Heine B. Sørensen and Paweł Urzyczyn.

The formula $\phi$ is negative if every propositional variable occurs only in the form $\lnot p$ and $\lor$ does not occur in $\phi$; that is, it only contains $\land$, $\to$ and $\lnot$ as logical connectives. A notable result is, if $\phi$ is negative formula then $\lnot\lnot\phi\to\phi$ holds intutionistically.

I will give the sketch of the proof. At first, we can prove that following formulas are provable from intutionistic logic:

1. $\lnot\lnot (\phi\to\psi)\to (\lnot\lnot\phi\to\lnot\lnot\psi)$,

2. $\lnot\lnot (\phi\land\psi)\to (\lnot\lnot\phi\land\lnot\lnot\psi)$,

3. $\lnot\lnot\lnot\phi\to \lnot\phi$.

From these results and inductive argument, you can prove the theorem.

If $p\lor q$ is equivalent to for some formula $\phi(p,q)$ which occurs only $\land$, $\to$ and $\lnot$, then from above theorem we get $$\lnot\lnot(\lnot p\lor\lnot q)\to (\lnot p\lor\lnot q).$$ However, it is not intuitionistically valid. You can check it from Heiting algebra given by open subsets of $\Bbb{R}$, taking $p=(-\infty,0)\cup(1,\infty)$ and $q=(-\infty,1)\cup(2,\infty)$.

Note that second-order intutionistic logic can define $\lor$ from second-order quantifier and $\to$ like as: $$p\lor q := [\forall r :(p\to r)\to ((q\to r)\to r)]$$

• Does the negative translation not work for $\lor$? I thought that negative formulas using any connectives work to create a submodel of classical logic inside intuitionistic logic (I think this was Godel's work). – Mario Carneiro Feb 1 '15 at 10:02
• @MarioCarneiro Double-negation translation is a interpretation of the classical logic into the intutionistic logic, not a definition of disjunction and existential quantifier. It realizes (or simulates?) classical connectives in intuitionistic logic, but it does not define the intuitionistic disjunction. – Hanul Jeon Feb 1 '15 at 10:19
• I realize that, but I was under the impression that the intuitionistic disjunction is interpretable as the classical disjunction under the negative translation. Or is the embedding more complicated than $(p\lor q)^*=(p^*\lor q^*)$? – Mario Carneiro Feb 1 '15 at 11:05
• @MarioCarneiro I wonder that you know the definition of double-negation translation. Also, I do not know well about the intuitionistic logic. Can you explain the definition of negative translation? – Hanul Jeon Feb 1 '15 at 11:17
• @Mario Carneiro: Double negation is not a Heyting algebra homomorphism in general. There are several schemes for the negative translation (see eecs.qmul.ac.uk/~pbo/papers/paper039.pdf). The scheme that just double negates atomic formulas works for conjunction and implication but not for disjunction. – Rob Arthan Feb 1 '15 at 11:20