13.1 Syntax of Proofs

A proof system needs a precise notion of proof. Informally, a proof is an argument that shows why a conclusion follows. Formally, a proof is a finite object built according to fixed rules.

The syntax of proofs describes the shape of these objects.

Formulas and Judgments

A proof does not manipulate meanings directly. It manipulates formulas.

A typical formula is written:

A derivability judgment is written:

This means that $A$ is derivable from the assumptions in $\Gamma$.

Here $\Gamma$ is a set, list, or multiset of formulas, depending on the proof system. For example:

says that $q$ can be derived from $p$ and $p \to q$.

The symbol $\vdash$ belongs to the proof system. It is about formal derivability, not semantic truth.

Proofs as Sequences

In many proof systems, a proof is a finite sequence of formulas:

Each line must be justified in one of three ways:

1. It is an assumption.
2. It is an axiom.
3. It follows from earlier lines by an inference rule.

The final line is the conclusion.

For example:

The third line follows from the first two by modus ponens:

Here $A$ is $p$, and $B$ is $q$.

Proofs as Trees

Proofs may also be represented as trees. In a proof tree, premises appear above a line, and the conclusion appears below it.

For modus ponens:

This tree says that if we have a proof of $p$ and a proof of $p \to q$, then we may form a proof of $q$.

Tree notation is useful because many logical rules naturally branch.

For example, conjunction introduction has the form:

To prove $A \land B$, we must prove both $A$ and $B$.

Axioms

An axiom is a formula that may be used without proof inside the system.

Some proof systems use axiom schemas. An axiom schema describes infinitely many axioms by a pattern.

Example:

This is not one single formula. It is a schema. For any formulas $A$ and $B$, the instance is an axiom.

For example:

and

are both instances.

Axioms give the system starting points.

Assumptions

An assumption is a formula temporarily accepted for the purpose of a derivation.

If $A$ is among the assumptions, then we may write:

This is the basic assumption rule.

For example:

because $p$ is one of the assumptions.

Assumptions are important because many proofs show that a conclusion follows from given premises, rather than proving the conclusion absolutely.

Inference Rules

An inference rule tells us how to derive a new formula from formulas already obtained.

A general rule has the shape:

The formulas above the line are premises. The formula below the line is the conclusion.

The rule says: if the premises have been derived, then the conclusion may be derived.

Examples:

Modus ponens

Conjunction introduction

Conjunction elimination

and

These rules describe legal proof steps.

Derivations from Assumptions

A derivation from assumptions records which formulas are allowed at the start.

For example, from:

we can derive:

So:

A proof tree is:

using conjunction elimination.

Similarly:

by the other conjunction elimination rule.

Discharged Assumptions

Some proof systems, especially natural deduction, allow assumptions to be used temporarily and then discharged.

For implication introduction, the rule is:

This means: if assuming $A$ allows us to derive $B$, then we may conclude $A \to B$.

The assumption $A$ is discharged. It no longer remains as an open assumption after the rule is applied.

Example:

To prove:

we temporarily assume $A$:

Then $A$ follows immediately from the assumption. Therefore:

by implication introduction.

As a derivation:

Open and Closed Proofs

A proof with undischarged assumptions is an open proof.

It establishes a judgment:

A proof with no undischarged assumptions is a closed proof.

It establishes:

For example:

is a closed theorem of ordinary propositional logic.

But:

is an open derivation, because it depends on assumption $A$.

Proof Syntax Is Mechanical

The syntax of proofs is deliberately strict. Every proof step must be locally checkable.

To verify a formal proof, we do not need to understand the intended meaning of the formulas. We only check whether each line is allowed by the rules.

This mechanical nature is what makes formal proof suitable for proof assistants, automated theorem provers, and metatheory.