What a Proof Is, Formally

Q: What is a formal proof

A formal proof is a derivation (a sequence of rule applications, or a proof tree) that starts from axioms and applies inference rules finitely many times to reach the target formula. Each step must follow from previous ones by the rules, and its correctness can be confirmed without considering the meaning of the formulas, by the shape of the symbols alone. Unlike an everyday 'convincing explanation,' the checking procedure is fully fixed.

Q: How do axioms and inference rules differ

An axiom is a formula accepted unconditionally as a starting point of a proof; an inference rule is a rewriting rule that says 'from formulas already derived you may form a new one.' A proof is the path from axioms, applying inference rules, to the conclusion, and which axioms and rules are accepted determines the system.

Q: Why is it important that a proof can be checked mechanically

If a proof can be checked by the shape of its symbols alone, that check can be entrusted to a small program (a proof checker). Even if finding a proof is hard, verifying that a given proof is correct is a simple matching task. This asymmetry — hard to find, easy to verify — is the basis for the trustworthiness of proof assistants and formal verification.

From a convincing explanation to a checkable derivation

Introduction (high school to first-year university)

Goal of this page

Redefine the everyday word "proof" formally, as a derivation from axioms and inference rules. Understand that a proof's correctness can be checked mechanically by the shape of the symbols alone, without considering meaning, and why this matters.

1. Everyday proofs and formal proofs

The proofs written in a math class are prose: "because of this, then this, therefore this." That is an explanation meant to convince the reader, and how finely to write it is left to the writer's judgment. Convenient, but with no mechanical standard for "is it really correct?"

In mathematical logic, to remove this vagueness, a proof is fully formalized. Every step is filled in using only predetermined axioms and inference rules, allowing no omissions. What results is a formal proof.

2. Proof as a derivation

Definition: formal proof (derivation)

A formal proof of a formula $A$ is a finite sequence of formulas $A_1, A_2, \dots, A_n$ (with $A_n = A$) such that each $A_i$ is one of: (1) an axiom, (2) obtained by applying an inference rule to formulas $A_j, A_k\ (j,k < i)$ already appearing, or (3) a formula placed as an assumption.

The $\Gamma \vdash A$ from Syntax and Semantics means exactly that "under the assumptions $\Gamma$, a formal proof of $A$ exists." A proof is no longer prose but a symbol string arranged according to the rules.

The same thing is clearer drawn as a tree rather than a sequence. Representing each rule application as a branch gives a proof tree: axioms and assumptions at the leaves, the conclusion at the root.

Figure 1: A schematic proof tree. Each horizontal line is one application of an inference rule, deriving the conclusion below from the premises above. Correctness is confirmed by checking that each line matches a rule.

3. The idea of proof checking

The greatest advantage of a formal proof is that its correctness can be confirmed mechanically. For each step of the proof sequence, you just check in turn "is this an axiom?" and "is this obtained by applying a rule to a previous one?" You never ask what the formulas mean.

Hard to find, easy to verify

Finding a proof is generally hard and demands human ingenuity and trial and error. But verifying that a given proof is correct is a simple task: just matching against the rules. This asymmetry is why a proof can be checked by a computer.

This "checking is simple" property leads to the core of later chapters: separate the part that generates proofs (humans, or clever but untrusted programs) from a small program that checks them, and trust only the checker. This is the idea of the LCF architecture and the de Bruijn criterion / TCB, and the basis for proof assistants' trustworthiness.

4. The chosen rules determine the system

A formal proof is relative to "axioms and inference rules." Which formulas are axioms and which rules are allowed changes the set of derivable formulas. For example, whether the law of excluded middle $A \lor \neg A$ is accepted as an axiom separates classical from intuitionistic logic (intuitionistic vs. classical).

The answer to "what is a proof?" ultimately reduces to "on which foundation (axioms and rules) do we build the derivation?" In the next chapter we take a bird's-eye view of the striking correspondence that logic and computation share the same structure (Curry–Howard), and step one further into the nature of proof.

Summary

Key points

Formal proof: a derivation (sequence or tree) reaching the conclusion by applying inference rules finitely from axioms
$\Gamma \vdash A$ = "under $\Gamma$, a formal proof of $A$ exists"
Correctness is checked mechanically by the shape of the symbols alone, ignoring meaning
The "hard to find, easy to verify" asymmetry is the basis for machine checking
Which axioms and rules are accepted determines the system (classical / intuitionistic, etc.)

Frequently asked questions

What is a formal proof?

A derivation (a sequence of rule applications, or a proof tree) that starts from axioms and applies inference rules finitely many times to reach the target formula. Each step must follow by the rules, and correctness can be confirmed by the shape of the symbols alone. Unlike an everyday "convincing explanation," the checking procedure is fully fixed.

How do axioms and inference rules differ?

An axiom is a formula accepted unconditionally as a starting point; an inference rule is a rewriting rule saying "from formulas already derived you may form a new one." A proof is the path from axioms, applying rules, to the conclusion, and which axioms and rules are accepted determines the system.

Why is it important that a proof can be checked mechanically?

If checkable by the shape of its symbols alone, the check can be entrusted to a small program (a proof checker). Even if finding a proof is hard, verifying a given proof is a simple matching task. This "hard to find, easy to verify" asymmetry is the basis for the trustworthiness of proof assistants and formal verification.