Derivations and Derivation Trees

Derivations

Definition

A derivation (or proof) that $v \in X_R$ is a finite tree where:

1. The root is labelled $v$
2. Each node is the conclusion of a rule whose premises are its children
3. Each leaf is an axiom

Intuition

A derivation shows how $v$ can be built by applying rules starting from axioms.

Derivation Trees

Structure

        v
       /|\
      / | \
    u1  u2  u3
    /|   |   \
   ...  ...  ...

• Root at top (conclusion)
• Leaves at bottom (axioms)
• Internal nodes: applications of rules

Depth and Height

• The height of a derivation is the length of the longest path from root to leaf
• The depth of a node is its distance from the root

Example: Natural Numbers

Derivation of $S(S(0))$:

    S(S(0))
       |
     S(0)
       |
      0

Reading

1. $0 \in \mathbb{N}$ (axiom)
2. $S(0) \in \mathbb{N}$ (by successor rule from 0)
3. $S(S(0)) \in \mathbb{N}$ (by successor rule from $S(0)$)

Example: Binary Trees

Derivation of $\text{Node}(\text{Leaf}, \text{Node}(\text{Leaf}, \text{Leaf}))$:

        Node(Leaf, Node(Leaf, Leaf))
              /              \
          Leaf          Node(Leaf, Leaf)
                          /        \
                       Leaf        Leaf

The Set of Derivable Elements

Definition

$X_R \subseteq X$ is the set of elements that have a derivation using rules $R$.

Key Theorem

$X_R = \bigcap \{S \subseteq X : S \text{ closed under } R\}$

The set of derivable elements equals the smallest closed set.

Types of Rules

Axioms (0-premise rules)

$\frac{}{a}$

Elements derived in one step.

Unary Rules (1-premise)

$\frac{u}{v}$

If $u$ derivable, so is $v$.

Binary Rules (2-premises)

$\frac{u_1 \quad u_2}{v}$

If both $u_1$ and $u_2$ derivable, so is $v$.

n-ary Rules

$\frac{u_1 \quad u_2 \quad \cdots \quad u_n}{v}$

Reasoning About Derivations

By Induction on Derivation Height

To prove $\forall v \in X_R. P(v)$:

1. Base: Prove $P(a)$ for every axiom $a$
2. Step: For each rule $\frac{u_1, \ldots, u_n}{v}$, assume $P(u_1), \ldots, P(u_n)$ and prove $P(v)$

This is a powerful proof technique that mirrors the structure of derivations.

Example: Balanced Strings

Rules for $\{w \in \{a, b\}^* : |w|_a = |w|_b\}$:

$\frac{}{\varepsilon} \qquad \frac{w}{awb} \qquad \frac{w}{bwa} \qquad \frac{u \quad v}{uv}$

Claim: All derivable strings have equal numbers of $a$‘s and $b$‘s.

Proof by induction on derivations:

• Base: $\varepsilon$ has $0$ $a$‘s and $0$ $b$‘s.
• If $w$ balances, so do $awb$ and $bwa$.
• If $u$ and $v$ balance, so does $uv$ (sums add).

---

Summary

• A derivation is a finite tree with axioms at leaves and rule applications at internal nodes
• $X_R$ = set of elements with a derivation
• Induction on derivation height: base case for axioms, step case for each rule