Axiomatic derivation of conditional from biconditional

I'm trying to do a proof which, it turns out, would work if I could prove:

$$\phi \leftrightarrow \psi \vdash \phi \rightarrow \psi$$

But I'm at a complete loss how to get there. I wonder if anyone get offer any pointers? I'm allowed the three basic axioms:

$$(A1) \hspace{1cm} \phi \rightarrow (\psi \rightarrow \phi)\$$

$$(A2) \hspace{1cm} \phi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))\$$

$$(A3) \hspace{1cm}(\neg \phi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \phi)$$

NOTE: We are viewing the biconditional here as an abbreviation for:

$$\neg ((\phi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \phi))$$

And any other rules that can be derived from these (but the less the better, really)

I know I ought to tell you what I've tried, but really I've just fiddled around with the first two axioms to see if I could get anything that would allow me to drop the antecedent and get with Modus Ponens, but I've arrived at nothing that is worth mentioning.

• What's your definition of $\leftrightarrow$? Nov 2, 2022 at 18:12
• It will be defined in terms of $\neg$ and $\rightarrow$ since those two are together expressively complete. But for the purposes of this proof we can just view it as a symbol Nov 3, 2022 at 9:47
• we can't just view it as a symbol because none of the axioms use that symbol. Nov 3, 2022 at 11:13
• I'm very sorry, you're quite right. Too long staring at $\phi$s and $\psi$s can give you brain fog. We are defining the biconditional this way: $\neg ((\phi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \phi))$ Nov 3, 2022 at 11:43
• If you could solve it just using the first two axioms, then you could also come up with a definition for the biconditional that did not involve $\lnot$. The fact that you cannot should indicate that the biconditional requires the special property of $\lnot$, which is A3. Nov 3, 2022 at 16:29

Throughout my answer, I will regard $$\rightarrow$$ as right-associative. This cuts down on the number of parentheses substantially, and means that e.g. $$A \rightarrow B \rightarrow C$$ stands for $$A \rightarrow (B \rightarrow C)$$. Similarly, $$(A \rightarrow B) \rightarrow C \rightarrow D$$ stands for $$(A \rightarrow B) \rightarrow (C \rightarrow D)$$. However, I do include some of the unnecessary parentheses when I think they substantially help comprehension.

Since $$\neg (P \rightarrow \neg Q)$$ is the definition of the conjunction $$P \wedge Q$$ in the classical Hilbert system, you're really defining your biconditional as $$(\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)$$. So we only need to derive $$(P \wedge Q) \rightarrow P$$ in our Hilbert system, and the required result involving the biconditional will follow immediately by substituting $$\varphi \rightarrow \psi$$ in place of $$P$$ (and $$\psi \rightarrow \varphi$$ in place of $$Q$$).

We can expand the definition of $$\wedge$$ in $$(P \wedge Q) \rightarrow P$$ to arrive at $$\neg(P \rightarrow \neg Q) \rightarrow P$$. Deriving this will be our goal.

For the rest of the exercise, we will require two standard lemmata, and we will repeatedly employ a well-known trick. The trick is that whenever you have a derivation of $$A \rightarrow B$$, you can get a derivation of $$(C \rightarrow A) \rightarrow (C \rightarrow B)$$ as follows.

1. $$A \rightarrow B$$ (by assumption)
2. $$(A \rightarrow B) \rightarrow C \rightarrow (A \rightarrow B)$$ (an instance of A1)
3. $$C \rightarrow A \rightarrow B$$ (modus ponens from 1,2)
4. $$(C \rightarrow A \rightarrow B) \rightarrow (C \rightarrow A) \rightarrow (C \rightarrow B)$$ (an instance of A2)
5. $$(C \rightarrow A) \rightarrow C \rightarrow B$$ (modus ponens from 3,4)

Using this trick will keep our proofs fairly short. You'll have to be familiar with the trick anyway, since you'll eventually need to use it in the proof of the deduction theorem.

The first standard lemma we'll need is double-negation introduction, that is $$\vdash A \rightarrow \neg\neg A$$. You should try to prove this yourself, but if you get stuck, you can read a solution here.

The second standard lemma we'll need is the so-called principle of explosion, $$\vdash \neg A \rightarrow (A \rightarrow B)$$. This one's surprisingly hard to find here, so I'll just write down a proof for you:

1. $$(\neg B \rightarrow \neg A) \rightarrow A \rightarrow B$$ (an instance of A3)
2. $$(\neg A \rightarrow \neg B \rightarrow \neg A) \rightarrow (\neg A \rightarrow A \rightarrow B)$$ (by the trick)
3. $$\neg A \rightarrow \neg B \rightarrow \neg A$$ (an instance of A1)
4. $$\neg A \rightarrow A \rightarrow B$$ (modus ponens from 3,2)

Now, we have all the tools we need to reach our goal! We can argue as follows:

1. $$(P \rightarrow \neg Q) \rightarrow \neg\neg (P \rightarrow \neg Q)$$ (by 1st lemma)
2. $$(\neg P \rightarrow P \rightarrow \neg Q) \rightarrow \neg P \rightarrow \neg\neg (P \rightarrow \neg Q)$$ (by the trick)
3. $$\neg P \rightarrow P \rightarrow \neg Q$$ (by 2nd lemma)
4. $$\neg P \rightarrow \neg\neg (P \rightarrow \neg Q)$$ (modus ponens from 3,2)
5. $$(\neg P \rightarrow \neg\neg (P \rightarrow \neg Q)) \rightarrow \neg (P \rightarrow \neg Q) \rightarrow P$$ (an instance of A3)
6. $$\neg (P \rightarrow \neg Q) \rightarrow P$$ (modus ponens from 4,5)
• Thank you so much for your comprehensive answer, this is an excellent explanation and proof. Nov 6, 2022 at 2:02
• Z.A.K thank you so much for this. This answer is a model for insightful answers on stack exchange that support people in stepping up their knowledge. I have a quick question about the proof: why do you call that principle the principle of explosion? I thought the principle of explosion was just ex falso quodlibet (i.e. $\phi$, $\neg$ $\phi$ $\vdash$ $\psi$) Nov 6, 2022 at 13:54
• @DanÖz: Precisely, and these two are the same principle! You can prove $A,\neg A \vdash B$ using my version as follows: 1. $A$, 2. $\neg A$, 3.$\neg A \rightarrow (A\rightarrow B)$ [explosion], 4. $A \rightarrow B$ [MP2,3], 5. $B$ [MP1,4].. You can also go the other way as well, and prove my version from yours, once you have the $\rightarrow_I$ rule. Nov 6, 2022 at 21:00