Calculus

logic proof-theory

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 is derivable from a set of formulas in a calculus (written ) if there exists a finite sequence of formulas ending in , where each formula is either an axiom, a premise in , or follows from previous formulas by an inference rule.

Soundness and Completeness

• Sound calculus: (Everything derived is true).
• complete calculus: (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.