Exercise 1: Forward Proof

## Overview

In this exercise you will build some small proofs of formulas in propositional logic. The proofs you will build will be in the forward style as they will start with the hypotheses you assume and work forwards towards the conclusion you are trying to establish.

## Learning Objectives

As you work through this exercise we expect you to learn the following:

• Learn to Construct proofs in the forward style.
• Learn to use feedback provided by the proof checker when you make a mistake.
• Internalize that logic is mechanizable.

## Getting Started

The proofs you will turn in will be mechanically checked proofs. The checking is done by a Haskell program, and in order to check your proofs you will have to:

• Install the Haskell Platform on your computer (an integrated system of compilers, tools and standard libraries).
• Load the proof checker into the Haskell Platform using GHCI, one of the many tools that comes with the platform.
• Learn how to format your proofs in a style acceptable as input to the proof checker.

The Haskell platform is easy to install on Windows machines, Macs, or Linux boxes. Simply follow the link to the Haskell Platform, and then follow the directions for your type of machine. If you have any problems at all, please seek help immediately. Professor Sheard has experience with Windows machines, and Professor Hook has experience with Macs. You will find that many of your classmates also have experience with installing the Haskell Platform , so ask around, or try the class mailing list.

Once the platform is installed, see that it is working. Open a shell or cmd interface and type "ghci". This starts up the ghci interpreter and leaves you at the ghci prompt where you can instruct the system to load Haskell programs. In my system the system shell with the working ghci program, waiting for a prompt looks like this:

The proof checker we will be using is composed of several files: (1) Prop.hs, (2) Blocks.hs, and (3) ForwardProver.hs.

To get started create a new directory where you will write your Haskell programs for this class, and then right click the links above and save all three of the files into that directory. Now in the same directory create a file called "ex1.hs" that looks like this:

You can also right click on the file image above and save the file in your code directory. Later, you will add your proofs to this file.

Once you have created the "Ex1.hs" file:

• Start up a shell.
• Start up GHCI
• Once it has started, load in "Ex1.hs" by typing the following command at the prompt: ":l Ex1.hs" (a colon ":" a lower case "L" a space and then file name).

Ex1.hs has several proofs already loaded. To observe a proof simply type its name. This is how my shell looks like after I have loaded Ex1.hs and asked to observe the proof ex1_14 which stands for example 1.14 which you can find in the textbook on page 16. Study the proof in the book, and the mechanized version inside the proof checker.

The two proofs have identical structure (though the numbering of the mechanized proof lines is a little different). Be sure you understand the the proof. Reread the textbook if you don't, or ask some one to give you some pointers.

In the next step of the assignment you will create some proof of your own by interacting with the proof checker inside the GHCI tool.

### Interacting at the prompt in GHCI

In general one interacts with GHCI by either giving a command or asking GHCI to evaluate a Haskell expression.

We've seen both kinds of interaction

1. ":l Ex1.hs" is a command. In general one gives commands to GHI by typing a colon then the command name. The command ":l Ex1.hs" means load the Ex1.hs file. You can find out about other GHCI commands by typing the command ":?".
2. "ex1_14" is a request for evaluation. ex1_14 is a Haskell variable whose value is a proof. The proof is displayed when we type its name. You can evaluate any well typed expression. Try typing "3+4" for example and see what happens.

### Creating Propositions and Proofs

This exercise is all about creating proofs. How is that done? Inside the file ForwardProver.hs is a declaration for the propositions p1, p1 and p3, and the proof ex1_14. Let's study how they are created. The declarations for p1,p2,p3 and ex1_14 looks like this:

```p1 = LetterP 1
p2 = LetterP 2
p3 = LetterP 3

ex1_14 = Proof
[ PREMISE 1 (ImpliesP p1 (ImpliesP p2 p3))
, IMPLYi 7 [ ASSUME 2 (AndP p1 p2)
, ANDe1 3 2
, ANDe2 4 2
, IMPLYe 5 1 3
, IMPLYe 6 5 4
] ]
```

Proofs are created from Rules, Propositions, Labels, Paths, and Lists. Generally, objects such as Rules, and Propositions are created using functions, and lists are created using square brackets like [2,39,7]. In the example above we observe the following.

• A Proposition is created using functions like LetterP and ImpliesP.
• A Labels and Paths are just Int constants. So 2 is a Label.
• Rules are created using functions like IMPLYi, ASSUME, ANDe1, and IMPLYe.
• A Proof is created using the function Proof applied to a list of Rules.

To use a function it must be applied to some arguments. Different functions will take different kinds of arguments. When we write:

```LetterP  :: Int -> Proposition
ANDe1    :: Label -> Path -> Rule
IMPLYi   :: Label -> [Rule] -> Rule
ImpliesP :: Proposition -> Proposition -> Proposition
Proof    :: [Rule] -> Proof
```

