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?

  • 1
    $\begingroup$ 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$. $\endgroup$
    – BrianO
    Mar 5, 2016 at 22:15
  • 2
    $\begingroup$ 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)$. $\endgroup$ Mar 5, 2016 at 22:20
  • $\begingroup$ @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. $\endgroup$ Mar 5, 2016 at 22:21
  • $\begingroup$ @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. $\endgroup$ Mar 5, 2016 at 22:25

1 Answer 1


You can see Implicational propositional calculus.

Using $\bot$ to formalize "the falsum", we can define negation:

$\lnot P$ is $P \to \bot$.

In this way, we have that:

$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$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .