Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 1: A ⇒ (BA)


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

For this first example we show how to develop the proof using the rules and presentation introduced on the previous page:


⊢ A ⇒ (B ⇒ A) by λ(x.slot1) Construction rule x : A ⊢ B ⇒ A by λ(y.slot2) Construction rule x : A, y : B ⊢ A by x Hypothesis rule

We can get the evidence for this simple proposition by following the complete proof from bottom up and substituting terms for slots. We substitute x for slot2 and then substitute λ(y.x) for slot1 to get λ(x.λ(y.x)). We call this the extract of the evidence from the proof. For this proposition, it is an operation that takes evidence x for A and returns an operation λ(y.x) which takes evidence y for B and returns evidence for A, namely x. Note that Nuprl displays the extract in a more compact form, as λx,y. x. This example is a very clean and elegant explanation of how we can come to know an implication without having specific evidence for any of the constituent propositions, A or B. This illustrates how logic is capable of working with hypothetical information and transforming it.


Nuprl Proof

Next we show how to develop this proof in Nuprl. One difference from above is that we can't simply type a goal of A (B A), because Nuprl won't know what A and B are. Instead we specify that our goal is to prove the theorem uniformly for all propositions A and B. In Nuprl this is displayed as [A, B : ]. (A B A). The symbol is a type of quantifier meaning "for all," which is a topic we will discuss later. To begin the proof in Nuprl, we must first apply the tactic UD for uniform decomposition, once for each propositional variable. This step declares that the variable (e.g. A) is a proposition, displayed as ; note, however, that in this step we do not yet have hypothetical evidence for the proposition.

Another difference from above is that some of the tactics are followed by THENA Auto. This additional step tells Nuprl to automatically prove any auxiliary well-formedness subgoals.

Here is a representation of the complete proof in Nuprl:

⊢ ∀[A,B:ℙ]. (A ⇒ B ⇒ A) | BY (UD THENA Auto) | [1]. A:ℙ ⊢ ∀[B:ℙ]. (A ⇒ B ⇒ A) | BY (UD THENA Auto) | [2]. B:ℙ ⊢ A ⇒ B ⇒ A | BY (D 0 THENA Auto) Construction rule | 3. A ⊢ B ⇒ A | BY (D 0 THENA Auto) Construction rule | 4. B ⊢ A | BY NthHyp 3 Hypothesis rule

In Nuprl, once a proof is finished we can actually extract the program from it. The extract shown at the top of the page is the result from this Nuprl proof.

In the frame below, you can follow the "Proof" link to view a step-by-step projection of the Nuprl proof. For instructions see How to step through a proof. In the frame there is also a list of the definitions used, along with lines of LaTeX for typing the statements. This LaTeX requires a separate style file written for Nuprl. Alternatively, you can also view a PDF of the complete proof as projected from Nuprl, similar to what is shown above.




Previous Page Next Page


Table of Contents