## Theorem 2: (*A* ⇒ *B*) ⇒ ((*A* ⇒ (*B* ⇒ *C*)) ⇒ (*A* ⇒ *C*))

The operational explanation of this theorem is λ(*f*. λ(*g*. λ(*x. g*(*x*)(*f* (*x*))))), or more compactly as λ* f, g, x.* (*g x* (*f x*)). What we have here is that *f* is hypothetical evidence for the assumption (*A* ⇒ *B*), and *g* is hypothetical evidence for (*A* ⇒ (*B* ⇒ *C*)), and *x* is hypothetical evidence for *A*. So we can see that *g*(*x*) is evidence for (*B* ⇒ *C*) and *f*(*x*) is evidence for *B*. Therefore by reasoning about the composition of the operations *f* and *g*, we see that *g*(*x*) applied to *f*(*x*), or *g*(*x*)(*f*(*x*)), is evidence for *C*. If we imagine being given concrete evidence for *f* and *g*, say *f*_{0} and *g*_{0}, then λ(*x*. *g*_{0}(*x*) (*f*_{0}(*x*))) is indeed an operation that takes evidence for *A* into evidence for *C*.

### Nuprl Proof

To begin the proof, we apply uniform decomposition (UD) to establish *A*, *B*, and *C* as propositions and then apply the construction rule to decompose the implications in the goal:

For the next step we decide to apply the operation (*A* ⇒ *B*) so that we can get evidence for *B*, i.e. *f* (*x*) in the extract above. This creates two subgoals in Nuprl. First, we have to prove that we can provide evidence for *A*. This part is trivial since we can just use the hypothesis rule. For the second subgoal, we now have evidence for *B* and can use it to prove the main goal, *C*.

Next we decide to apply the operation (*A* ⇒ *B* ⇒ *C*) from our list of assumptions to get evidence for (*B* ⇒ *C*), i.e. *g* (*x*) in the extract above. Again, we'll have to show that we have evidence for *A* in one subgoal, and then we can use evidence for (*B* ⇒ *C*) when returning to the main goal of proving *C*.

To finish the proof, we apply the operation (*B* ⇒ *C*) to get evidence for *C*. This corresponds to *g* (*x*) (*f* (*x*)) in the extract.

- View the proof in PDF format
- Step through the proof in the frame:

Table of Contents