# Help understanding $P\land Q$ derivation in implicational propositional calculus?

According to its formulation, the implicational propositional calculus uses implication equipped with a tautologically false proposition $F$ to achieve soundness. Thus, consider the following equivalence: $$P\land Q \equiv (P\to (Q\to F))\to F$$ So:

1. $\neg (\neg P\lor (\neg Q\lor F))\lor F$
2. $(P\land \neg (\neg Q\lor F))\land F$
3. $(P\land (Q\land \neg F))\land F$

How is $F$ eliminated to finally reach the conclusion $P\land Q$? I don't see how to remove $F$ despite the observation that both $P$ and $Q$ depend upon $\neg F$. This is explicitly so for $Q$ and implicit for $P$ in the formula. But implicit is no good in a substitution system. In other words, it appears to require more axioms to be fully specified or it is using some intuitive grounds?

• Your 2nd to last line and last lines are incorrect: $A\land F\equiv F$ for any $A$. Typo, presumably? You should have $\lor$ there. You can eliminate $F$ because $A\lor F \equiv A$; similarly, $\neg F \equiv T$ and $A\land T\equiv A$. Mar 5, 2016 at 22:15
• You have to note that (using $\bot$ in place of $F$): $P \to \bot$ is $\lnot P$. Thus: $(P \to (Q \to \bot))\to \bot$ is simply: $\lnot (P \to \lnot Q)$. Mar 5, 2016 at 22:20
• @BrianO, It is of the form $\neg G\lor H \equiv \neg(G\land \neg H)$. The goal is to convert the connectives to logical-AND towards reaching the conclusion. Mar 5, 2016 at 22:21
• @MauroALLEGRANZA, superb. That's it. I take it that it is a rule of this logic's formulation? If you put that as the answer it is accepted for your credit. Mar 5, 2016 at 22:25

Using $\bot$ to formalize "the falsum", we can define negation:
$\lnot P$ is $P \to \bot$.
$P \land Q$ can be defined as $(P \to (Q \to \bot))\to \bot$.
This is simply: $\lnot (P \to \lnot Q)$, which is equivalent (in classical logic) to: $P \land Q$.