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.
As you work through this exercise we expect you to learn the following:
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:
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:
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.
We've seen both kinds of interaction
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.
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.
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.
= 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
Figure 1.2 on page 27 of the textbook lists all the salient features for what rules prove.
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