Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

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


∀[A,B,C:ℙ].((A ⇒ B) ⇒ (A ⇒ B ⇒ C) ⇒ A ⇒ C) Extract: λf,g,x.(g x (f x)) where f : A ⇒ B g : A ⇒ B ⇒ C x : A

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.


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:

⊢ ∀[A,B,C:ℙ]. ((A ⇒ B) ⇒ (A ⇒ B ⇒ C) ⇒ A ⇒ C) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. A: ℙ [2]. B: ℙ [3]. C: ℙ ⊢ (A ⇒ B) ⇒ (A ⇒ B ⇒ C) ⇒ A ⇒ C | BY RepeatFor 3 ((D 0 THENA Auto)) Construction rule, 3 times | 4. A ⇒ B 5. A ⇒ B ⇒ C 6. A ⊢ C

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.

[1]. A: ℙ [2]. B: ℙ [3]. C: ℙ 4. A ⇒ B 5. A ⇒ B ⇒ C 6. A ⊢ C | BY D 4 Application rule on (A ⇒ B) |\ | 4. A ⇒ B ⇒ C | 5. A | ⊢ A Subgoal 1: Provide evidence for A | | 1 BY NthHyp 5 Hypothesis rule \ 4. A ⇒ B ⇒ C 5. A 6. B ⊢ C Subgoal 2: Prove C, with evidence for B now available to use

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.

[1]. A: ℙ [2]. B: ℙ [3]. C: ℙ 4. A ⇒ B ⇒ C 5. A 6. B ⊢ C | BY D 4 Application rule on (A ⇒ B ⇒ C) |\ | 4. A | 5. B | ⊢ A Subgoal 2.1: Provide evidence for A | | 1 BY NthHyp 4 Hypothesis rule \ 4. A 5. B 6. B ⇒ C ⊢ C Subgoal 2.2: Prove C, with evidence for (B ⇒ C) now available to use

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.

[1]. A: ℙ [2]. B: ℙ [3]. C: ℙ 4. A 5. B 6. B ⇒ C ⊢ C | BY D 6 Application rule on (B ⇒ C) |\ | ⊢ B Subgoal 2.2.1: Provide evidence for B | | 1 BY NthHyp 5 Hypothesis rule \ 6. C ⊢ C Subgoal 2.2.2: Prove C, with evidence for C now available to use | BY NthHyp 6 Hypothesis rule, finishing the proof




Previous Page Next Page


Table of Contents