The Hilbert System is a proof system with only one rule of inference, implication elimination, in additional to three axiom schemas.
Despite its simplicity, the Hilbert system is both sound and complete. In other words, for this system, logical entailment and provability are identical.
Definition
- implication elimination (modus ponens)
Example: given
and , prove We can prove with the following steps:
premise premise A1 implication elimination: 3, 2 A2 implication elimination: 5, 4 implication elimination: 5, 4