The implicational propositional calculus is
semantically complete with respect to the usual two-valued semantics of classical propositional logic. That is, if Γ is a set of implicational formulas, and
A is an implicational formula
entailed by Γ, then \Gamma\vdash A.
Proof A proof of the completeness theorem is outlined below. First, using the
compactness theorem and the deduction theorem, we may reduce the completeness theorem to its special case with empty Γ, i.e., we only need to show that every tautology is derivable in the system. The proof is similar to completeness of full propositional logic, but it also uses the following idea to overcome the functional incompleteness of implication. If
A and
F are formulas, then is equivalent to where
A* is the result of replacing in
A all, some, or none of the occurrences of
F by falsity. Similarly, is equivalent to So under some conditions, one can use them as substitutes for saying
A* is false or
A* is true respectively. We first observe some basic facts about derivability: ::Indeed, we can derive
A → (
B →
C) using Axiom 1, and then derive
A →
C by modus ponens (twice) from Ax. 2. ::This follows from () by the deduction theorem. ::If we further assume
C →
B, we can derive using (), then we derive
C by modus ponens. This shows A\to C,(A\to B)\to C,C\to B\vdash C, and the deduction theorem gives A\to C,(A\to B)\to C\vdash(C\to B)\to C. We apply Ax. 3 to obtain (). Let
F be an arbitrary fixed formula. For any formula
A, we define and Consider only formulas in propositional variables
p1, ...,
pn. We claim that for every formula
A in these variables and every
truth assignment e, {{NumBlk|:|p_1^{e(p_1)},\dots,p_n^{e(p_n)}\vdash A^{e(A)}.|}} We prove () by induction on
A. The base case
A =
pi is trivial. Let We distinguish three cases: •
e(
C) = 1. Then also
e(
A) = 1. We have • ::(C\to F)\to F\vdash((B\to C)\to F)\to F • :by applying () twice to the axiom Since we have derived by the induction hypothesis, we can infer •
e(
B) = 0. Then again
e(
A) = 1. The deduction theorem applied to () gives • ::B\to F\vdash((B\to C)\to F)\to F. • :Since we have derived by the induction hypothesis, we can infer •
e(
B) = 1 and
e(
C) = 0. Then
e(
A) = 0. We have • ::\begin{align}(B\to F)\to F,C\to F,B\to C&\vdash B\to F&&\text{by (1)}\\&\vdash F&&\text{by modus ponens,}\end{align} • :thus (B\to F)\to F,C\to F\vdash(B\to C)\to F by the deduction theorem. We have derived and by the induction hypothesis, hence we can infer This completes the proof of (). Now let
F be a tautology in variables
p1, ...,
pn. We will prove by reverse induction on
k =
n,...,0 that for every assignment
e, {{NumBlk|:|p_1^{e(p_1)},\dots,p_k^{e(p_k)}\vdash F.|}} The base case
k =
n follows from a special case of () using : F^{e(F)} = F^1 = ((F \to F) \to F) and the fact that
F→
F is a theorem by the deduction theorem. Assume that () holds for
k + 1, we will show it for
k. By applying deduction theorem to the induction hypothesis, we obtain :\begin{align}p_1^{e(p_1)},\dots,p_k^{e(p_k)}&\vdash(p_{k+1}\to F)\to F,\\ p_1^{e(p_1)},\dots,p_k^{e(p_k)}&\vdash((p_{k+1}\to F)\to F)\to F,\end{align} by first setting
e(
pk+1) = 0 and second setting
e(
pk+1) = 1. From this we derive () using modus ponens. For
k = 0 we obtain that the tautology
F is provable without assumptions. This is what was to be proved. This proof is constructive. That is, given a tautology, one could actually follow the instructions and create a proof of it from the axioms. However, the length of such a proof increases exponentially with the number of propositional variables in the tautology, hence it is not a practical method for any but the very shortest tautologies. == The Bernays–Tarski axiom system ==