Inmathematical logic, theimplicational propositional calculus is a version ofclassicalpropositional calculus that uses only oneconnective, calledimplication or conditional. Informulas, thisbinary operation is indicated by "implies", "if ..., then ...", "→", "${\displaystyle \to }$", etc..

Implication alone is notfunctionally complete as alogical operator because one cannot form all othertwo-valuedtruth functions from it.

For example, the two-place truth function that always returnsfalse is not definable from → and arbitrary propositional variables: any formula constructed from → and propositional variables must receive the valuetrue when all of its variables are evaluated to true.It follows that {→} is not functionally complete.

However, if one adds a nullary connective ⊥ for falsity, then one can define all other truth functions. Formulas over the resulting set of connectives {→, ⊥} are calledf-implicational.^[1] IfP andQ are propositions, then:

• ¬P isequivalent toP → ⊥
• P ∧Q is equivalent to (P → (Q → ⊥)) → ⊥
• P ∨Q is equivalent to (P →Q) →Q
• P ↔Q is equivalent to ((P →Q) → ((Q →P) → ⊥)) → ⊥

Since the above operators are known to be functionally complete, it follows that any truth function can be expressed in terms of → and ⊥.

The following statements are consideredtautologies (irreducible and intuitively true, by definition).

• Axiom schema 1 isP → (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 non-nullaryrule of inference (modus ponens) is: fromP andP →Q inferQ.

Where in each case,P,Q, andR may be replaced by any formulas that contain only "→" as a connective. If${\displaystyle \mathrm{\Gamma }}$ is a set of formulas andA a formula, then${\displaystyle \mathrm{\Gamma }⊢A}$ means thatA is derivable using the axioms and rules above and formulas from${\displaystyle \mathrm{\Gamma }}$ as additional hypotheses.

Łukasiewicz (1948) found an axiom system for the implicational calculus that 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.^[2]

Since all axioms and rules of the calculus are schemata, derivation is closed undersubstitution:

If${\displaystyle \mathrm{\Gamma }⊢A,}$ then${\displaystyle \sigma (\mathrm{\Gamma })⊢\sigma (A),}$

where σ is any substitution (of formulas using only implication).

The implicational propositional calculus also satisfies thededuction theorem:

If${\displaystyle \mathrm{\Gamma },A⊢B}$, then${\displaystyle \mathrm{\Gamma }⊢A\to B.}$

As explained in thededuction theorem article, this holds for any axiomatic extension of the system containing axiom schemas 1 and 2 above and modus ponens.

The implicational propositional calculus issemantically complete with respect to the usual two-valued semantics of classical propositional logic. That is, if Γ is a set of implicational formulas, andA is an implicational formulaentailed by Γ, then${\displaystyle \mathrm{\Gamma }⊢A}$.

A proof of the completeness theorem is outlined below. First, using thecompactness 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. IfA andF are formulas, thenA →F is equivalent to(¬A*) ∨F, whereA* is the result of replacing inA all, some, or none of the occurrences ofF by falsity. Similarly,(A →F) →F is equivalent toA* ∨F. So under some conditions, one can use them as substitutes for sayingA* is false orA* is true respectively.

We first observe some basic facts about derivability:

${\displaystyle A\to B,B\to C⊢A\to C}$

1

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

${\displaystyle A\to B⊢(B\to C)\to (A\to C)}$

2

This follows from (1) by the deduction theorem.

${\displaystyle A\to C,(A\to B)\to C⊢C}$

3

If we further assumeC →B, we can deriveA →B using (1), then we deriveC by modus ponens. This shows${\displaystyle A\to C,(A\to B)\to C,C\to B⊢C}$, and the deduction theorem gives${\displaystyle A\to C,(A\to B)\to C⊢(C\to B)\to C}$. We apply Ax. 3 to obtain (3).

LetF be an arbitrary fixed formula. For any formulaA, we defineA⁰ = (A →F) andA¹ = ((A →F) →F). Consider only formulas in propositional variablesp₁, ...,p_n. We claim that for every formulaA in these variables and everytruth assignmente,

${\displaystyle p_1^{e(p_1)},\dots ,p_n^{e(p_n)}⊢A^{e(A)}.}$

4

We prove (4) by induction onA. The base caseA =p_i is trivial. LetA = (B →C). We distinguish three cases:

1. e(C) = 1. Then alsoe(A) = 1. We have

   ${\displaystyle (C\to F)\to F⊢((B\to C)\to F)\to F}$

   by applying (2) twice to the axiomC → (B →C). Since we have derived(C →F) →F by the induction hypothesis, we can infer((B →C) →F) →F.

2. e(B) = 0. Then againe(A) = 1. The deduction theorem applied to (3) gives

   ${\displaystyle B\to F⊢((B\to C)\to F)\to F.}$

   Since we have derivedB →F by the induction hypothesis, we can infer((B →C) →F) →F.

3. e(B) = 1 ande(C) = 0. Thene(A) = 0. We have

   

   thus${\displaystyle (B\to F)\to F,C\to F⊢(B\to C)\to F}$ by the deduction theorem. We have derived(B →F) →F andC →F by the induction hypothesis, hence we can infer(B →C) →F. This completes the proof of (4).

Now letF be a tautology in variablesp₁, ...,p_n. We will prove by reverse induction onk =n,...,0 that for every assignmente,

${\displaystyle p_1^{e(p_1)},\dots ,p_k^{e(p_k)}⊢F.}$

5

The base casek =n follows from a special case of (4) using

${\displaystyle F^{e(F)}=F^1=((F\to F)\to F)}$

and the fact thatF→F is a theorem by the deduction theorem.

Assume that (5) holds fork + 1, we will show it fork. By applying deduction theorem to the induction hypothesis, we obtain

by first settinge(p_k+1) = 0 and second settinge(p_k+1) = 1. From this we derive (5) using modus ponens.

Fork = 0 we obtain that the tautologyF 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 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 calledhypothetical syllogism.This makes derivation of the deduction meta-theorem a little more difficult, but it can still be done.

We show that fromP→(Q→R) andP→Q one can deriveP→R. This fact can be used in lieu of axiom schema 2 to get the meta-theorem.

1. P→(Q→R) given
2. P→Q given
3. (P→Q)→((Q→R)→(P→R)) ax 2'
4. (Q→R)→(P→R) mp 2,3
5. (P→(Q→R))→(((Q→R)→(P→R))→(P→(P→R))) ax 2'
6. ((Q→R)→(P→R))→(P→(P→R)) mp 1,5
7. P→(P→R) mp 4,6
8. (P→(P→R))→(((P→R)→R)→(P→R)) ax 2'
9. ((P→R)→R)→(P→R) mp 7,8
10. (((P→R)→R)→(P→R))→(P→R) ax 3
11. P→R mp 9,10 qed

Satisfiability in the implicational propositional calculus is trivial, because every formula is satisfiable: just set all variables to true.

Falsifiability in the implicational propositional calculus isNP-complete,^[3] meaning that validity (tautology) isco-NP-complete.

In this case, a useful technique is to presume that the formula is not a tautology and attempt to find a valuation that makes it false. If one succeeds, then it is indeed not a tautology. If one fails, then it is a tautology.

Example of a non-tautology:

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; andE is false.

SinceD is true,C→D is true. So the truth ofF→((C→D)→E) is equivalent to the truth ofF→E.

Then sinceE is false andF→E is true, we get thatF is false.

SinceA→F is true,A is false. ThusA→B is true and (C→A)→E is true.

C→A is false, soC is true.

The value ofB does not matter, so we can arbitrarily choose it to be true.

Summing up, the valuation that setsB,C andD to be true andA,E andF 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; andA is false.

SinceA is false,A→B is true. SoC is true. ThusA must be true, contradicting the fact that it is false.

Thus there is no valuation that makes ((A→B)→C)→((C→A)→(D→A)) false. Consequently, it is a tautology.

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 numbern there will still be theorems that cannot be proved inn 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 thatA is a theorem of the extended system. Then all one has to do to prove any formula is to replaceA by the desired formula throughout the proof ofA. This proof will have the same number of steps as the proof ofA.

The axioms listed above primarily work through the deduction metatheorem to arrive at completeness. Here is another axiom system that aims directly at completeness without going through the deduction metatheorem.

First we have axiom schemas that are designed to efficiently prove the subset of tautologies that contain only onepropositional 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) that 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 Φ that may containA,B,C₁, ...,C_nand ends withA as its final conclusion. Then we take

