[Math] Deduction Theorem + Modus Ponens + What = Implicational Propositional Calculus

Question

Implicational propositional calculus is a system of propositional calculus in which implication is the only logical connective, and all other connectives are defined with respect implication and a single false statement. Consider the system of implicational propositional calculus with the following two rules of inference: the Deduction Theorem, which states that if by assuming P you can conclude Q then P implies Q, and Modus Ponens, which states that if P and P implies Q then Q.

I'm guessing that this is not a complete system for the implicational propositional calculus, so my question is, what else do we need to add to make it complete? Is Peirce's Law all we need?

Any help would be greatly appreciated.

Thank You in Advance.

Answer 1

In order to verifiy if Peirce's law is sufficient, when added to Deduction Theorem and modus ponens, we can try to verify if the (complete) axiom system for propositional logic of Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997) [page 35] can be derived under these assumptions.

(A1) $\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{B})$

We have that :

$B$ 1 --- assumption

$C$ 2 --- assumption

$B$ 3 --- assumption

$C \rightarrow B$ 4 --- deduction theorem from 2 and 3

$B \rightarrow (C \rightarrow B)$ 5 --- deduction theorem from 1 and 4.

(A2) $(\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{D})) \rightarrow ((\mathcal{B} \rightarrow \mathcal{C}) \rightarrow (\mathcal{B} \rightarrow \mathcal{D}))$

We have that :

$B \rightarrow (C \rightarrow D)$ 1 --- assumption

$B \rightarrow C$ 2 --- assumption

$B$ 3 --- assumption

$C$ 4 --- modus ponens from 2 and 3

$C \rightarrow D$ 5 --- modus ponens from 1 and 3

$D$ 6 --- modus ponens from 4 and 5

$B \rightarrow D$ 7 --- deduction theorem from 3 and 6

$(B \rightarrow C) \rightarrow (B \rightarrow D)$ 8 --- deduction theorem from 2 and 7

$(B \rightarrow (C \rightarrow D)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow D))$ 9 --- deduction theorem from 1 and 8.

We still have to derive

(A3) $(\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$.

But, according to Implicational propositional calculus

the axiom system formed by (A1), (A2) and Peirce's law with the rule of inference modus ponens is semantically complete with respect to the usual two-valued semantics of classical propositional logic.

Note. Peirce's law is necessary, due to the fact that $\nvdash_{(A1)(A2)}(Peirce)$. The addition of Peirce’s law is sufficient, due to some results of Tarski and Bernays.

In order to have "full" propositional calculus, we have to add the falsum symbol ($\bot$) and an additional axiom : Ex Falso Quodlibet ($\bot \rightarrow \mathcal{A}$).