When talking with a mathematics teacher the other day, we discussed these axioms in the context of proving tautologies with semantic tableaux:
- $(p\to(q\to p))$
- $((p\to(q\to r))\to((p\to q)\to(p\to r)))$
- $((\lnot p\to\lnot q)\to(q\to p))$
We wondered if it was possible to show that $\neg(\neg A) \rightarrow A$ from these axioms (along with MP), but it did not seem obvious how to do so and yet this fact is not included as an axiom. Is it provable from the axioms or is this fact simply unprovable in this version of PL?