We are making a statement about what kinds of arguments a function takes. We read the statement ANDe1 :: Label -> Path -> Rule as "the function ANDe1 has the type Label -> Path -> Rule". Which means it is a function of two argumenta (a Label and a Path) and it produces a Rule. In general, one can determine the number of arguments that a function takes by counting the arrows (->) in its type statement. Thus LetterP and Proof take one argument and ANDe1, IMPLYi, and ImpliesP take 2 arguments.

#### A Complete set of functions for creating Propositions.

```LetterP  :: Int -> Proposition
AndP     :: Proposition -> Proposition -> Proposition
OrP      :: Proposition -> Proposition -> Proposition
ImpliesP :: Proposition -> Proposition -> Proposition
NotP     :: Proposition -> Proposition
AbsurdP  :: Proposition
TruthP   :: Proposition
```

As a convention every function for creating Propositions ends in a capital letter P. The function LetterP creates propositional variables. Each variable like (LetterP n) stands for the truthfulness of some proposition that can be either true or false. We use a different n for each proposition in question. TruthP is the proposition that is always true, and AbsurdP is the proposition that can never be true.

#### A Complete set of functions for creating Rules.

```  = PREMISE Label (Prop Int)
| ASSUME Label (Prop Int)

| ANDi  Label Path Path
| ANDe1 Label Path
| ANDe2 Label Path

| ORi1 Label Path (Prop Int)
| ORi2 Label (Prop Int) Path
| ORe Label Path [Rule] [Rule]

| IMPLYi Label [Rule]
| IMPLYe Label Path Path

| NOTi Label [Rule]
| NOTe Label Path Path
| NOTNOTe Label Path

| ABSURDe Label Path (Prop Int)
| COPY Label Path

| LEM Label (Prop Int)
| MT Label Path Path
| NOTNOTi Label Path
| PBC Label [Rule]

```

We have grouped the rules by the kind of Proposition they manipulate. Generally rules are classified as either an introduction rule or an elimination rule. As a convention we use the suffix "i" (e.g. ANDi, ORi1, NOTi) for introduction rules and the suffix "e" (e.g. ANDe1, ORe, NOTe). for elimination rules.

If we use XX as a generic Rule name base, we find

• (XXi label m n) proves an XX fact from inputs m and n.
• (XXe label x m) proves something from an XX fact input x and other information m.

Figure 1.2 on page 27 of the textbook lists all the salient features for what rules prove.

#### The only way to create a Proof.

There is only one way to create a proof, That is using the function Proof:: [Rule] -> Proof. Evaluation of a proof causes the system to pass the proof to the proof checker. If the checker succeeds, then a proof tree is printed. I.e.

```---------- Proof Checks! -----------

1  p1 => p2 => p3    PREMISE
+----------+
2  p1 /\ p2          |ASSUME    |
3  p1                |ANDe1 2   |
4  p2                |ANDe2 2   |
5  p2 => p3          |IMPLYe 1 3|
6  p3                |IMPLYe 5 4|
+----------+
7  (p1 /\ p2) => p3  IMPLYi [2,3,4,5,6]

----------   Theorem!    -----------

p1 => p2 => p3 |- (p1 /\ p2) => p3
```

If the check fails, then a diagnostic error is printed. For example

```******** ERROR ********

Near 6   IMPLYe 5 99
The path 99   is not in the scope:
1   = PREMISE p1 => p2 => p3
2   = ASSUME p1 /\ p2
3   = ANDe1 2
4   = ANDe2 2
5   = IMPLYe 1 3

---- in the putative proof: ----

1  p1 => p2 => p3  PREMISE
2  p1 /\ p2           ASSUME
3  a                  ANDe1 *2  = a /\ b
4  b                  ANDe2 *2  = a /\ b
5  *3                 IMPLYe 1 3
6  *99                IMPLYe 5 99
7  p1 /\ p2 => *99 IMPLYi [2,3,4,5,6]

******** ERROR ********
```

The checker scans the proof from top to bottom. When it discovers an error it tells the user

• What proof rule the error is near (Rule with label 6).
• What the error is (The path 99 from (IMPLYe 5 99) is not in scope)
• The prefix of the proof that checked (labels 1)
• The suffix of the proof that has not yet been checked (labels 2 - 7)

## Directions

• Read and study the section in the textbook about constructing proofs, pages 1-29.
• Reconstruct the example proofs 1.16 (page 18) and 1.20 (page 21) and 1.23 (page 23) by writing a declaration for them in your file Ex1.hs.
• Pick two (2) problems from problem 1 (a)-(y) from Exercise 1.2 (page 78-79) and create proofs for them and enter the proofs as declarations in your file Ex1.hs. Be prepared to talk about the proofs you created in class on Thursday.