In mathematical logic, a proof calculus or a proof system is built to prove statements.

Overview

A proof system includes the components:

  • Formal language: The set L of formulas admitted by the system, for example, propositional logic or first-order logic.
  • Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems.
  • Axioms: Formulas in L assumed to be valid. All theorems are derived from axioms.

A formal proof of a well-formed formula in a proof system is a set of axioms and rules of inference of the proof system that infers that the well-formed formula is a theorem of the proof system.