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


if it is true, otherwise


  • $\begingroup$ 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)$? $\endgroup$ – barak manos Feb 1 '15 at 6:38
  • $\begingroup$ 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. $\endgroup$ – MarnixKlooster ReinstateMonica Feb 1 '15 at 6:56
  • 2
    $\begingroup$ 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). $\endgroup$ – Mario Carneiro Feb 1 '15 at 7:14
  • 1
    $\begingroup$ @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)$. $\endgroup$ – Hanul Jeon Feb 1 '15 at 7:34
  • 1
    $\begingroup$ @barakmanos Sorry, but there is no finite-valued faithful interpretation of intuitionistic logic. (See the part of the wiki article about Heyting algebras.) $\endgroup$ – 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)]$$

  • $\begingroup$ 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). $\endgroup$ – Mario Carneiro Feb 1 '15 at 10:02
  • $\begingroup$ @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. $\endgroup$ – Hanul Jeon Feb 1 '15 at 10:19
  • $\begingroup$ 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^*)$? $\endgroup$ – Mario Carneiro Feb 1 '15 at 11:05
  • $\begingroup$ @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? $\endgroup$ – Hanul Jeon Feb 1 '15 at 11:17
  • 2
    $\begingroup$ @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. $\endgroup$ – Rob Arthan Feb 1 '15 at 11:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.