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:

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:

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

Derivability from No Assumptions

When there are no assumptions, we write:

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

For example, in ordinary propositional logic:

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:

then we can immediately derive:

So:

This is the identity or assumption principle.

If we assume both:

and

then by modus ponens we can derive:

Therefore:

This is one of the simplest examples of derivability.

Weakening

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

If:

then:

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:

Therefore:

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

Cut

Cut expresses chaining of derivations.

If:

and:

then:

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:

and:

So:

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

Monotonicity

Derivability is usually monotone with respect to assumptions.

If:

and:

then:

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:

and:

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

using conjunction introduction.

So the rule:

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:

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 natural strategy is to prove $A$ and prove $B$ separately:

To prove:

a natural strategy is to assume $A$ temporarily and try to prove $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:

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:

Completeness says:

Together, they show that formal derivability matches semantic consequence.