Calculus

logic

Definition

Calculus

A calculus (or proof system) is a formal framework consisting of a set of axioms and a set of inference rules. It provides a purely syntactic method for deriving theorems from a given set of premises.

Properties

Derivability

A formula $F$ is derivable from a set of formulas $\Gamma$ in a calculus $\mathcal{C}$ (written $\Gamma {⊢}_{\mathcal{C}}F$) if there exists a finite sequence of formulas ending in $F$, where each formula is either an axiom, a premise in $\Gamma$, or follows from previous formulas by an inference rule.

Soundness and Completeness

• Soundness: $\Gamma ⊢F⟹\Gamma \models F$ (Everything derived is true).
• Completeness: $\Gamma \models F⟹\Gamma ⊢F$ (Everything true can be derived).

Examples

Different calculi prioritise different aspects of reasoning:

• Hoare Calculus: Specialised for program verification.
• Hilbert Calculus: Uses many axioms and few rules (usually just Modus Ponens).
• Sequent Calculus: Focuses on symmetric rules for logical operators.
• Natural Deduction: Aims to mimic human reasoning styles.

Syntax vs. Semantics

A calculus allows for reasoning without considering the semantics (interpretations). A machine can check a proof in a calculus by simply matching patterns according to the rules.