Formal Proof Systems — Mathematics Knowledge System

Overview

A formal proof system consists of a formal language, a set of axioms (formulas assumed true without proof), and a set of inference rules that license deriving new formulas from previous ones purely by syntactic pattern-matching, with no appeal to meaning. A formal proof (or derivation) of a formula φ is a finite sequence of formulas ending in φ, where each formula is either an axiom or follows from earlier formulas by an inference rule; if such a derivation exists we write ⊢ φ ('φ is a theorem' or 'φ is provable'). Common formal proof systems include Hilbert-style systems (few inference rules, many axiom schemas), natural deduction (many introduction/elimination rules, few or no axioms), and sequent calculus, all of which can be shown to prove exactly the same theorems for a given logic despite looking very different. The central achievement of proof theory is separating this syntactic notion of provability (⊢) from the semantic notion of truth in a model (⊨), a distinction made precise by the soundness and completeness theorems.

Intuition

A formal proof system is like a board game with a fixed starting position (the axioms) and a fixed set of legal moves (the inference rules) — a proof is simply a sequence of legal moves that ends at the position you wanted to reach, and crucially, checking whether a proposed proof is valid never requires understanding what the symbols 'mean,' only whether each step obeys the rules syntactically. This is exactly what makes formal proofs mechanically checkable (and eventually, computer-verifiable): the game is purely about symbol manipulation, and it's only afterward, via a separate semantic theory, that we connect 'reachable in this game' (⊢) to 'true in every intended interpretation' (⊨).

Formal Definition

Definition

A formal proof system is a triple (language, axioms, inference rules). Its core notions:

\Gamma \vdash \varphi \quad \text{('} \varphi \text{ is derivable from the set of premises } \Gamma \text{')}

Syntactic derivability

\text{Modus Ponens: from } \varphi \text{ and } \varphi \rightarrow \psi, \text{ infer } \psi

Canonical inference rule

\vdash \varphi \quad \text{('} \varphi \text{ is a theorem, provable from no premises but the axioms')}

Theoremhood

\text{A proof of } \varphi \text{ is a finite sequence } \varphi_1, \dots, \varphi_n = \varphi

Formal derivation

Worked Examples

List the premises as the first lines of the derivation.
$1.\ p \quad \text{(premise)}$
Second premise.
$2.\ p \rightarrow q \quad \text{(premise)}$
Apply modus ponens to lines 1 and 2.
$3.\ q \quad \text{(modus ponens, 1, 2)}$

Answer: {p, p → q} ⊢ q, a 3-line formal derivation.

Practice Problems

Difficulty 2/10

In natural deduction, what inference rule lets you go from a proof of φ and a proof of ψ to a proof of φ ∧ ψ?

Difficulty 3/10

Distinguish the symbols ⊢ and ⊨ and state which one belongs to proof theory versus model theory.

Difficulty 4/10

Explain why formal proof systems are designed to be purely syntactic (no reference to meaning) rather than semantic.

Quiz

Summary

A formal proof system consists of a language, axioms, and inference rules; a proof is a finite sequence of formulas each justified syntactically.
Hilbert-style systems, natural deduction, and sequent calculus are different-looking but (for the same logic) equally powerful proof systems.
Formal derivability (⊢) is a syntactic notion, distinct from semantic truth (⊨); relating the two is the job of the soundness and completeness theorems.

References

WebsiteWikipedia — Formal system