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

References

See Also