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 f0 and g0, then λ(x. g0(x) (f0(x))) is indeed an operation that takes evidence for A into evidence for C.
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