3
$\begingroup$

If I have a rule for negation introduction...

Rule (NegationIntroduction,ProofByNegation)
  Premises
    P=>Q, P=>⌐Q
  Conclusion
    ⌐P

...then it seems to me that I can derive the rule for double negation introduction:

Rule (DoubleNegationIntroduction)
  Premises
    P
  Conclusion
    ⌐⌐P
  Proof
    Suppose
      ⌐P
    Hence
      P
    ⌐P=>P

    Suppose
      ⌐P
    Hence
      ⌐P
    ⌐P=>⌐P

    ⌐⌐P by NegationIntroduction

There are two places where I can see that the reasoning might be faulty. Firstly, the assumption $⌐P$ when $P$ is given as a premise. However, can you not assume anything for the purposes of an argument even if the contrary is known to be true? Secondly, the resulting implication $⌐P=>P$. However, I know that intuitionistically as well as classically we have $A=>(C=>A)$. I have read Propositional Logic - Can you Derive $C \to A$ from $A$ alone, given the introduction rule? for example, so I'm pretty sure that this is okay.

$\endgroup$
1
  • $\begingroup$ The derivation of the rule about halfway down the page here en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/… suggests this derivation is fine. In particular, they use the same 'trick' as me, namely repeating the outer premise to derive the implication $⌐P=>P$. The contrasting implication $⌐P=>⌐P$ is not derived, however I assume the rule for negation introduction that they employ is simpler. This is not intuitionistic logic, but I think that at least in this case the principles are the same. $\endgroup$ Jun 15, 2016 at 13:41

1 Answer 1

5
$\begingroup$

Yes, $A\to \neg \neg A$ is intuitionistically valid, and your proof looks correct.

Many presentations of intuitionistic logic consider $\neg A$ to be an abbreviation for $A\to \bot$, and in that case $A\to\neg\neg A$ is $$ A\to((A\to\bot)\to \bot)$$ which is just an instance of the generally valid $$ A\to((A\to B)\to B) $$

$\endgroup$
2
  • $\begingroup$ Many thanks, good to get that one cleared up. $\endgroup$ Jun 15, 2016 at 14:27
  • $\begingroup$ If Np abbreviates Cp0, then CCpNqCCpqNp is an instance of CCpCqrCCpqCpr. $\endgroup$ Jun 15, 2016 at 16:11

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.