# 13.2 Derivability

## 13.2 Derivability

Derivability is the formal relation between assumptions and conclusions. It tells us when a formula can be obtained by applying the rules of a proof system.

We write:

$$
\Gamma \vdash A
$$

to mean that $A$ is derivable from the assumptions in $\Gamma$.

Here $\Gamma$ is a collection of formulas. It may contain one formula, many formulas, or no formulas at all.

For example:

$$
p,\ p \to q \vdash q
$$

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

### Derivability from No Assumptions

When there are no assumptions, we write:

$$
\vdash A
$$

This means that $A$ is a theorem of the proof system.

For example, in ordinary propositional logic:

$$
\vdash A \to A
$$

This formula can be proved without assuming $A$ permanently.

A theorem is therefore a formula whose proof is closed. It depends only on the rules and axioms of the system.

### Derivability from Assumptions

Most mathematical reasoning begins with assumptions.

If we assume:

$$
A
$$

then we can immediately derive:

$$
A
$$

So:

$$
A \vdash A
$$

This is the identity or assumption principle.

If we assume both:

$$
A
$$

and

$$
A \to B
$$

then by modus ponens we can derive:

$$
B
$$

Therefore:

$$
A,\ A \to B \vdash B
$$

This is one of the simplest examples of derivability.

### Weakening

Weakening says that adding extra assumptions does not destroy a derivation.

If:

$$
\Gamma \vdash A
$$

then:

$$
\Gamma, B \vdash A
$$

The idea is simple. If $A$ was already derivable from $\Gamma$, then giving yourself one more assumption $B$ cannot make the old proof invalid.

Example:

$$
p \vdash p
$$

Therefore:

$$
p,\ q \vdash p
$$

The assumption $q$ is unused, but it is allowed.

### Cut

Cut expresses chaining of derivations.

If:

$$
\Gamma \vdash A
$$

and:

$$
\Delta, A \vdash B
$$

then:

$$
\Gamma, \Delta \vdash B
$$

The formula $A$ works as an intermediate result.

You can read this as: if $\Gamma$ proves $A$, and $A$ together with $\Delta$ proves $B$, then $\Gamma$ together with $\Delta$ proves $B$ directly.

Example:

$$
p \vdash p
$$

and:

$$
p,\ p \to q \vdash q
$$

So:

$$
p,\ p \to q \vdash q
$$

In larger systems, cut is important because it describes composition of proofs.

### Monotonicity

Derivability is usually monotone with respect to assumptions.

If:

$$
\Gamma \subseteq \Delta
$$

and:

$$
\Gamma \vdash A
$$

then:

$$
\Delta \vdash A
$$

This says that expanding the assumption set preserves derivability.

For ordinary classical and intuitionistic logics, monotonicity holds. In some non-classical logics, such as relevance logic or linear logic, assumptions are treated more carefully, so this property may need adjustment.

### Derived Rules

A rule is **derived** if it is not primitive, but can be justified using the primitive rules.

For example, suppose the system has conjunction elimination:

$$
\frac{A \land B}{A}
$$

and:

$$
\frac{A \land B}{B}
$$

Then from $A \land B$, we may derive $B \land A$:

$$
\frac{
\frac{A \land B}{B}
\qquad
\frac{A \land B}{A}
}{
B \land A
}
$$

using conjunction introduction.

So the rule:

$$
\frac{A \land B}{B \land A}
$$

is a derived rule.

Derived rules are useful because they shorten proofs. They do not increase the real strength of the system, since each use can be expanded into primitive steps.

### Admissible Rules

An admissible rule is a rule that preserves provability, even if it cannot always be inserted as a direct derived proof step.

A rule of the form:

$$
\frac{A}{B}
$$

is admissible if whenever $A$ is provable, $B$ is also provable.

Derived rules are admissible, but admissible rules need not be derived.

This distinction matters in proof theory, especially for systems where the shape of proofs is important.

### Derivability and Proof Search

Derivability can be read in two directions.

From top to bottom, it describes proof checking. Given a proposed derivation, we verify each step.

From bottom to top, it describes proof search. Given a goal $A$, we ask which rule could have produced it.

For example, to prove:

$$
A \land B
$$

a natural strategy is to prove $A$ and prove $B$ separately:

$$
\frac{A \qquad B}{A \land B}
$$

To prove:

$$
A \to B
$$

a natural strategy is to assume $A$ temporarily and try to prove $B$:

$$
\frac{
\begin{array}{c}
[A] \
\vdots \
B
\end{array}
}{
A \to B
}
$$

This goal-directed reading is the basis of proof assistants and automated theorem provers.

### Derivability and Semantics

Derivability is syntactic. It depends on proof rules.

Semantic consequence is written:

$$
\Gamma \models A
$$

and means that every interpretation making all formulas in $\Gamma$ true also makes $A$ true.

A good proof system connects these two relations.

Soundness says:

$$
\Gamma \vdash A \quad \Longrightarrow \quad \Gamma \models A
$$

Completeness says:

$$
\Gamma \models A \quad \Longrightarrow \quad \Gamma \vdash A
$$

Together, they show that formal derivability matches semantic consequence.