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 '15 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$ – Mauro ALLEGRANZA Apr 26 '15 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$ – Mauro ALLEGRANZA Apr 26 '15 at 12:04
7
$\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$ – Marc van Leeuwen Apr 26 '15 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

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.