In mathematical logic, the implicational propositional calculus is a version of classical propositional calculus that uses only one connective, called implication or conditional. In formulas, this binary operation is indicated by "implies", "if ..., then ...", "→", " → {\displaystyle \rightarrow } ", etc..
Functional (in)completeness Implication alone is not functionally complete as a logical operator because one cannot form all other two-valued truth functions from it. For example, the two-place truth function that always returns false is not definable from → and arbitrary propositional variables: any formula constructed from → and propositional variables must receive the value true 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 called f-implicational. If P and Q are propositions, then:
¬P is equivalent to P → ⊥ 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 ⊥.
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 non-nullary 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 that contain only "→" as a connective. If Γ {\displaystyle \Gamma } is a set of formulas and A a formula, then Γ ⊢ A {\displaystyle \Gamma \vdash A} means that A is derivable using the axioms and rules above and formulas from Γ {\displaystyle \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.
Basic properties of derivation Since all axioms and rules of the calculus are schemata, derivation is closed under substitution:
If Γ ⊢ A , {\displaystyle \Gamma \vdash A,} then σ ( Γ ) ⊢ σ ( A ) , {\displaystyle \sigma (\Gamma )\vdash \sigma (A),}
where σ is any substitution (of formulas using only implication). The implicational propositional calculus also satisfies the deduction theorem:
If Γ , A ⊢ B {\displaystyle \Gamma ,A\vdash B} , then Γ ⊢ A → B . {\displaystyle \Gamma \vdash A\to B.}
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 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 Γ ⊢ A {\displaystyle \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 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:
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 (1) by the deduction theorem.
If we further assume C → B, we can derive A → B using (1), then we derive C by modus ponens. This shows A → C , ( A → B ) → C , C → B ⊢ C {\displaystyle A\to C,(A\to B)\to C,C\to B\vdash C} , and the deduction theorem gives A → C , ( A → B ) → C ⊢ ( C → B ) → C {\displaystyle A\to C,(A\to B)\to C\vdash (C\to B)\to C} . We apply Ax. 3 to obtain (3). Let F be an arbitrary fixed formula. For any formula A, we define A0 = (A → F) and A1 = ((A → F) → F). Consider only formulas in propositional variables p1, ..., pn. We claim that for every formula A in these variables and every truth assignment e,
We prove (4) by induction on A. The base case A = pi is trivial. Let A = (B → C). We distinguish three cases:
e(C) = 1. Then also e(A) = 1. We have
( C → F ) → F ⊢ ( ( B → C ) → F ) → F {\displaystyle (C\to F)\to F\vdash ((B\to C)\to F)\to F}
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
… excerpt ends here. Continue reading the full article.
