0

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?

Doug Spoonwood
  • 11,211
  • To clarify - the statement says that 'p implies q' is equivalent to 'either p is false or q is true'. –  Oct 01 '14 at 06:11
  • @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'. – Doug Spoonwood Oct 01 '14 at 16:25
  • @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. – Doug Spoonwood Oct 01 '14 at 20:46

1 Answers1

3

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.

Mauro ALLEGRANZA
  • 94,169
  • Is the equivalence of connectives the same sort of equivalence as involved in an equivalence like ECpqANpq? – Doug Spoonwood Oct 01 '14 at 16:29
  • "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.

     – Doug Spoonwood Oct 01 '14 at 21:02
  • 1
    @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$. – Mauro ALLEGRANZA Oct 02 '14 at 06:07