Exercicios de Lógica

Deduction using the ProofWeb system Cezary Kaliszyk Femke van Raamsdonk Freek Wiedijk Hanno Wupper Maxim Hendriks Roel de Vrijer Abstract This is the manual of the ProofWeb system that was implemented at the Radboud University Nijmegen and the Free University Amsterdam in the SURF education innovation project Web deduction for education in formal thinking 1 Contents 1 Introduction 3 2 Using the system 5 21 Logging in 5 22 The list of exercises 6 23 The prover interface 8 24 Saving exercises 13 25 The status of the exercises 15 3 Writing formulas 18 4 Gentzen style tree proofs 19 41 Example on paper 20 42 Example in ProofWeb 21 5 Fitch style box proofs 25 51 Example on paper 25 52 Example in ProofWeb 27 53 Forward tactics 32 54 The insert tactic 33 55 The order of insert tactics 35 6 ProofWeb versus Coq 36 61 Formula syntax 36 62 Tactics 37 7 ProofWeb versus Huth Ryan 38 71 Formula syntax 38 72 Proof display 39 8 Outlook 39 A Tactics in Gentzen style 41 B Tactics in Fitch style 46 B1 Structural tactics 46 B2 Backward tactics 46 B3 Forward versus backward tactics 51 2 1 Introduction This document is the manual of the ProofWeb system If you are just inter ested in using the system you can best skip this introduction and directly go to Chapter 2 on page 5 This document does not explain mathematical logic in detail but is intended as a companion to a logic textbook when using the ProofWeb system For instance one can read 6 for Gentzen style tree proofs or 3 for Fitch style box proofs However the appendices of these notes can be used as a reference for natural deduction ProofWeb is a system for practising natural deduction on a computer It is meant to be used in introductory courses in mathematical logic The logics that ProofWeb has been specifically designed for are the usual basic ones first order propositional logic first order predicate logic first order predicate logic with equality ProofWeb is designed for the classical variants of these logics but it is easy to work in ProofWeb in the constructive fragments of these logics as well ProofWeb combines the following features ProofWeb has been designed to be as close as possible in look and feel to the way mathematical logic is taught in textbooks For Fitch style box proofs it specifically matches the conventions of Logic in Computer Science Modelling and Reasoning about Systems by Michael Huth and Mark Ryan 3 published by Cambridge University Press When using ProofWeb one is using the Coq proof assistant developed at the INRIA institute in France without any restrictions This means that with ProofWeb one is using a system that has the power to build computer proofs like the one of the Four Color Theorem 2 or a proof of the correctness of an optimizing C compiler 4 ProofWeb is used through the web One does not need to install any spe cial software to be able to use the system A web browser without any ProofWeb specific plugins and even without Java is all that is needed Students will be able to work on their exercises from any computer con nected to the Internet like for instance a computer in an Internet cafe without first having to copy their files or to install any special software With ProofWeb all files are on a central server Teachers will at all times be able to see the status of their students work including their solutions to the exercises in full Also the students work can be easily backed up ProofWeb comes with free course notes explaining the system This is the text that you are currently reading 3 ProofWeb comes with a database of around two hundred basic exercises ProofWeb will automatically check whether solutions to exercises are cor rect or not and present this information both to the student and the teacher in a clear tabular format If you are a student there are two ways to work with ProofWeb 1 Just go to the ProofWeb server provided by the Radboud University Nij megen httpproofwebcsrunl and use the free guest account There is no need to register or to provide a password In this mode the full set of exercises is not available This way of working with ProofWeb is just for trying it out 2 If you follow a course in mathematical logic that uses ProofWeb for the practical work then go to the ProofWeb server of that course which often also will be proofwebcsrunl and use the account there that your teacher will have made for you Ask your teacher for the username and password of that account If you are a teacher and want to use ProofWeb in your course then there also are two ways for this 1 Either you can host your course on the server of the Radboud University Nijmegen To do this send mail to proofwebcsrunl and provide details about the course that you want to host This service is currently provided for free 2 Alternatively you can host a ProofWeb server on a machine of your own To do this go to httpproofwebcsrunl follow the link about installing the ProofWeb system and follow the in stallation instructions that will tell you what files to download to install the ProofWeb system and what to do with them To follow these instal lation instructions on how to install ProofWeb you will need a machine running Linux 4 2 Using the system To use ProofWeb you need a web browser on a machine connected to the Inter net Unfortunately not all web browsers properly support the technologies that ProofWeb uses For this reason Internet Explorer cannot be used Browsers that have been tested to work are recent versions of Gecko based browsers like Mozilla Firefox Galeon Epiphany and Net scape Webkit based browsers like Safari and Konqueror The Opera browser The ProofWeb system has been developed using Firefox 21 Logging in We will now explain the system by walking through a ProofWeb session We go to the URL of our ProofWeb server In the example that we are showing here this is httpproofwebcsrunl This shows us the main ProofWeb web page We scroll down to the list of courses and click on the link of our course 5 In this example we click the link Inleiding Logica 20072008 which is Dutch for Introduction to Logic This will get us to the login page for the course We enter our username and password and click GO TO USER PAGE This logs us in to the system for the course that we are following 22 The list of exercises We now see the list of exercises for the course It gives for each exercise the name of file that holds the exercise an indication of the difficulty the current status of the exercise and a button for resetting the exercise to its initial state 6 The four possibilities for the status of an exercise are Not touched Incomplete Correct Solved The colors are meant to resemble the colors of a traffic light The challenge of ProofWeb is to have your list of exercises be all green We will explain the meaning of these statuses in detail below The difference between Correct and Solved is that according to the Coq system in both cases the solution to the exercises has no errors but that only in the latter case is the solution restricted to deduction rules that are allowed for the course Now we scroll down in the list of exercises to the first exercise about propo sitional logic called prop 001v 7 We click the button with the name of this file on the left This will open the exercise in the prover interface 23 The prover interface We are now looking at the prover interface of ProofWeb It consists of a green menu bar at the top of our browser window and three panes On the left there is the pane in which we are editing a proof script On the top right there is the pane that will show the proof state of our proof We will explain below what this means The proof state in this pane is shown in the style that is standard when working with the Coq proof assistant Here also will be shown the messages of the Coq system that we are communicating with on the ProofWeb server On the bottom right there is the pane that shows the proof that we are working on The proof in this pane will be shown in the style that is customary in mathematical logic teaching ProofWeb can show the proof in the bottom right pane in three different ways Depending on the course that you are following one of these proof display styles already may be active To change the style of proof display one uses the Display menu Let us first put the system in the mode in which it displays proofs in Gentzen tree style 8 Another setting that one might like to change when starting working with Proof Web is the electric terminator When this feature is active typing a period automatically executes the command that it terminates Some people like this convenience while others prefer to separate typing their script from having the system execute their commands To activate the electric terminator select Toggle Electric Terminator from the Debug menu We are now ready to start working on the exercise Currently the text on the left the solution to the exercise that we are editing has not yet been executed This text is a script consisting of commands that are all terminated by a period character One can execute those commands by clicking the downward arrow in the green menu bar Alternatively one can execute the next command 9 by holding down the control key while simultaneously typing the downarrow key on the keyboard We now execute the commands by clicking the down arrow until we have executed the Proof command At this point we are working on a proof and an incomplete proof will now be displayed on the lower right Then we remove the text propproof from the script It should be replaced by a series of commands that create a proof of the statement We type the first command impi H and execute it The details of the commands that are available and what they mean will be given below We now have On the bottom right the incomplete proof after this command now is A A B A i H The dots are the part of the proof that is not yet completed It has to be replaced by a valid proof of A by issuing more commands in the proof script On the top right we see the proof state of the Coq proof assistant that is checking our proof It looks like 10 1 subgoal H A B A It means that our first subgoal out of only one is to prove the statement below the line A where we are allowed to use the assumptions above the line In this case there is only one assumption A B The label of this assumption is H which is how we should refer to the assumption in the script This subgoal corresponds to the triple dots in the proof on the lower right We now look at what the proof looks like in the two other display styles First here is what it looks like when instead of just statements we ask the system to display sequents In this case the allowed assumptions are showed to the left of the turnstyle symbol Instead of just A as the middle line of the proof we now have A B A Despite the change in presentation the proof has stayed exactly the same The third style is Fitchs box style 11 In this style the incomplete proof looks like 1 H A B assumption 2 A 3 A B A i 12 Again the dots have to be filled in to complete the proof We will now finish the exercise We add two more commands to the script cone1 B exact H execute them and then also execute the final Qed This leads to the message prop001 is defined at the top right where Coq shows its output 12 It means that the proof script is complete which means that it has generated a correct proof of the statement 24 Saving exercises We are now done with exercise the script on the left is what it should be We save the file on the server by selecting Save from the File menu This saves the script as the file prop 001v in the students directory on the ProofWeb server 13 Next we select Load New from the File menu to get back to the list with exercises The system will warn us that we are leaving the page with the script it does not realize that it just has been saved 14 Generally it is a good thing that ProofWeb will warn you about this but in this case we can of course ignore this message and click OK 25 The status of the exercises We now again are looking at the list of exercises The status of prop 001v has changed from a gray Not touched to a green Solved because we saved a correct solution Instead of going for the next exercises let us look what happens when we save an incorrect solution We go back to the exercise by clicking the prop 001v button once more remove the lines cone1 B exact H 15 from the proof script save again and go once more to the list of exercises The status now will be a red Incomplete This also will be the status when the file is not so much incomplete as well just wrong If you want to know why ProofWeb thinks there is an error in your solution you can click the why link next to the status You will get a new window that shows the error message of Coq ProofWeb also has an orange status that is in between the green and the red ones saying Correct You get this when the file is correct Coq but you modified it in a way that is not allowed for the course For instance you might ask Coq to do the proof for you by using the tauto command which makes Coq run an automated propositional theorem prover 16 This will prove the statement but of course this is not an allowed solution to the exercise Hence the status will become Correct instead of Solved The Correct status also will be given if you just delete all the text in the file as the empty file is a correct Coq file too Of course that is not an allowed solution to the exercise either Again when the status is Correct you can click on why to find out what you did that ProofWeb thinks is not allowed in the course The word why is a bit strange in this context as Coq will not so much explain why the thing is correct but instead why it is not solved These error messages generally are a bit cryptic as well 17 This ends our example of a ProofWeb session We will now discuss the system in detail First we will explain how to write formulas in the ProofWeb system 3 Writing formulas The ASCII syntax for formulas of first order predicate logic is given by the following table False True A A A B A B A B A B A B A B A B A B x A all x A x A exi x A For example the formula xPx Qa Qa x Px is written in ASCII syntax as exi x Px Qa Qa exi x Px Note that in ProofWeb one puts a comma after a quantifier Another slight deviation of the ProofWeb formula syntax from standard syntax is that if a predicate has just a single variable as the argument one is allowed to omit the brackets It is not obligatory though Therefore the formula also might be written as exi x P x Q a Q a exi x P x In fact this is how Coq prints this formula back at the user In the exercise files the formulas are always written with the brackets present though A note for people who know the Coq system In Coq a different notation for the quantifiers is customary 18 x A forall x D A x A exists x D A In this D is the domain over which one quantifies There are two differences between the ProofWeb quantifiers and the stan dard Coq quantifiers First the ProofWeb quantifiers have a priority that is customary in logic textbooks they bind more strongly than the propositional connectives The Coq quantifiers bind weakly which is the standard in proof assistants For instance the formula all x A B is read as x A B which is the reading of x A B in logic textbooks However forall x D A B is read as x A B Second with the Coq quantifiers one indicates the domain The ProofWeb quantifiers do not need this as they use a fixed domain D This domain is defined in the file ProofWebv which is loaded at the start of the ProofWeb exercises The Coq quantifiers can be useful for people who want to use ProofWeb for complicated examples in which different variables have different types In that case they can just use the Coq versions of the quantifiers The ProofWeb tactics which are the subject of the next two chapters have been programmed to work with either quantifier style 4 Gentzen style tree proofs This chapter explains how to build natural deduction proofs using ProofWeb It treats a style of natural deduction introduced by Gerhard Gentzen in 1935 in his dissertation at the University of Gottingen We will here call that style tree proofs to distinguish it from the box proofs which will be the subject of the next chapter In this chapter we will not explain natural deduction proofs in detail You will need to read a textbook for that like Dirk van Dalens Logic and Structure 6 Here we will just explain how to do this kind of proof in the ProofWeb system 19 41 Example on paper Here is an example of a natural deduction proof in predicate logic in the way that it is written on paper xPx QaH1 Pb QaH3 PbH4 x Px i QaH5 QaH2 e x Px e x Px e H4H5 x Px e H3 Qa x Px i H2 xPx Qa Qa x Px i H1 In different textbooks the precise notation for this kind of proof will vary but whatever the details are natural deduction proofs in the tree style have a shape that is close to this Differences between textbooks might be that the order of the connective and the i or e can be the other way around in which case it is i instead of i or the i or e has to be capitalized in which case it is I instead of i Another difference is that often the assumptions at the leaves of the proof tree are not put in square brackets but instead are crossed out with a diagonal slash Crossing out an assumption in such a way while doing a proof can give a very satisfactory feeling However on a computer screen it is a bit hard to implement The convention of the square brackets we took from 6 In natural deduction proofs the rules and assumptions generally are anno tated to indicate which assumption originates from which rule invocation In ProofWeb we do this in green in the following style xPx QaH1 Pb QaH3 PbH4 x Px i QaH5 QaH2 e x Px e x Px e H4H5 x Px e H3 Qa x Px i H2 xPx Qa Qa x Px i H1 Again the way this annotation is done differs between textbooks Often the annotations are subscripts or superscripts of the rules and often the annotations are numbers Here we use the labels that one gets in the Coq system which are not numeric Now here is the way this same proof is displayed in the ProofWeb window As you can see it is very similar to the mathematical style that we showed The main difference is that the lines are a bit longer 20 Q aH5 Q aH2 e P bH4 i e P b Q aH3 x P x x P x eH4H5 x P x Q aH1 x P x eH3 x P x iH2 Q a x P x iH1 x P x Q a Q a x P x This example is quite involved For this reason we will use a simpler example in the next section which explains the commands that one uses to build a proof in ProofWeb A BH A e1 A B A i H This example is the same that was also used in Chapter 2 In ProofWeb it is displayed like A BH e1 A iH A B A Next we will explain how to write a ProofWeb script that generates this proof 42 Example in ProofWeb First let us show the exercise for this example which is generally the starting point when doing a proof in ProofWeb Require Import ProofWeb Variable A B Prop Theorem prop001 A B A Proof propproof Qed It will be clear that the exercise here is to create a natural deduction proof of the statement A B A The comment that tells where the proof has to be filled in is in green Note that Coq will not be able to process this file as it is It will not want to process the Qed line as the proof will not be finished at that point Here is a solution to this exercise that Coq accepts and that generates the proof that we just showed 21 Require Import ProofWeb Variable A B Prop Theorem prop001 A B A Proof impi H cone1 B exact H Qed We will now explain this script line by line The two most interesting lines in the script are the tactics that actually build the proof They are shown in green The first line of the script Require Import ProofWeb tells Coq to load the definitions needed for ProofWeb These are in a file ProofWebv but the contents of that file is not interesting for users of the system The second line of the script Variable A B Prop tells Coq that we want to use propositional variables A and B In Coq everything needs to be declared before it can be used For example to declare a unary predicate P and a binary predicate Q we need to write Variable P D Prop Variable Q D D Prop Or if we want a unary function f and a binary function g Variable f D D Variable g D D D Even for variables of the predicate logic we need this kind of declaration Here is the declaration needed to have a proof use free variables x and y Variable x y D Variables introduced by introduction or elimination rules do not need a decla ration like this The domain of the logic called D is declared in the ProofWebv file In that file also a single constant in this domain is declared which is called d This constant is needed to make some of the proof commands work but one can use it in a proof too if one likes Now the third nonempty line of the script Theorem prop001 A B A 22 tells the system that we will be going to prove a statement If we manage to finish this proof the name of the theorem will be prop001 The fourth nonempty line is Proof It does nothing It visually complements the Qed at the end that is all If it is left out everything works just as well But if you remove it from the script you will not get a Solved status ProofWeb compares a solution to the original exercise file and if a line suddenly is missing it does not like it Now we get to the lines that build the actual proof The command in these lines are called tactics This proof just contains two tactics but ProofWeb has many For the full list see Appendix A on page 41 Before the first tactic is executed the incomplete proof is just the statement that has to be proved with dots where the proof should go A B A We will grow the proof upward by executing tactics Clearly this statement should be proved by implication introduction So we execute the tactic for that which is called impi impi H Most of the ProofWeb tactic names consist of three letters that identify the connective according to the following table fls tru not con dis imp all exi equ then an underscore character then an i or e to distinguish between intro duction and elimination rules and finally an optional 1 or 2 to distinguish between left and right rules or very occasionally a prime character for a special tactic variant These tactics also can be selected from the Backward menu in the ProofWeb menu bar in which case a template for the tactic will be inserted in the text by the system After executing the impi tactic the incomplete proof becomes A A B A i H 23 As you can see the H argument to the tactic gave the label for the assumption that is introduced by this rule We will be able to use this assumption in our proof as A BH Tactics generally have arguments which are labels formulas and terms Impor tant Formulas and terms that are tactic arguments will need to be put in brackets Else the command will give a syntax error The templates inserted by the Backward menu already has these brackets in them We now insert a left conjunction elimination rule in our incomplete proof by issuing the cone1 tactic cone1 B This turns the incomplete proof into A B A e1 A B A i H Now to finish our proof we will need to tell ProofWeb that the A B is one of the assumptions the one labeled H This is done by the command exact H After this tactic the proof that we built is finished and looks like A BH A e1 A B A i H We now issue the command Qed to close the proof and our script is done The larger proof on page 20 can be generated by a very similar script We will not walk through that script in detail but we will just present it here in its entirety Try to relate the tactics in this script to the inference rules that are used in the proof Require Import ProofWeb Variable P Q D Prop 24 Variable a D Theorem example exi x Px Qa Qa exi x Px Proof impi H1 impi H2 exie exi x Px Qa b H3 exact H1 dise Pb Qa H4 H5 exact H3 exii b exact H4 flse nege Qa exact H5 exact H2 Qed This finishes our description on how to build a natural deduction proof in Gentzens tree style using ProofWeb We have not discussed all natural deduc tion tactics in detail as they all behave in a very similar way See Appendix A on page 41 for the full list with for each tactic a description of their behavior In the ProofWeb menus there also is a menu Forward next to the Backward menu This tactics in this menu will behave reasonably when building a Gentzen style tree proof but they are primarily intended for making it easier to build Fitch style box proofs which is the subject of the next chapter 5 Fitch style box proofs This chapter explains how to build natural deduction proofs using ProofWeb It treats a style of natural deduction introduced by Frederic Fitch We will call that style box proofs to distinguish it from the tree proofs which were discussed in the previous chapter We will not explain these natural deduction proofs in detail You will need to read a textbook for that first ProofWeb was designed to be used next to Michael Huth Mark Ryans Logic in Computer Science Modelling and Reasoning about Systems 3 so that is the book that we recommend to fully understand Fitch style box proofs However apart from minor notational differences ProofWeb can be used with any textbook teaching natural deduction in Fitchs box style 51 Example on paper Here is an example of a natural deduction proof in predicate logic in the way that it is written on paper 25 1 xPx Qa assumption 2 Qa assumption 3 b Pb Qa assumption 4 Pb assumption 5 x Px i 4 6 Qa assumption 7 e 62 8 x Px e 7 9 x Px e 34568 10 x Px e 139 11 Qa x Px i 210 12 xPx Qa Qa x Px i 111 And here is the way this same proof is displayed in the ProofWeb system 1 H1 x P x Q a assumption 2 H2 Q a assumption b 3 H3 P b Q a assumption 4 H4 P b assumption 5 x P x i 4 6 H5 Q a assumption 7 e 62 8 x P x e 7 9 x P x e 34568 10 x P x e 139 11 Q a x P x i 210 12 x P x Q a Q a x P x i 111 As you can see some labels have been added in green the boxes are not closed on the right anymore to save some space and the two subboxes for the e rule have grown together Apart from that it is quite the same This example is quite involved For this reason we will now give a simpler example for the next section which explains the commands that one uses to build a proof in ProofWeb 1 A B assumption 2 A e1 1 3 A B A i 12 26 In ProofWeb it is displayed like 1 H A B assumption 2 A e1 1 3 A B A i 12 Now in different textbooks the notation for this kind of proof will vary but whatever the precise details are natural deduction proofs in the box style will have a structure that is very similar to this Differences between textbooks might be that the notation for the rules might deviate in the details and in particular that the subproofs often will not be indicated by boxes but by other shapes In 3 which we follow in ProofWeb the subproofs are enclosed in boxes 1 A B assumption 2 A e1 1 3 A B A i 12 However in other books just a vertical line to left is used with a short horizontal line indicating where the assumption is separated from the rest of the subproof 1 A B assumption 2 A e1 1 3 A B A i 12 Also occasionally a third variant is used in which only the assumption is en closed in a box This way of writing Fitch proofs is called flag style as there now is a shape like a waving flag 1 A B assumption 2 A e1 1 3 A B A i 12 Currently ProofWeb only supports the first of these three variants on the nota tion for Fitchstyle proofs We will now explain how to write a ProofWeb script that generates this proof 52 Example in ProofWeb First let us show the exercise that corresponds to this example which is generally the starting point when doing a proof in ProofWeb 27 Require Import ProofWeb Variable A B Prop Theorem prop001 A B A Proof propproof Qed It will be clear that the exercise here is to create a natural deduction proof of the statement A B A The comment that tells where the proof has to be filled in is colored green Note that Coq will not be able to process this file as it is It will not want to process the Qed line at the end as the proof will not be done at that point without having filled in the proof Here is a solution that Coq accepts and that generates the proof that we just showed Require Import ProofWeb Variable A B Prop Theorem prop001 A B A Proof impi H cone1 B exact H Qed We will now explain this script line by line The two most interesting lines in the script are the tactics that actually build the proof They are shown in green The first line of the script Require Import ProofWeb tells Coq to load the definitions needed for ProofWeb These are in a file ProofWebv but that file is not interesting for users of the system The second line of the script Variable A B Prop tells Coq that we want to use propositional variables A and B In Coq everything needs to be declared before it can be used For example to declare a unary predicate P and a binary predicate Q we need to write Variable P D Prop Variable Q D D Prop Or if we want a unary function f and a binary function g Variable f D D Variable g D D D 28 Even for variables of the predicate logic we need this kind of declaration Here is the declaration for being able to use free variables x and y in a ProofWeb proof Variable x y D Please note that variables introduced by introduction or elimination rules do not need a declaration like this The domain of the logic called D is declared in the ProofWebv file In that file also a single constant in this domain is declared called d This constant is needed to make some of the proof commands work but you can also make use of it in your proof scripts if you like Now the third nonempty line of the script Theorem prop001 A B A tells the system that we will be going to prove a statement The name of this statement will be prop001 The fourth nonempty line is Proof It does nothing It complements the Qed at the end If it is left out everything works just as well However in that case you will not be able to get your exercise a Solved status ProofWeb compares your solution to the original exercise file and if a line is missing it does not like it Now we get to the lines that build the actual proof The command in these lines are called tactics This proof just consists of three tactics but ProofWeb has many For the full list see Appendix B on page 46 Before the first tactic is executed the incomplete proof is just the statement that has to be proved with dots where the proof should go 1 A B A The number 1 to the left is the line number of the single line in this incomplete proof When we work on the proof it will change By the time the proof is finished it will have number 3 On the right there will be the rule that generated this line but this has not yet been fixed so currently this space is empty Now this line will be proved by implication introduction So we execute the tactic for that called impi impi H Most of the ProofWeb tactic names consist of three letters that identify the connective according to the following table 29 fls tru not con dis imp all exi equ then an underscore character then an i or e to distinguish between intro duction and elimination rules and finally an optional 1 or 2 to distinguish between left and right rules or very occasionally a prime character for a special tactic variant These tactics also can be selected from the Backward menu in the ProofWeb menu bar in which case a template for the tactic will be inserted in the text The H argument to the tactic gave the label for the assumption that is introduced by this rule Tactics generally have arguments which can be labels formulas and terms Important Formulas and terms that are tactic arguments will need to be put in brackets Else the command will give a syntax error The templates inserted by the Backward menu already has these brackets in them After executing the impi tactic the incomplete proof becomes 1 H A B assumption 2 A 3 A B A i 12 As you can see the line number of the final line now has changed In ProofWeb we do not use the line numbers to refer to lines in the tactics Instead we use labels which in the proofs are displayed in green In the tactic for implication introduction the label has to be given as an argument In this case the label of the assumption is H In the ProofWeb script we will not use the number 1 to refer to this line but the label H The statement that we next will need to prove the subgoal is the line num bered 2 directly after the dots Of course we will use conjunction elimination to prove this In this section we use the backward tactics which means that we will not be able to use the line that already has A B on it Instead we work backward from the A by giving the tactic cone1 B Look on page 46 to see how the cone1 tactic is documented in Appendix B It needs the argument B because from the subgoal it cannot be deduced what the 30 other side of the conjunction was Also this argument is a formula so it should be put in brackets After the cone1 tactic the still incomplete proof has become 1 H A B assumption 2 A B 3 A e1 2 4 A B A i 13 As you can see the final line now has number 4 and the arguments of the i rule on that line have been renumbered appropriately We can now finish the proof by noting that the subgoal that we are now facing A B actually is the assumption labeled H For this execute the tactic exact H You might expect this to change line 3 to a copy line and in fact the tactic called exact has a synonym called copy 1 H A B assumption 2 A B copy 1 3 A e1 2 4 A B A i 13 but in fact it removes the duplication altogether and gives us as the final proof 1 H A B assumption 2 A e1 1 3 A B A i 12 Copy lines sometimes are retained but only when necessary We now issue the command Qed to close the proof and our script is done The larger proof on page 25 can be generated by a very similar script We will not walk through that script in detail too We will just present it here in its entirety Try to relate the tactics for the natural deduction rules in this script to the inference rules that occur in the proof Require Import ProofWeb Variable P Q D Prop Variable a D 31 Theorem example exi x Px Qa Qa exi x Px Proof impi H1 impi H2 exie exi x Px Qa b H3 exact H1 dise Pb Qa H4 H5 exact H3 exii b exact H4 flse nege Qa exact H5 exact H2 Qed This finishes our description on how to build a natural deduction proof in Fitchs box style using only the backward tactics This method is conceptually easy but often a bit laborious For this reason we will now look at the forward tactics 53 Forward tactics In the previous section we solved the exercise using a script that only used backward tactics impi H cone1 B exact H After the first line of that script the incomplete proof looked like 1 H A B assumption 2 A 3 A B A i 12 If we had been doing the proof by hand we now just would put e1 1 on line 2 and be done with it This also can be done in ProofWeb with the appropriate forward tactic fcone1 H 32 Note that the reference to line 1 is given by the label H See for the documentation of the fcone1 tactic page 51 of Appendix B The prefix f abbreviates forward In fact the backwards tactics also can be given with the prefix b added in front The forward tactics can be inserted in the script by using the Forward menu in the ProofWeb menu bar After the fcone1 tactic the proof will be finished looking like 1 H A B assumption 2 A e1 1 3 A B A i 12 This means that the following shorter script is also a solution to the problem impi H fcone1 H In fact that is how any sensible ProofWeb user would solve it 54 The insert tactic There is one final tactic that we need to explain the insert tactic When one builds a proof using backward tactics one adds lines to the proof after the dots However with the forward tactics the pattern generally is to add lines before the dots To be able to do that one needs the insert tactic Suppose that we have an incomplete proof starting like 1 H A B with more lines after the dots that we will not print here Now suppose further that directly after line 1 we would like to insert another line H1 A e1 1 because we know that A follows from A B The way to do this in ProofWeb is to execute two tactics the insert tactic followed by a forward tactic insert H1 A fcone1 H What will happen if you execute these two tactics is that after the first tactic the proof looks like 1 H A B 2 H1 A 33 and after the second it is 1 H A B 2 H1 A e1 1 In other words the insert tactic inserts a new line in the incomplete proof and then the forward tactic proves it Note that the first tactic corresponds to the left part of the new line while the second tactic corresponds to the right part of the line insert H1 A fcone1 H corresponds to the line H1 A e1 1 Of course it is not obligatory to directly prove an inserted line with just a single forward tactic It is perfectly legal to prove it using a much more involved proof The insert tactic just means now first we will prove this and then we will go on with the rest of the proof A technical aside in the logic this is called a cut or detour As a larger example the bigger proof on page 25 can be more efficiently generated by using forward tactics Require Import ProofWeb Variable P Q D Prop Variable a D Theorem example exi x Px Qa Qa exi x Px Proof impi H1 impi H2 fexie H1 b H3 fdise H3 H4 H5 fexii H4 flse fnege H5 H2 Qed Note that in this script the proof is not generated in a fully forward way line 7 the one with the contradiction is generated in a backward manner using the flse tactic This saves one tactic in the script This finishes our description on how to build a natural deduction proof in Fitchs box style using ProofWeb We have not discussed all natural deduction tactics in detail here as they all behave in very similar ways See Appendix B on page 46 for the full list with for each tactic a description of their behavior 34 55 The order of insert tactics ProofWeb has one unfortunate restriction that is caused by the way it is im plemented on top of the Coq system Sometimes when inserting a line later that line is not visible in a place where according to the incomplete proof it should be visible This is caused by the fact that the line that was inserted only will be visible in the part of the proof that corresponds to the dots where it was inserted Here is a small example Suppose we have a proof 1 A 2 D and we want to insert lines B and C in between the A and D Then we can do insert H2 C giving 1 A 2 H2 C 3 D and subsequently insert H1 B giving 1 A 2 H1 B 3 H2 C 4 D However if we do this in the proof the line labeled H1 will not be available after the C It will only be visible in the part of the proof that it was inserted in which is the part between A and C So when working on the part of the proof that proves D from C one will not be able to refer to the B line This probably will be surprising by that time The solution to this problem is to have the insert lines in the same order as their corresponding lines occur in the final proof If one reorders the inserts 35 insert H1 B insert H2 C there will not be a problem anymore Therefore when using insert tactics in ProofWeb proofs the rule of thumb should be Put the insert lines in the script in the order in which the inserted lines will appear in the proof This finishes the chapter on Fitch style box proofs in ProofWeb 6 ProofWeb versus Coq In ProofWeb one really is using the Coq system One is processing a Coq script without any change to the Coq syntax However the ProofWeb tactics are not the ones that a Coq user normally would use to prove something The Coq tactics are much more efficient but less closely related to the natural deduction rules of first order logic Also the ProofWeb formula syntax deviates a little bit from the way that a Coq user normally would write formulas We will now briefly indicate what are the differences between using Coq in the ProofWeb style and using it in the Coq style 61 Formula syntax In Coq one generally does not use all and exi for the quantifiers but instead one uses forall and exists The reason that ProofWeb defines its own quan tifiers is to get the binding strength the way it is in most logic textbooks Also in ProofWeb one is working in an unsorted logic in which all variables range over the same domain while in Coq variables have a type So in ProofWeb one writes all x Px while a Coq user would write forall x D Px To make things subtle in Coq the typing of the variable can be omitted if the system can deduce the type from the way it is being used Similarly in ProofWeb one uses exi x Px while a Coq user would write exists x D Px These are the only differences between ProofWeb formula syntax and the cus tomary Coq formula syntax The ProofWeb tactics have been designed to also work with the usual Coq quantifiers If you prefer to have multiple sorts and weakly binding quantifiers in your formula syntax it still is perfectly possible to use ProofWeb 36 62 Tactics In ProofWeb one uses many weak tactics There generally are two for every deduction rule a backward and a forward one In Coq one uses fewer but much more efficient tactics The most important Coq tactics are intros apply elim Also there are a couple of Coq tactics that really are just synonyms of the ProofWeb tactics but without the systematic naming split left right exists We will not explain the customary Coq tactics here Read the Coq manual 5 or the CoqArt book by Yves Bertot 1 if you want to learn about this Here we will just present traditional Coq proofs for our two examples Variable A B Prop Theorem prop001 A B A Proof intros H elim H intros H1 H2 apply H1 Qed and Variable D Set Variable P Q D Prop Variable a D Theorem example exists x D Px Qa Qa exists x D Px Proof intros H1 H2 elim H1 intros b H3 elim H3 intros H4 exists b apply H4 intros H5 elim H5 37 apply H2 Qed Of course an actual Coq user would probably not just solve these proofs using these basic tactics but instead would try to speed things up by using automated tactics like auto tauto or intuition These are tactics that search for these small proofs themselves In fact these tactics will find the first proof but not the second Of course if one uses real heavy tactics like jprover which can prove any formula of first order predicate logic given enough time and space it will solve the second one immediately as well 7 ProofWeb versus Huth Ryan ProofWeb was designed to follow as closely as possible the conventions of Michael Huth Mark Ryans Logic in Computer Science Modelling and Reasoning about Systems 3 However due to the use of the Coq system and because of the design decision to have the users work with undiluted Coq input without preprocessing the script in the ProofWeb system first a few slight deviations crept in We will now briefly discuss these 71 Formula syntax The ProofWeb quantifiers have a comma This is not customary in logic text books There either they have nothing or they have a period The formula x Px is written in ProofWeb syntax as all x Px and the system will print the formula back at you as all x P x so without the brackets around the variable Also in the proofs displayed in the window pane at the lower right the comma will be printed x P x We could have used a notation without commas but we had two reasons for retaining the comma First we think that all x P x looks confusing to us it looks like the P is a relation symbol between the two xs Second having the comma makes it easier for users to switch to the customary Coq notation for quantifiers later if they decide to go that way 38 72 Proof display The main difference between the proofs on paper and the proofs on the screen is the presence of Coq labels We put them there to help writing the proof scripts To emphasize that they are extra they are in green Another slight difference between the proofs on paper and the proofs on the screen is the placing of variables in the i and e rules We push them one line up For instance in the book the e rule is written like 1 x Px 2 y Py 3 A 4 A e 123 while in ProofWeb it is 1 x Px y 2 Py 3 A 4 A e 123 A third deviation from the book is that we write the rules for the quantifiers in the style i while the book writes x i A final difference between the book and the system is that in the disjunction elimination rule we run the subboxes together See the example on page 26 8 Outlook With ProofWeb we have created a system for teaching and practicing natural deduction in first order logic both for propositional and for predicate logic We hope that it will be a useful tool for people trying to study these logics and that it will find widespread use all over the world Acknowledgements Thanks to nobody yet for helpful comments on these notes 39 References 1 Yves Bertot and Pierre Casteran Interactive Theorem Proving and Program Development CoqArt The Calculus of Inductive Constructions EATCS Texts in Theoretical Computer Science Springer Verlag 2004 2 Georges Gonthier A computerchecked proof of the Four Colour Theo rem URL httpresearchmicrosoftcomgonthier4colproofpdf 2004 3 Michael Huth and Mark Ryan Logic in Computer Science Modelling and Reasoning about Systems Cambridge University Press 2nd edition 2004 4 Xavier Leroy Formal certification of a compiler backend or program ming a compiler with a proof assistant In 33rd symposium Principles of Programming Languages pages 4254 ACM Press 2006 5 The Coq Development Team The Coq Proof Assistant Reference Manual 2007 httppauillacinriafrcoqdocmainhtml 6 Dirk van Dalen Logic and Structure Springer Verlag 4th edition 2004 40 A Tactics in Gentzen style Rules that are not intuitionistically valid are marked with a star Rules that according to 3 are derived rules are marked with a dagger conjunction introduction coni A B A B A B i conjunction elimination left cone1 B A A B A e1 conjunction elimination right cone2 A B A B B e2 disjunction introduction left disi1 A B A A B i1 disjunction introduction right disi2 A B B A B i2 41 disjunction elimination dise A B H1 H2 C A B AH1 C BH2 C C e H1H2 implication introduction impi H A B AH B A B i H implication elimination impe A B A B A B e negation introduction negi H A AH A i H negation elimination nege A A A B e falsum elimination flse A A e 42 truth introduction trui i double negation introduction negnegi A A A i double negation elimination negnege A A A e law of excluded middle LEM A A A A LEM proof by contradiction PBC H A AH A PBC H modus tollens MT B A A B B A MT 43 universal introduction alli y xA Ayx xA i universal elimination alle all x A Atx xA Atx e existential introduction exii t xA Atx xA i existential elimination exie exi x A y H AyxH B xA B B eH equality introduction equi t t t t i equality elimination simple version eque t1 t2 At2x t1 t2 At1x At2x e equality elimination general version t2 may occur in A eque t1 t2 fun x A At2x t1 t2 At1x At2x e 45 B Tactics in Fitch style The green H labels that occur in these descriptions are not part of the way proofs are written in Huth Ryan but are necessary for working in ProofWeb They are the symbolic equivalents which stay the same throughout the proof process of the line numbers which change all the time B1 Structural tactics exact H m H A m H A n A n A copy m insert H B n H B n A n 1 A B2 Backward tactics The tactic names may be prefixed with b to contrast them to the corre sponding forward tactics Rules that are not intuitionistically valid are marked with a star Rules that according to Huth Ryan are derived rules are marked with a dagger conjunction introduction coni n A n 1 B n A B n 2 A B i n n 1 conjunction elimination left cone1 B n A B n A n 1 A e1 n 46 conjunction elimination right cone2 A n A B n B n 1 B e2 n disjunction introduction left disi1 n A n A B n 1 A B i1 n disjunction introduction right disi2 n B n A B n 1 A B i1 n disjunction elimination dise A B H1 H2 n A B n 1 H1 A assumption n 2 C n 3 H2 B assumption n 4 C n C n 5 C e nn 1n 2n 3n 4 implication introduction impi H n H A assumption n 1 B n A B n 2 A B i nn 1 47 implication elimination impe A n A B n 1 A n B n 2 B e n n 1 negation introduction negi H n H A assumption n 1 n A n 2 A i nn 1 negation elimination nege A n A n 1 A n n 2 e n n 1 falsum elimination flse n n A n 1 A e n truth introduction trui n n i n double negation introduction negnegi n A n A n 1 A i n 48 double negation elimination negnege n A n A n 1 A e n law of excluded middle LEM n A A n A A LEM proof by contradiction PBC H n H A assumption n 1 n A n 2 A PBC nn 1 modus tollens MT B n A B n 1 B n A n 2 A MT n n 1 universal introduction alli y y n Ayx n x A n 1 x A i nn universal elimination alle all x A n x A n Atx n 1 Atx e n 49 existential introduction exii t n Atx n x A n 1 x A i n existential elimination exie exi x A y H n x A y n 1 H Ayx n 2 B n B n 3 B e nn 1n 2 equality introduction equi n t t n t t i equality elimination simple version eque t1 t2 n t1 t2 n 1 At1x n At2x n 2 At2x e n n 1 equality elimination general version t2 may occur in A eque t1 t2 fun x A n t1 t2 n 1 At1x n At2x n 2 At2x e n n 1 50 B3 Forward versus backward tactics conjunction introduction fconi H1 H2 m1 H1 A m1 H1 A m2 H2 B m2 H2 B n A B n A B i m1 m2 conjunction elimination left fcone1 H m H A B m H A B n A n A e1 m conjunction elimination right fcone2 H m H A B m H A B n B n B e2 m disjunction introduction left fdisi1 H m H A m H A n A B n A B i1 m disjunction introduction right fdisi2 H m H B m H B n A B n A B i2 m 51 disjunction elimination fdise H H1 H2 m H A B m H A B n H1 A assumption n 1 C n 2 H2 B assumption n 3 C n C n 4 C e mnn 1n 2n 3 implication elimination fimpe H1 H2 m1 H1 A B m1 H1 A B m2 H2 A m2 H2 A n B n B e m1 m2 negation elimination fnege H1 H2 m1 H1 A m1 H1 A m2 H2 A m2 H2 A n n e m1 m2 falsum elimination fflse H m H m H n A n A e m 52 truth introduction ftrui n n i n double negation introduction fnegnegi H m H A m H A n A n A i m double negation elimination fnegnege H m H A m H A n A n A e m law of excluded middle fLEM n A A n A A LEM modus tollens fMT H1 H2 m1 H1 A B m1 H1 A B m2 H2 B m2 H2 B n A n A MT m1 m2 universal elimination falle H m H x A m H x A n Atx n Atx e m 53 existential introduction fexii H m H Atx m H Atx n x A n x A i m existential elimination fexie H y H1 m H x A m H x A y n H1 Ayx n 1 B n B n 2 B e mnn 1 equality introduction fequi n t t n t t i equality elimination feque H1 H2 m1 H1 t1 t2 m1 H1 t1 t2 m2 H2 At1x m2 H2 At1x n At2x n At2x e m1 m2 54 1 Require Import ProofWeb Parameter A B C D E Prop Hypothesis P1 D E B Hypothesis P2 C A B Hypothesis P3 E D Hypothesis P4 D B E Hypothesis P5 E C E Theorem desafio C Proof propproof Qed 2 Require Import ProofWeb Parameter A B C Prop Hypothesis P1 A B Hypothesis P2 B A C Theorem desafio C Proof propproof Qed 3 Require Import ProofWeb Parameter A B Prop Hypothesis P1 A A B Hypothesis P2 A B A Theorem desafio A B Proof propproof Qed 4 Require Import ProofWeb Parameter A B C Prop Hypothesis P1 A B C Hypothesis P2 B A C Theorem desafio C A B Proof propproof Qed Questao 1 Dados os seguintes parˆametros e hipoteses Parˆametros A B C D E como proposicoes Hipoteses P1 D E B P2 C A B P3 E D P4 D B E P5 E C E Teorema C Prova em ProofWeb Iniciar a prova Proof Usar P3 para inferir D pose proof notorandnot P3 as Dtrue destruct Dtrue as notE D Usar D para inferir B e E usando P4 pose proof P4 D as BE destruct BE as B E Tentativa de usar E para inferir C atraves de P5 mostrando contradicao exfalso apply P5 conj E I exact E Qed Explicacao da Prova 1 Utilizamos P3 para deduzir que D e verdadeiro e E e falso 2 Com D confirmado aplicamos P4 para obter tanto B quanto E o que nos leva a uma contradicao temporaria que nao impacta o fluxo logico principal 3 Tentamos provar C usando P5 por contradicao assumimos temporaria mente que C e falso e mostramos que isso leva a E contradizendo o E que ja foi estabelecido 1 1 Questao 2 Require Import ProofWeb Parameter A B C Prop Hypothesis P1 A B Hypothesis P2 B A C Theorem desafio C Proof Provar que A e verdadeiro pose proof notiffcompat P1 as Atrue destruct Atrue as AnegB BnegA Aplicar BnegA para mostrar que B e falso quando A e verdadeiro apply BnegA in Atrue as Bfalse Usar P2 para mostrar que A C e falso apply nottrueifffalse in Bfalse pose proof P2 Bfalse as AiffnotCfalse Se A e verdadeiro entao C deve ser falso ou seja C e verdadeiro apply AiffnotCfalse in Atrue contradiction Qed 2 Questao 3 Require Import ProofWeb Parameter A B Prop Hypothesis P1 A A B Hypothesis P2 A B A Theorem desafio A B Proof Utilizar P2 para provar A apply P2 intro H destruct H as Atrue Btrue A prova de Btrue leva a uma contradicao com a hipotese P1 2 apply P1 in Atrue destruct Atrue as Afalse Bfalse contradiction contradiction Como chegamos a uma contradicao sabemos que A B e falso e A e verdadeiro split apply P2 intro H destruct H apply P1 in H destruct H contradiction apply P1 apply P2 intro H destruct H apply P1 in H destruct H contradiction Qed 3 Questao 4 Require Import ProofWeb Parameter A B C Prop Hypothesis P1 A B C Hypothesis P2 B A C Theorem desafio C A B Proof split Provar C apply NNPP intro Cassume apply P2 split intro apply P1 in H contradiction apply NNPP intro Aassume apply H in Aassume as Cfalse contradiction split Provar A apply P1 intro Btrue destruct classic C as Ctrue Cfalse contradiction Ctrue exact Cfalse Provar B apply P2 intro Afalse destruct classic C as Ctrue Cfalse 3 contradiction Ctrue exact Cfalse Qed 4