• aa 5: Φ₋→(Φ₊→ꞈΦ)

as an axiom schema where Φ₋ is the result of replacingB byA throughout Φ and Φ₊ is the result of replacingB 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 bothA andB) 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 whenB is false Φ₋ and the case whenB is true Φ₊.

If the variable that 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 ifA is true, then Φ, Φ₋, Φ₊ and Φ₋→(Φ₊→Φ) are all true. Sowithout loss of generality, we may assume thatA is false. Notice that Φ is a tautologyif and only if both Φ₋ and Φ₊ are tautologies. But while Φ hasn+2 distinct variables, Φ₋ and Φ₊ both haven+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 whetherB is false or true.

Examples:

Deriving Peirce's law

1. [((P→P)→P)→P]→([((P→(P→P))→P)→P]→[((P→Q)→P)→P]) aa 5
2. P→P aa 1
3. (P→P)→((P→P)→(((P→P)→P)→P)) aa 3
4. (P→P)→(((P→P)→P)→P) mp 2,3
5. ((P→P)→P)→P mp 2,4
6. [((P→(P→P))→P)→P]→[((P→Q)→P)→P] mp 5,1
7. P→(P→P) aa 4
8. (P→(P→P))→((P→P)→(((P→(P→P))→P)→P)) aa 3
9. (P→P)→(((P→(P→P))→P)→P) mp 7,8
10. ((P→(P→P))→P)→P mp 2,9
11. ((P→Q)→P)→P mp 10,6 qed

