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:
- $\neg (\neg P\lor (\neg Q\lor F))\lor F$
- $(P\land \neg (\neg Q\lor F))\land F$
- $(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?