Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

**Assignment 9**

I’m having trouble proving the third formula in 9.2.

Is it allowed to transform logically equivalent formulas? In my case I’d like to make notA and not(A=>B) contradict, as, A=>B HAS to be true by its definition via or…

If that’s not allowed (which I kinda assume), any hints how to deal with this syntactically?

No; the exercise is explicitly to use natural deduction

Even those definitions don’t matter in the context of natural deduction, since you have specific rules for implications - and it’s almost always easier to use those directly rather than go via the definitions (which in addition are somewhat arbitrary anyway, since you can define almost any connective in terms of almost any others…)

The good thing about natural deduction is that there’s almost always pretty much only „one way“ to go about things. For example, to prove an implication ((P=>Q)=>P)=>P, pretty much the only thing you *can* do is to *assume* (P=>Q)=>P and derive P from that. And of yourse you may always assume the opposite of what you’re trying to prove (e.g. P) and try to derive a contradiction (and using FALSE-elimination on that)…

Well “easier” is a strong word xD The proof just got 5 times more voluminous on paper :'D Your hint has been helpful though!

As my calculus professor used to say:

„If you don’t succeed - don’t try harder, try the opposite!“