Deriving Łukasiewicz' sole axiom

1. [((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
2. [((P→P)→P)→((P→P)→(S→P))]→([((P→(P→P))→P)→((P→P)→(S→P))]→[((P→Q)→P)→((P→P)→(S→P))]) aa 5
3. P→(S→P) aa 4
4. (P→(S→P))→(P→((P→P)→(S→P))) aa 2
5. P→((P→P)→(S→P)) mp 3,4
6. P→P aa 1
7. (P→P)→((P→((P→P)→(S→P)))→[((P→P)→P)→((P→P)→(S→P))]) aa 3
8. (P→((P→P)→(S→P)))→[((P→P)→P)→((P→P)→(S→P))] mp 6,7
9. ((P→P)→P)→((P→P)→(S→P)) mp 5,8
10. [((P→(P→P))→P)→((P→P)→(S→P))]→[((P→Q)→P)→((P→P)→(S→P))] mp 9,2
11. P→(P→P) aa 4
12. (P→(P→P))→((P→((P→P)→(S→P)))→[((P→(P→P))→P)→((P→P)→(S→P))]) aa 3
13. (P→((P→P)→(S→P)))→[((P→(P→P))→P)→((P→P)→(S→P))] mp 11,12
14. ((P→(P→P))→P)→((P→P)→(S→P)) mp 5,13
15. ((P→Q)→P)→((P→P)→(S→P)) mp 14,10
16. [((P→Q)→(P→P))→(((P→P)→P)→(S→P))]→[((P→Q)→R)→((R→P)→(S→P))] mp 15,1
17. (P→P)→((P→(S→P))→[((P→P)→P)→(S→P)]) aa 3
18. (P→(S→P))→[((P→P)→P)→(S→P)] mp 6,17
19. ((P→P)→P)→(S→P) mp 3,18
20. (((P→P)→P)→(S→P))→[((P→Q)→(P→P))→(((P→P)→P)→(S→P))] aa 4
21. ((P→Q)→(P→P))→(((P→P)→P)→(S→P)) mp 19,20
22. ((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⁴ cases since it contains 4 distinct variables. In this derivation, we were able to restrict consideration to merely 3 cases:R is false andQ is false,R is false andQ is true, andR is true. However because we are working within the formal system of logic (instead of outside it, informally), each case required much more effort.

• Deduction theorem
• List of logic systems § Implicational propositional calculus
• Peirce's law
• Propositional calculus
• Tautology (logic)
• Truth table
• Valuation (logic)

• Mendelson, Elliot (1997)Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall.

• Systems of formal logic
• Propositional calculus
• Conditionals

• CS1: long volume value
• Articles with short description
• Short description is different from Wikidata
• Articles containing proofs