3
$\begingroup$

I'm training to prove this statement , but first I need to know if this statement can be proved in :

1 - both in classical and Intuitionistic logic ( in this case i need to provide demonstration in Intuitionistic logic )

2 - classical logic but not Intuitionistic logic ( in this case i need to provide a Kripke Counter-Models )

3 - not provable in either classic and Intuitionistic logic ( in this case i need to provide a classic Counter-Models )

My question is how to distinguish if a statement is provable in one of this cases ?

PS : I know the Intuitionistic logic doesn't allow the elimination of double negation

$ \neg ( \neg \alpha \wedge \neg \neg \alpha ) $

$\endgroup$
3
  • $\begingroup$ Related: What is a constructive proof of $\lnot\lnot(P\vee\lnot P)$? $\endgroup$
    – MJD
    Apr 26, 2015 at 7:49
  • 1
    $\begingroup$ The question is trick", because it alludes to the intuitionistically "forbidden" doble negation elimination rule; but we do not need it to see that $\lnot \alpha \land \lnot \lnot \alpha$ is a contradiction : thus, its negation must be valid. $\endgroup$ Apr 26, 2015 at 8:22
  • 1
    $\begingroup$ You can prove it in Natural Deduction assuming : 1) $¬α∧¬¬α$, deriving by $\land$-eliminartion both : 2) $¬α$ and 3) $¬¬α$ , i.e. $\lnot \alpha \to \bot$; deriving 4) $\bot$ from 2) and 3) by $\to$-elimination and finally : 5) $(¬α∧¬¬α) \to \bot$, i.e. $¬(¬α∧¬¬α)$ from 1) and 4) by $\to$-introduction. All the rules used are intuitionistically valid (no RAA, EM or Double Negation). $\endgroup$ Apr 26, 2015 at 12:04

3 Answers 3

8
$\begingroup$

This statement can be proved in minimal logic. When you rewrite the negations as implications in the usual way, the statement is $$ ((\alpha \to \bot) \land ((\alpha \to \bot) \to \bot) \to \bot $$ which is really of the form $$ (X \land X \to Y) \to Y $$ which is just a form of modus ponens. The provability of the statement has nothing to do with negation, really, apart from rewriting the negations as implications in the usual way.

$\endgroup$
1
  • 1
    $\begingroup$ @ZeRubeus As the name suggests minimal logic has fewer rules even then intuitionistic logic, and the given proof is therefore valid in both deduction systems. $\endgroup$ Apr 26, 2015 at 5:11
2
$\begingroup$

For every proposition $P$, the deduction that $P\land\lnot P\to\bot$, that is, that $\lnot(P\land\lnot P)$, is simply applying modus ponens, therefore intuitionistically valid; this is because $\lnot P$ just means $P\to\bot$. Apply this for $P=\lnot\alpha$.

$\endgroup$
0
$\begingroup$

Hint: Assume $\neg\alpha \wedge \neg\neg \alpha$, derive a contradiction. Does the resulting proof requires some use of the double negation elimation rule?

$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .