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?

  • $\begingroup$ To clarify - the statement says that 'p implies q' is equivalent to 'either p is false or q is true'. $\endgroup$ – user117644 Oct 1 '14 at 6:11
  • $\begingroup$ @mistermarko No, it doesn't say that. 'either p is false or q is true' says that 'either the valuation of p is false or the valuation of q is true'. 'p implies q' doesn't say anything about the valuations of 'p' and 'q'. $\endgroup$ – Doug Spoonwood Oct 1 '14 at 16:25
  • $\begingroup$ @Silenttiffy If you're going to try and change what I've written in Polish/Lukasiewicz notation, I request that you put them into a form which is a formula (or equivalently well-formed formula) in some formal language. You did not do so. I don't object to answers which use informal schematics. I have learned that I can learn a lot by reading such answers, and don't object to informal notation as I once did. However, when I see someone changing what I have written as I did, I become worried that the concept of rigor and a formal language has gotten lost. $\endgroup$ – Doug Spoonwood Oct 1 '14 at 20:46

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)$.


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.

  • $\begingroup$ Is the equivalence of connectives the same sort of equivalence as involved in an equivalence like ECpqANpq? $\endgroup$ – Doug Spoonwood Oct 1 '14 at 16:29
  • $\begingroup$ "4) ⊥ --- from 2) and 3) by modus ponens (→-E)" So, I guess with FALSE and NOT2', you can get there using modus ponens. I like how the weak law of identity (p$\rightarrow$p) got used as a minor premise. I have found it oftentimes useful in formal proofs, and it pops up in computer-generated proofs a fair amount of the time. The old prejudice against it as a useful theorem/axiom, totally misses it's use as a minor premise, even when there is no deduction theorem around. $\endgroup$ – Doug Spoonwood Oct 1 '14 at 21:02
  • 1
    $\begingroup$ @DougSpoonwood - about 4) : I've used the abbreviation : $\lnot p$ is $p \rightarrow \bot$. Thus, form 3) $p$ and 2) $p \rightarrow \bot$ by mp we get : 4) $\bot$. $\endgroup$ – Mauro ALLEGRANZA Oct 2 '14 at 6:07

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.