Recursive function $Hyp: DER \to 2^{PROP}$ such that given a derviation in PROP the function returns the set of all its hypotheses?

Question

From Van Dalen's Logic and Structure:

Give a recursive definition of the function Hyp which assigns to each derivation D its set of hypotheses Hyp(D) (this is a bit stricter than the notion in Definition 2.4.2, since it is the smallest set of hypotheses, i.e. hypotheses without “garbage”).

With definition 2.4.2 being:

Definition 2.4.2 The relation Γ $\vdash$ φ between sets of propositions and propositions is defined as follows: there is a derivation with conclusion φ and with all (un- canceled) hypotheses in Γ . (See also Exercise 6.)

I've been trying to define this function, but don't know where to start or which angle to take this on from. Any help is greatly appreciated.

Answer 1

See Def.2.4.1, page 34, for the list of rules.

The recursive def of $\text {Hyp}(\mathcal D)$ must be:

Basis: if $\mathcal D$ is the single-node derivation with formula $\varphi$, then $\text {Hyp}(\mathcal D) = \{ \varphi \}$.

Induction step: assume that $\mathcal D_1$ and $\mathcal D_2$ are derivations with $\text {Hyp}(\mathcal D_1)$ and $\text {Hyp}(\mathcal D_2)$ respectively.

I'll consider only one example of "non-discharging" rules (the other are similar):

$(\land$-elim) : if $\varphi \land \psi$ is the last formula of $\mathcal D_1$ and $\mathcal D$ is obtained from $\mathcal D_1$ using $(\land$-elim) to add the new formula $\varphi$, then $\text {Hyp}(\mathcal D) = \text {Hyp}(\mathcal D_1)$.

$(\land$-intro) : if $\varphi$ is the last formula of $\mathcal D_1$ and $\varphi'$ is the last formula of $\mathcal D_2$ and $\mathcal D$ is obtained from $\mathcal D_1$ and $\mathcal D_2$ using $(\land$-intro) to add the new formula $\varphi \land \varphi'$, then $\text {Hyp}(\mathcal D) = \text {Hyp}(\mathcal D_1) \cup \text {Hyp}(\mathcal D_2)$.

Now for the "interesting" cases:

(EFQ) : if $\bot$ is the last formula of $\mathcal D_1$ and $\mathcal D$ is obtained from $\mathcal D_1$ using (EFQ) to add the new formula $\varphi$, then $\text {Hyp}(\mathcal D) = \text {Hyp}(\mathcal D_1)$.

($\bot$-elim) : if $\bot$ is the last formula of $\mathcal D_1$ and $\lnot \varphi \in \text {Hyp}(\mathcal D_1)$ and $\mathcal D$ is obtained from $\mathcal D_1$ using ($\bot$-elim) to add the new formula $\varphi$, then $\text {Hyp}(\mathcal D) = \text {Hyp}(\mathcal D_1) \setminus \{ \lnot \varphi \}$.

($\to$-intro) : if $\psi$ is the last formula of $\mathcal D_1$ and $\varphi \in \text {Hyp}(\mathcal D_1)$ and $\mathcal D$ is obtained from $\mathcal D_1$ using ($\to$-intro) to add the new formula $\varphi \to \psi$, then $\text {Hyp}(\mathcal D) = \text {Hyp}(\mathcal D_1) \setminus \{ \varphi \}$.