Can ECpqANpq get proved in intuitionistic logic?

Question

I use Lukasiewicz/Polish notation. Given intuitionistic logic with the optional axioms for equivalence and negation given in the Wikipedia, can

ECpqANpq or in other notation

[(p$\rightarrow$q)=($\lnot$p$\lor$q)] get proved in intuitionistic logic?

Answer 1

NO; in intuitionistic logic the "basic" connectives are independent.

See Jan von Plato, Elements of Logical Reasoning (2013), page 59 :

Independence of the connectives. We have seen that there are connections between the connectives, such as the derivable implications $A \land B \rightarrow ¬(¬A \lor ¬B), A \lor B \rightarrow ¬(¬A \land ¬B)$, and $(A \rightarrow B) \rightarrow ¬(A \land ¬B)$. It can be shown that none of the converse implications is derivable in intuitionistic logic. Further similar results show the following:

Independence of the connectives in intuitionistic logic. None of the connectives can be expressed equivalently by the remaining ones.

See also page 75 for an example regarding : $\nvdash ¬(¬ A \land ¬ B ) \rightarrow A \lor B$.

---

Regarding specifically the question about $(p → q) \leftrightarrow (¬p \lor q)$ we have :

$\vdash (¬p \lor q) \rightarrow (p → q)$

while :

$\nvdash (p → q) \rightarrow (¬p \lor q)$.

Assuming $(p → q) \rightarrow (¬p \lor q)$, by substitution we get : $(p → p) \rightarrow (¬p \lor p)$.

But $\vdash p \rightarrow p$; thus by modus ponens we were able to prove the intitionistically invalid :

$(¬p \lor p)$.

---

Note

For $\vdash (¬p \lor q) \rightarrow (p → q)$ :

1) $\lnot p \lor q$ --- assumed [a]

2) $\lnot p$ --- assumed [b] (it is the abbreviation for : $p \rightarrow \bot$)

3) $p$ --- assumed [c]

4) $\bot$ --- from 2) and 3) by modus ponens ($\rightarrow$-E)

5) $q$ --- from 4) by $\bot$-E

6) $p \rightarrow q$ --- from 3) and 5) by $\rightarrow$-I, discharging [c]

7) $q$ --- assumed [d]

8) $p \rightarrow q$ --- from 7) by $\rightarrow$-I

9) $p \rightarrow q$ --- from 8), 7), 6), 2) and 1), by $\lor$-E, discharging [b] and [d]

10) $(¬p \lor q) \rightarrow (p → q)$ --- from 9) and 1), by $\rightarrow$-I.