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.
The following statements are considered tautologies (irreducible and intuitively true, by definition).
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 that replaces the schemas 1–3 above with a single schema He also argued that there is no shorter axiom system.
The implicational propositional calculus also satisfies the deduction theorem: 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.
The proof is similar to completeness of full propositional logic, but it also uses the following idea to overcome the functional incompleteness of implication.
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: Let F be an arbitrary fixed formula.
We claim that for every formula A in these variables and every truth assignment e, We prove (4) by induction on A.
Falsifiability in the implicational propositional calculus is NP-complete,[3] meaning that validity (tautology) is co-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.
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).
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 one propositional variable.
Then insert additional tautological hypotheses (which are true even when the sole variable is false) into the original hypothesis.
(The symbol "ꞈ" in each axiom schema indicates where the conclusion used in the completeness proof begins.
Consider any formula Φ that may contain A, B, C1, ..., Cn and ends with A as its final conclusion.
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.
Examples: Deriving Peirce's law Deriving Łukasiewicz' sole axiom Using a truth table to verify Łukasiewicz' sole axiom would require consideration of 16=24 cases since it contains 4 distinct variables.
However because we are working within the formal system of logic (instead of outside it, informally), each case required much more effort.