Axiomatic Proof of Conjunction Introduction

I need to give an axiomatic proof from $\{\psi, \phi\}$ to $\neg(\phi\rightarrow\neg\psi)$.

I can use the deduction theorem, axioms PL1, PL2 and PL3 (I have also established that $\vdash P\rightarrow P, \vdash (\neg P \rightarrow P) \rightarrow P, \neg\neg P \vdash P)$ and the rules of Weakening, The MP Technique, Transitivity, Cut Elimination, Contraposition, Principle of Explosion, Negated Condition and Excluded Middle.

I'm stuck at a very long line of conditions that I got from a combination of Weakening, Contraposition and the schema of the results I've already proven. I'm having a hard time either getting a contradiction so that I can use the P.O.E. to get my result.

Does anyone have tips or advice about how to proceed? Maybe I should use the axioms more?

• Which contraposition rule are you allowed to use, exactly? The proof may be easier or harder depending on which rule you have available. Oct 15 '17 at 18:08
• I'm now sure what you mean by "which," but I am allowed to infer from $\phi\rightarrow\psi$ that $\neg\psi\rightarrow\neg\phi$ and infer the converse. Oct 15 '17 at 20:33
• In some more basic systems of propositional logic, you're allowed to infer $\phi \to \psi$ from $\neg \psi \to \neg \phi$ but not the converse. You can derive contraposition going the other way, but it's fiddly; but if you're allowed to go both ways then that is useful. Oct 15 '17 at 20:35

Exactly what your proof will look like will depend on which inference rules you have access to. My best advice would be to proceed in three steps:

1. Taking $\phi$, $\psi$ and $\phi \to \neg \psi$ as premises, can you arrive at a contradiction such as $\neg (\chi \to \chi)$? For this you will need modus ponens and your principle of explosion.

2. Now that you know that $\phi$, $\psi$ and $\phi \to \neg \psi$ lead to a contradiction, can you use this derive $(\phi \to \neg \psi) \to \neg (\chi \to \chi)$ from $\phi$ and $\psi$? This is much easier if you are able to use the deduction theorem, which I notice you didn't explicitly say you could use. If you don't have the deduction theorem, this part is trickier, but it's possible to do it using the PL1 and PL2 axioms.

3. Can you turn your proof of $(\phi \to \neg \psi) \to \neg (\chi \to \chi)$ into a proof of $\neg (\phi \to \neg \psi)$? For this you will need your contraposition rule (or PL3) and potentially the double-negation rule you derived earlier. Your proof of $\vdash P \to P$ and modus ponens is likely to come in handy for the last step.

This isn't a complete answer, but should hopefully be enough of a hint that you can fill the rest of the bits in.

• Thank you so much; I do, though, have a question. Why is it the case that you are giving yourself three premises? I thought that my premise set could only consist in two WFFs. Also, is it the case that the meta logical symbols in my premise set can stand for ANY WFFs? Oct 15 '17 at 20:37
• To your first question: this is what is useful about the deduction theorem (if you are allowed to use it). The deduction theorem says that if you have a proof of $\psi$ from a set of premises (say $\Gamma$ plus $\phi$), you can also derive $\phi \to \psi$ from $\Gamma$ alone. This gives a useful strategy for constructing proofs: turn a complicated proof with few premises into a simpler proof with more premises. If you're not allowed to use the deduction theorem, this whole proof is much fiddlier; I can give further hints if needed. Oct 15 '17 at 20:42
• To your second question: the metalogical symbols in your premise set can indeed stand for any well-formed formulae, but they have to stand for the same ones that they stand for in the conclusion. So the sentence which your premise $\phi$ stands for has to be the same as the $\phi$ in $\neg (\phi \to \neg \psi)$. What you will end up producing is not technically a proof but a proof scheme: you will show that for any well-formed formulae $\phi$ and $\psi$, you can derive $\neg (\phi \to \neg \psi)$ from the set ${\phi, \psi}$. Oct 15 '17 at 20:44
• I absolutely can use the deduction theorem. However, I'm still not seeing how that helps. Given the DT, since I know that my goal follows from $\phi$ and $\psi$ does it mean that I know that my goal follows from some set of premises that DOESNT involve $\phi$ or $\psi$? Oct 15 '17 at 20:47
• The deduction theorem is strange at first. As an example, suppose you need to prove that $\emptyset \vdash P \to P$, i.e. you can derive $P \to P$ from no premises at all. The deduction theorem helps you: you have a proof that ${P} \vdash P$ (which is trivial, since $P$ is premise and conclusion), and by applying the deduction theorem you now know that $\emptyset \vdash P \to P$. The deduction theorem lets you change your goal (from a $\phi \to \psi$ to just $\psi$) while also giving you $\phi$ as a premise. Oct 15 '17 at 21:07