Order of discharging assumptions in natural deduction

Question

Is there a mechanical rule for the order in which assumptions can be discharged?

Consider this proof tree:

It first discharges $y$ and then $x$. Discharging $y$ first gives a proof for $C$, so discharging $x$ first would not actually be allowed because it proves $C$ on an assumption in which $C$ occurs, I guess? Like so:

(edit: fixed last row of second tree)

But that is just a semantic consideration, so are there mechanical rules for the order of discharging? And if not, how do you make sure the order of discharging you do is valid?

Answer 1

We can write these proofs as terms in a lambda calculus. This connection between the (simply typed) lambda calculus and natural deduction (for intuitionistic propositional logic) is the archetypal example of the Curry-Howard correspondence. If you're not familiar with the lambda calculus, then for this purpose all you need to know is that an expression like $\lambda x\!:\!A.f(x)$ is similar to $x \mapsto f(x)$.

There's a one-to-one correspondence between the rules of inference and operations in the lambda calculus. Your first derivation can be written as the lambda term: $$\lambda x\!:\!(A\Rightarrow B\Rightarrow C).\lambda y\!:\!(A\land B).x(\pi_1(y))(\pi_2(y))$$ and your second derivation can be written as the lambda term: $$\lambda y\!:\!(A\land B).\lambda x\!:\!(A\Rightarrow B\Rightarrow C).x(\pi_1(y))(\pi_2(y))$$ The types of these lambda terms correspond to the theorems they prove: $$(A \Rightarrow B \Rightarrow C) \Rightarrow (A \land B) \Rightarrow C \quad \text{and}\quad(A \land B) \Rightarrow (A \Rightarrow B \Rightarrow C) \Rightarrow C$$ respectively. These are different theorems. Changing the order you discharge assumptions, i.e. changing the order of the lambda abstractions, gives you a different proof and usually a proof of a different theorem. (It can be the same theorem if the variables have the same type, e.g. $\lambda x\!:\!A.\lambda y\!:\!A.(\dots).$) However, since we can prove $(A\Rightarrow B\Rightarrow C)\equiv(B\Rightarrow A\Rightarrow C)$, a proof with one order of discharging assumptions can be turned into a proof with a different order. In particular, let $\mathtt{flip}_{A,B,C}$ be the lambda term $$\lambda f\!:\!(A\Rightarrow B\Rightarrow C).\lambda y\!:\!B.\lambda x\!:\!A.f(x)(y)$$ which corresponds to a derivation of the theorem $(A\Rightarrow B\Rightarrow C)\Rightarrow (B\Rightarrow A\Rightarrow C)$. An equivalent (in a sense I'll explain) proof to your second proof is the following: $$\mathtt{flip}_{A \Rightarrow B\Rightarrow C,A\land B, C}(\lambda x\!:\!(A\Rightarrow B\Rightarrow C).\lambda y\!:\!(A\land B).x(\pi_1(y))(\pi_2(y)))$$ This is just the proof of the first theorem with $\mathtt{flip}$ applied to it to turn it into a proof of the second theorem. However, this proof (once the definition of $\mathtt{flip}$ is inlined) contains "detours" in the proof. We have rewrite rules for derivations that simplify them, and these correspond to the rewrite rules in the lambda calculus. For example, the core $\beta$-rule of the lambda calculus looks like: $(\lambda x\!:\!A.t_1))(t_2)\leadsto t_1[t_2/x]$ where $t_i$ is an arbitrary lambda term and $t_1[t_2/x]$ stands for substituting $t_2$ for each $x$ in $t_1$. This corresponds to the following rewrite rule for derivations:$$\cfrac{\cfrac{\cfrac{\cfrac{[x:A]}{\mathcal{D}_1}}{B}}{A\Rightarrow B}\Rightarrow I,x\qquad \cfrac{\mathcal{D}_2}{A}}{B}\Rightarrow E \quad \leadsto \quad \cfrac{\cfrac{\cfrac{\mathcal{D}_2}{A}}{\mathcal{D}_1}}{B}$$ where $\cfrac{\mathcal{D}}{A}$ represents an arbitrary (potentially open) derivation ending in $A$ and the intent is that $\cfrac{\mathcal{D}_2}{A}$ replaces all occurrences of the $x$ labelled assumptions above $\mathcal{D}_1$. There can be more than one despite the limitations of the notation.

If we apply the above rewrite rule, we'd find that the proof using $\mathtt{flip}$ actually rewrites into the first proof of the second theorem. If you're gung-ho, you can draw out the derivation that represents the proof using $\mathtt{flip}$ and apply the rewrite rule on derivations above until you get the second derivation you presented. In this case, $\mathcal{D}_1$ will be the derivation of $\mathtt{flip}$ and $\mathcal{D}_2$ will be your first derivation. However, after applying the rewrite rule once, you'll see that it can be applied again (and one more time after that). However, it is not the case that all derivations of the same proof rewrite to each other. There can be multiple distinct derivations even modulo the equivalence relation induced by the rewrite rules. These correspond to the potential multiple normal form terms of a given type in the lambda calculus.

Answer 2

I think I have found the answer to my question myself:

The order in which assumptions are discharged is irrelevant. Assumption are all put together in a big conjunction. Say we have deduced a proposition $c$ with our assumptions $x_1$ to $x_n$. Then we have

\begin{align*} \left(\bigwedge_{i=1}^n x_i\right) \implies c \end{align*}

We can now manipulate this term as follows

\begin{align*} & \left(\bigwedge_{i=1}^n x_i\right) \implies c\\ \iff & \lnot \left(\bigwedge_{i=1}^n x_i\right) \lor c\\ \iff & \left( \bigvee_{i=1}^n \lnot x_i\right) \lor c \end{align*}

At this point we can continue like so:

\begin{align*} & \left( \bigvee_{i=1}^n \lnot x_i\right) \lor c\\ \iff & \left( \bigvee_{i=1}^{n-1} \lnot x_i\right) \lor \lnot x_n \lor c\\ \iff & \left( \bigvee_{i=1}^{n-1} \lnot x_i\right) \lor x_n \implies c\\ \iff & \left( \bigvee_{i=1}^{n-2} \lnot x_i\right) \lor x_{n-1} \implies x_n \implies c\\ \iff & x_1 \implies \dots \implies x_{n-1} \implies x_n \implies c \end{align*}

But note that as the disjunction is commutative we could also have proceeded this way:

\begin{align*} & \left( \bigvee_{i=1}^n \lnot x_i\right) \lor c\\ \iff & \left( \bigvee_{i=2}^{n} \lnot x_i\right) \lor \lnot x_1 \lor c\\ \iff & \left( \bigvee_{i=2}^{n} \lnot x_i\right) \lor x_1 \implies c\\ \end{align*}

Or any other way. This shows that the order in which we discharge assumptions does not matter.

Edit:

apparently this cannot be correct, as the answer by Derek Elkins says the order does matter.