Implicational propositional calculus
In mathematical logic, the implicational propositional calculus is a version of classical propositional calculus which uses only one connective, called implication or conditional. In formulas, this binary operation is indicated by "implies", "if ..., then ...", "→", "", etc..
Virtual completeness as an operator
Implication alone is not functionally complete as a logical operator because one cannot form all other twovalued truth functions from it. However, if one has a propositional formula which is known to be false and uses that as if it were a nullary connective for falsity, then one can define all other truth functions. So implication is virtually complete as an operator. If P,Q, and F are propositions and F is known to be false, then:
 ¬P is equivalent to P → F
 P ∧ Q is equivalent to (P → (Q → F)) → F
 P ∨ Q is equivalent to (P → Q) → Q
 P ↔ Q is equivalent to ((P → Q) → ((Q → P) → F)) → F
More generally, since the above operators are known to be functionally complete, it follows that any truth function can be expressed in terms of "→" and "F", if we have a proposition F which is known to be false.
It is worth noting that F is not definable from → and arbitrary sentence variables: any formula constructed from → and propositional variables must receive the value true when all of its variables are evaluated to true. It follows as a corollary that {→} is not functionally complete. It cannot, for example, be used to define the twoplace truth function that always returns false.
Axiom system
The following statements are considered tautologies (irreducible and intuitively true, by definition).
 Axiom schema 1 is P → (Q → P).
 Axiom schema 2 is (P → (Q → R)) → ((P → Q) → (P → R)).
 Axiom schema 3 (Peirce's law) is ((P → Q) → P) → P.
 The one nonnullary rule of inference (modus ponens) is: from P and P → Q infer Q.
Where in each case, P, Q, and R may be replaced by any formulas which contain only "→" as a connective. If Γ is a set of formulas and A a formula, then means that A is derivable using the axioms and rules above and formulas from Γ as additional hypotheses.
Łukasiewicz (1948) found an axiom system for the implicational calculus, which replaces the schemas 1–3 above with a single schema
 ((P → Q) → R) → ((R → P) → (S → P)).
He also argued that there is no shorter axiom system.
Basic properties of derivation
Since all axioms and rules of the calculus are schemata, derivation is closed under substitution:
 If then
where σ is any substitution (of formulas using only implication).
The implicational propositional calculus also satisfies the deduction theorem:
 If , then
As explained in the deduction theorem article, this holds for any axiomatic extension of the system containing axiom schemas 1 and 2 above and modus ponens.
Completeness
The implicational propositional calculus is semantically complete with respect to the usual twovalued semantics of classical propositional logic. That is, if Γ is a set of implicational formulas, and A is an implicational formula entailed by Γ, then .
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 A → F is equivalent to (¬A*) ∨ F, where A* is the result of replacing in A all, some, or none of the occurrences of F by falsity. Similarly, (A → F) → F is equivalent to A* ∨ F. 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:

(1)
 Indeed, we can derive A → (B → C) using Axiom 1, and then derive A → C by modus ponens (twice) from Ax. 2.

(2)
 This follows from (1) by the deduction theorem.

(3)
 If we further assume C → B, we can derive A → B using (1), then we derive C by modus ponens. This shows , and the deduction theorem gives . We apply Ax. 3 to obtain (3).
Let F be an arbitrary fixed formula. For any formula A, we define A^{0} = (A → F) and A^{1} = ((A → F) → F). Let us consider only formulas in propositional variables p_{1}, ..., p_{n}. We claim that for every formula A in these variables and every truth assignment e,

(4)
We prove (4) by induction on A. The base case A = p_{i} is trivial. Let A = (B → C). We distinguish three cases:
 e(C) = 1. Then also e(A) = 1. We have
 by applying (2) twice to the axiom C → (B → C). Since we have derived (C → F) → F by the induction hypothesis, we can infer ((B → C) → F) → F.
 e(B) = 0. Then again e(A) = 1. The deduction theorem applied to (3) gives
 Since we have derived B → F by the induction hypothesis, we can infer ((B → C) → F) → F.
 e(B) = 1 and e(C) = 0. Then e(A) = 0. We have
 thus by the deduction theorem. We have derived (B → F) → F and C → F by the induction hypothesis, hence we can infer (B → C) → F. This completes the proof of (4).
Now let A be a tautology in variables p_{1}, ..., p_{n}. We will prove by reverse induction on k = n,...,0 that for every assignment e,

(5)
The base case k = n is a special case of (4). Assume that (5) holds for k + 1, we will show it for k. By applying deduction theorem to the induction hypothesis, we obtain
by first setting e(p_{k+1}) = 0 and second setting e(p_{k+1}) = 1. From this we derive (5) using (3).
For k = 0 we obtain that the formula A^{1}, i.e., (A → F) → F, is provable without assumptions. Recall that F was an arbitrary formula, thus we can choose F = A, which gives us provability of the formula (A → A) → A. Since A → A is provable by the deduction theorem, we can infer A.
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
The Bernays–Tarski axiom system is often used. In particular, Łukasiewicz's paper derives the Bernays–Tarski axioms from Łukasiewicz's sole axiom as a means of showing its completeness.
It differs from the axiom schemas above by replacing axiom schema 2, (P→(Q→R))→((P→Q)→(P→R)), with
 Axiom schema 2': (P→Q)→((Q→R)→(P→R))
which is called hypothetical syllogism. This makes derivation of the deduction metatheorem a little more difficult, but it can still be done.
We show that from P→(Q→R) and P→Q one can derive P→R. This fact can be used in lieu of axiom schema 2 to get the metatheorem.
 P→(Q→R) given
 P→Q given
 (P→Q)→((Q→R)→(P→R)) ax 2'
 (Q→R)→(P→R) mp 2,3
 (P→(Q→R))→(((Q→R)→(P→R))→(P→(P→R))) ax 2'
 ((Q→R)→(P→R))→(P→(P→R)) mp 1,5
 P→(P→R) mp 4,6
 (P→(P→R))→(((P→R)→R)→(P→R)) ax 2'
 ((P→R)→R)→(P→R) mp 7,8
 (((P→R)→R)→(P→R))→(P→R) ax 3
 P→R mp 9,10 qed
Testing whether a formula of the implicational propositional calculus is a tautology
In this case, a useful technique is to presume that the formula is not a tautology and attempt to find a valuation which makes it false. If one succeeds, then it is indeed not a tautology. If one fails, then it is a tautology.
Example of a nontautology:
Suppose [(A→B)→((C→A)→E)]→([F→((C→D)→E)]→[(A→F)→(D→E)]) is false.
Then (A→B)→((C→A)→E) is true; F→((C→D)→E) is true; A→F is true; D is true; and E is false.
Since D is true, C→D is true. So the truth of F→((C→D)→E) is equivalent to the truth of F→E.
Then since E is false and F→E is true, we get that F is false.
Since A→F is true, A is false. Thus A→B is true and (C→A)→E is true.
C→A is false, so C is true.
The value of B does not matter, so we can arbitrarily choose it to be true.
Summing up, the valuation which sets B, C and D to be true and A, E and F to be false will make [(A→B)→((C→A)→E)]→([F→((C→D)→E)]→[(A→F)→(D→E)]) false. So it is not a tautology.
Example of a tautology:
Suppose ((A→B)→C)→((C→A)→(D→A)) is false.
Then (A→B)→C is true; C→A is true; D is true; and A is false.
Since A is false, A→B is true. So C is true. Thus A must be true, contradicting the fact that it is false.
Thus there is no valuation which makes ((A→B)→C)→((C→A)→(D→A)) false. Consequently, it is a tautology.
Adding an axiom schema
What would happen if another axiom schema were added to those listed above? There are two cases: (1) it is a tautology; or (2) it is not a tautology.
If it is a tautology, then the set of theorems remains the set of tautologies as before. However, in some cases it may be possible to find significantly shorter proofs for theorems. Nevertheless, the minimum length of proofs of theorems will remain unbounded, that is, for any natural number n there will still be theorems which cannot be proved in n or fewer steps.
If the new axiom schema is not a tautology, then every formula becomes a theorem (which makes the concept of a theorem useless in this case). What is more, there is then an upper bound on the minimum length of a proof of every formula, because there is a common method for proving every formula. For example, suppose the new axiom schema were ((B→C)→C)→B. Then ((A→(A→A))→(A→A))→A is an instance (one of the new axioms) and also not a tautology. But [((A→(A→A))→(A→A))→A]→A is a tautology and thus a theorem due to the old axioms (using the completeness result above). Applying modus ponens, we get that A is a theorem of the extended system. Then all one has to do to prove any formula is to replace A by the desired formula throughout the proof of A. This proof will have the same number of steps as the proof of A.
An alternative axiomatization
The axioms listed above primarily work through the deduction metatheorem to arrive at completeness. Here is another axiom system which aims directly at completeness without going through the deduction metatheorem.
First we have axiom schemas which are designed to efficiently prove the subset of tautologies which contain only one propositional variable.
 aa 1: ꞈA→A
 aa 2: (A→B)→ꞈ(A→(C→B))
 aa 3: A→((B→C)→ꞈ((A→B)→C))
 aa 4: A→ꞈ(B→A)
The proof of each such tautology would begin with two parts (hypothesis and conclusion) which are the same. Then insert additional hypotheses between them. Then insert additional tautological hypotheses (which are true even when the sole variable is false) into the original hypothesis. Then add more hypotheses outside (on the left). This procedure will quickly give every tautology containing only one variable. (The symbol "ꞈ" in each axiom schema indicates where the conclusion used in the completeness proof begins. It is merely a comment, not a part of the formula.)
Consider any formula Φ which may contain A, B, C_{1}, ..., C_{n} and ends with A as its final conclusion. Then we take
 aa 5: Φ_{−}→(Φ_{+}→ꞈΦ)
as an axiom schema where Φ_{−} is the result of replacing B by A throughout Φ and Φ_{+} is the result of replacing B by (A→A) throughout Φ. This is a schema for axiom schemas since there are two level of substitution: in the first Φ is substituted (with variations); in the second, any of the variables (including both A and B) may be replaced by arbitrary formulas of the implicational propositional calculus. This schema allows one to prove tautologies with more than one variable by considering the case when B is false Φ_{−} and the case when B is true Φ_{+}.
If the variable which is the final conclusion of a formula takes the value true, then the whole formula takes the value true regardless of the values of the other variables. Consequently if A is true, then Φ, Φ_{−}, Φ_{+} and Φ_{−}→(Φ_{+}→Φ) are all true. So without loss of generality, we may assume that A is false. Notice that Φ is a tautology if and only if both Φ_{−} and Φ_{+} are tautologies. But while Φ has n+2 distinct variables, Φ_{−} and Φ_{+} both have n+1. So the question of whether a formula is a tautology has been reduced to the question of whether certain formulas with one variable each are all tautologies. Also notice that Φ_{−}→(Φ_{+}→Φ) is a tautology regardless of whether Φ is, because if Φ is false then either Φ_{−} or Φ_{+} will be false depending on whether B is false or true.
Examples:
Deriving Peirce's law
 [((P→P)→P)→P]→([((P→(P→P))→P)→P]→[((P→Q)→P)→P]) aa 5
 P→P aa 1
 (P→P)→((P→P)→(((P→P)→P)→P)) aa 3
 (P→P)→(((P→P)→P)→P) mp 2,3
 ((P→P)→P)→P mp 2,4
 [((P→(P→P))→P)→P]→[((P→Q)→P)→P] mp 5,1
 P→(P→P) aa 4
 (P→(P→P))→((P→P)→(((P→(P→P))→P)→P)) aa 3
 (P→P)→(((P→(P→P))→P)→P) mp 7,8
 ((P→(P→P))→P)→P mp 2,9
 ((P→Q)→P)→P mp 10,6 qed
Deriving Łukasiewicz' sole axiom
 [((P→Q)→P)→((P→P)→(S→P))]→([((P→Q)→(P→P))→(((P→P)→P)→(S→P))]→[((P→Q)→R)→((R→P)→(S→P))]) aa 5
 [((P→P)→P)→((P→P)→(S→P))]→([((P→(P→P))→P)→((P→P)→(S→P))]→[((P→Q)→P)→((P→P)→(S→P))]) aa 5
 P→(S→P) aa 4
 (P→(S→P))→(P→((P→P)→(S→P))) aa 2
 P→((P→P)→(S→P)) mp 3,4
 P→P aa 1
 (P→P)→((P→((P→P)→(S→P)))→[((P→P)→P)→((P→P)→(S→P))]) aa 3
 (P→((P→P)→(S→P)))→[((P→P)→P)→((P→P)→(S→P))] mp 6,7
 ((P→P)→P)→((P→P)→(S→P)) mp 5,8
 [((P→(P→P))→P)→((P→P)→(S→P))]→[((P→Q)→P)→((P→P)→(S→P))] mp 9,2
 P→(P→P) aa 4
 (P→(P→P))→((P→((P→P)→(S→P)))→[((P→(P→P))→P)→((P→P)→(S→P))]) aa 3
 (P→((P→P)→(S→P)))→[((P→(P→P))→P)→((P→P)→(S→P))] mp 11,12
 ((P→(P→P))→P)→((P→P)→(S→P)) mp 5,13
 ((P→Q)→P)→((P→P)→(S→P)) mp 14,10
 [((P→Q)→(P→P))→(((P→P)→P)→(S→P))]→[((P→Q)→R)→((R→P)→(S→P))] mp 15,1
 (P→P)→((P→(S→P))→[((P→P)→P)→(S→P)]) aa 3
 (P→(S→P))→[((P→P)→P)→(S→P)] mp 6,17
 ((P→P)→P)→(S→P) mp 3,18
 (((P→P)→P)→(S→P))→[((P→Q)→(P→P))→(((P→P)→P)→(S→P))] aa 4
 ((P→Q)→(P→P))→(((P→P)→P)→(S→P)) mp 19,20
 ((P→Q)→R)→((R→P)→(S→P)) mp 21,16 qed
Using a truth table to verify Łukasiewicz' sole axiom would require consideration of 16=2^{4} cases since it contains 4 distinct variables. In this derivation, we were able to restrict consideration to merely 3 cases: R is false and Q is false, R is false and Q is true, and R is true. However because we are working within the formal system of logic (instead of outside it, informally), each case required much more effort.
See also
 Deduction theorem
 List of logic systems#Implicational propositional calculus
 Peirce's law
 Propositional calculus
 Tautology (logic)
 Truth table
 Valuation (logic)
References
 Mendelson, Elliot (1997) Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall.
 Łukasiewicz, Jan (1948) The shortest axiom of the implicational calculus of propositions, Proc. Royal Irish Academy, vol. 52, sec. A, no. 3, pp. 25–33.