Home

ETPS User`s Manual - Pages on gtps

Contents

1. 56 49 FORALL x A S OA x IMPLIES E OA x Defn 54 lt 8 gt idef 92 49 FORALL x A S OA x IMPLIES D OA INTERSECT E OA x PLAN16 lt 9 gt P 55 49 FORALL x A S OA x IMPLIES D OA x Defn 53 56 49 FORALL x A S OA x IMPLIES E OA x Defn 54 92 49 FORALL x A S OA x IMPLIES D OA INTERSECT E OA x PLAN16 We have to get rid of the universal quantifier but we have to be careful to give our variable the right type namely a lt 10 gt ui 55 D2 LINE Instantiated Line 57 gt t GWFF Substitution Term No Default gt x A 57 49 S OA x A IMPLIES D OA x UTE D5 lt l gt ui 56 D2 LINE Instantiated Line 58 gt Let s use the editor to extract the variable t GWFF Substitution Term No Default gt ed 56 lt Edl gt a x A Ed2 ok 58 49 S OA x A IMPLIES E OA x UI x 56 lt 2 gt ugen 91 49 S OA x A IMPLIES D OA INTERSECT E OA x PLAN19 lt 3 gt deduct 59 49 59 S OA x A Hyp 90 49 59 D OA INTERSECT E OA x A PLAN20 lt 4 gt idef 89 49 59 D OA x A AND E OA x PLAN21 lt 5 gt P 55 49 FORALL x A S OA x IMPLIES D OA x Defn 53 56 49 FORALL x A S OA x IMPLIES E OA x Defn 54 57 49 S OA x A IMPLIES D OA x UTi SD 58 49 S OA x A IMPLIES E OA x UI
2. 100 FORALL x FORALL y P x y IMPLIES Q x x IMPLIES FORALL z P a z AND P b z IMPLIES Q a a AD OQO b b PLANI This example does not involve an existential quantifier but has a more complicated structure Since our theorem is an implication we use the deduction theorem again right away lt 2 gt deduct P3 LINE Line with Implication 100 gt 1 1 FORALL x FORALL y P x y IMPLIES Q x x Hyp 99 1 FORALL z P a z AND P b z IMPLIES Q a a AND Qb b PLAN2 Note that we used to specify that we want to choose the defaults for the remaining arguments It is clear that we need to instantiate x with a and b We do this in the next two steps lt 3 gt ui D1 LINE Universally Quantified Line 1 gt Some defaults could not be determined t GWFF Substitution Term No Default gt a 2 1 FORALL y P a y IMPLIES Qaa UES sal We again used but ETPS couldn t determine all the defaults so it prompted us again for the arguments for which it couldn t figure the defaults lt 4 gt ui D1 LINE Universally Quantified Line 2 gt 1 D2 LINE Instantiated Line 3 gt t GWFF Substitution Term No Default gt b 3 1 FORALL y P b y IMPLIES Q b b UIs 6 1 The planned line 99 is again an implication which suggests using DEDUCT again lt 5 gt deduct P3 LINE Line with Implication 99 gt D2 LINE Line with Conclusion 98 gt H1 LINE Line with Hypothesis 4 gt 4 1 4 FORALL z P a z AND P b z Hyp 98
3. Note that EXISTS for example was typed in lower case but is always printed in upper case lt 2 gt deduct P3 LINE Line with Implication 100 gt D2 LINE Line with Conclusion 99 gt H1 LINE Line with Hypothesis 1 gt 1 1 EXISTS x FORALL y P x y Hyp 99 1 FORALL y EXISTS x P x y PLAN2 DEDUCT is often the right way to start the proof of an implication Note that the defaults were just what we wanted anyway so we selected them by simply typing lt Return gt lt 3 gt ugen P2 LINE Universally Quantified Line 99 gt PI LINE Line with Scope of Universal Quantifier 98 gt 98 T EXISTS x P x y PLAN3 lt 4 gt rulec P4 LINE Conclusion without Additional Hypothesis 98 gt D1 LINE Existentially Quantified Line 1 gt D3 LINE Conclusion with Additional Hypothesis 97 H2 LINE Hypothesis with Chosen Variable 2 gt y GWFF Chosen Variable Name No Default gt x 2 1 2 FORALL y P x y Choose x 97 L Zoi EXISTS x P x y PLAN5 We now doa P note that this is not a control character to see what still has to be proven lt 5 gt P 2 1 2 FORALL y P x y Choose x 97 1 2 1 EXISTS x P x y PLAN5 33 ETPS User s Manual lt 6 gt ui 2 D2 LINE Instantiated Line 3 gt t GWFF Substitution Term No Default gt y 3 2 1 3 P x y UIs y 2
4. 54 Appendix III Appendix ITI Wif Operations This is a list of those wffops mentioned in Chapter 3 you can get a complete list of wffops by typing ENVIRONMENT and then WFFOP IIL1 Equality between Wffs WFFEQ AB wffl wff2 Tests for equality modulo alphabetic change of bound variables WFFEQ AB BETA w ffl wff2 Tests for equality modulo alphabetic change of bound variables and beta conversion WFFEQ AB ETA wffl wff2 Tests for equality modulo alphabetic change of bound variables and eta conversion WFFEQ AB LAMBDA wffl wff2 Tests for equality modulo alphabetic change of bound variables and both beta and eta conversion WFFEQ DEF wffl wff2 Tests for equality modulo definitions lambda conversion and alphabetic change of bound variables II 2 Predicates on Wffs FREE FOR term var inwff Tests whether a term is free for a variable in a wff IS VARIABLE gwff Tests whether a wff is a logical variable NON ATOMIC gwff Tests whether a wff is not atomic that is negated quantified or the result of joining two wffs with a binary connective NOT FREE IN gvar inwff Tests whether a variable is not free in a wff NOT FREE IN HYPS gvar Tests whether a variable is not free in the set of hypotheses of a rule R PRIME RESTR terml wffl term2 wff2 Verifies that wff2 follows from wffl by Rule R using equality term term2 SAME MODULO EQUALITY wffl wff2 terml term
5. Will list all available commands LIST RULES Will list all the available inference rules PROBLEMS Lists all exercises available in ETPS and shows which are practice exercises for which ADVICE is available Also lists theorems which can be asserted with the ASSERT command NEWS Will list all bugs fixed changes improvements et cetera The most recent ETPS news items are announced whenever you start ETPS REMARK string Will mail the string to the teacher or will include it as a comment in a recordfile created in the teacher s directory 2 2 Starting and Finishing EXERCISE label Set up the proof outline to attempt the proof of exercise label from the logic text PROVE gwff0 label line Similar to EXERCISE but lets you prove your own wff label is the name of the proof line is number of the last line of the proof i e the number of the line which will assert the theorem PROOF LIST Gives a list of all the completed or partially completed proofs in memory any of which may be RECONSIDERed RECONSIDER label Allows you to return to a previous proof label is the name that you gave the proof when you originally started it using EXERCISE or PROVE all of the proofs that you have worked on in the current session with ETPS may be RECONSIDERed a CLEANUP Deletes in the current completed proof unnecessary lines and redundant lines introduce
6. R w w D dx dy Rx yA Qy xDdVzQ2zz2 Vx dy Q x yDP x A Vv Ju Q u y A VW Vz wv z2 530 zw vV z2 2 gt Vz P z Vz dx Vy P x yvQ xz gt Vy 4ax P xX yVQxy dx Vy P xAQyDOxvVPy dx dy Vu P x yzDPux x dx Vy P x DOxvPBy Vx dy F x y A dx Ve dn Vw S nw Vy Vz FayaAFbz2DDyzejloD ye D D w x e A Ve dd Va Vb Dabdb dy Ve dm Vw S mw D Vz F wzoDD IV 3 Higher Order Logic X5200 X5201 X5202 X5203 X5204 X5205 X5206 X5207 X5208 X5209 X5210 X5211 X5212 X5304 X5305 X5308 X5309 X5310 X5500 X6004 X6101 X6104 X6105 Xoo Yi Yon U Av v KV A KA OY OVA a V x vv y fo Xo Y Yol f XUB Y Lo Xp N Yp CBE XA EY yfe U Woop U S f w fy O Woop c N s 3 f w fo Xp Y Yol F KXUB Y fo Xp N Yp Ce Ex sty AS Vx S x V Pa x A S X V Qu x Vy P yvQy ee Da WO Dee x Az dy y xAZ y Yo VAZ By Y X AZ x Az Ax kI SAN a Sol D Mi A n a A E VS Ge ME E E E A a Age f oua ce J 3 gop VPog 3x P Xx D p j pl 2 Vx dyg roa X Y df Vx r x f x SIN Vp YeI hp hqg2op 1q VX Bop VE dy rz y3 AE rop Verh fe x eD J 5 5 08 VP op p 2D p 3 VPig aay P x DPI Pl D V VO f J x f x gx g dan f x gx DE Q E sooo Xp T Ya Two o 01 Jian Ioa i g Ax X A DESAN g g x ME VWA Ax y fDfy s This is a lemma for X6106 You may need to ASSERT DESCR or T5310 or T5310A Vi Dy NAT n D Vg n q gt Aj a VESI E QgA AK L
7. 1 3 History Substitutions 1 4 Aliases Appendix II More Editor Commands II 1 Labels II 2 Basic Abbreviations II 3 Lambda Calculus II 4 Quantifier Commands II 5 Embedding Commands IL 6 Changing and Recursive Changing Commands II 7 Miscellaneous II 8 Wellformedness II 9 Saving and Recording Wffs Appendix III Wff Operations IIL 1 Equality between Wffs III 2 Predicates on Wffs III 3 Substitution III 4 Basic Abbreviations 111 5 Lambda Calculus II 6 Negation movers Appendix IV Theorems and Exercises IV 1 Book Theorems IV 2 First Order Logic IV 3 Higher Order Logic Index ii
8. 1 4 Q aaANDQDbD PLANS We now use universal instantiation again this time to distribute the universal quantifier over a conjunction lt 6 gt ul D1 LINE Universally Quantified Line 4 gt D2 LINE Instantiated Line 5 gt 35 ETPS User s Manual t GWFF 5 Aji Substitution Term Pay lt 7 gt help econj DI H D2 H D3 H A AND B A IB Transformation p AND P b y HELP command No Default gt y Just to make sure ECONJ is the inference rule we want let s call the Conj DI Conj DI p DI ss gt pp D2 D3 ss Yes that s what we need Let s look at the current planned line and its support lines ES Q xX X FS Q x x 1 8Xeconj D1 LINE sine with Conjunction 5 gt D3 LINE Line with Right Conjunct 7 gt D2 LINE Line with Left Conjunct 6 gt 6 1 4 Pay 7 1 4 Pby lt 9 gt pplan PLINE PLINE Print planned line 98 gt 1 T FORALL x FORALL y P x y IMPLI 2 1 FORALL y P a y IMPLIES Q aa 3 1 FORALL y P b y IMPLIES Q bb 4 1 4 FORALL z P a z AND P b z 6 1 4 Pay 7 1 4 Pby 98 1 4 Q aa AND Obb lt 10 gt iconj P3 LINE Line with Conjunction 98 gt P2 LINE Line with Right Conjunct 97 gt P1 LINE Line with Left Conjunct 52 gt 52 1 4 Qaa 97 1 4
9. 54 57 49 S OA x A IMPLIES D OA x UI X oS 58 49 S OA x A IMPLIES E OA x UIL X 56 59 49 59 S OA x A Hyp 89 49 59 D OA x A AND E OA x Rulep 59 58 57 90 49 59 D OA INTERSECT E OA x A Defn 89 91 49 S OA x A IMPLIES D OA INTERSECT E OA x Deduct 90 92 49 FORALL x A S OA x IMPLIES D OA INTERSECT E OA x Ugen x 91 93 49 S OA SUBSET D OA INTERSECT E OA Defn 92 94 49 POWERSET D OA INTERSECT E OA S OA Defn 93 95 POWERSET D OA INTERSECT POWERSET E OA S OA IMPLIES POWERSET D INTERSECT E S Deduct 94 96 POWERSET D OA INTERSECT E OA S OA IMPLIES POWERSET D INTERSECT POWERSET E S AND POWERSET D INTERSECT POWERSET EJ S IMPLIES POWERSET D INTERSECT E S Conj 48 95 97 POWERSET D OA INTERSECT E OA S OA EQUIV POWERSET D INTERSECT POWERSET E S ImpEquiv 96 98 POWERSET D OA INTERSECT E OA S OA POWERSET D INTERSECT POWERSET E S Ext 97 99 FORALL S OA POWERSET D OA INTERSECT E OA S POWERSET D INTERSECT POWERSET EJ S Ugen S 98 100 POWERSET D OA INTERSECT E OA POWERSET D INTERSECT POWERSET E Ext 99 lt 9 gt exit 45 ETPS User s Manual 46 Appendix I Appendix I menities ETPS incorporates several features of the Unix C shell csh top level These features include various control characters command sequences a history mechanism and aliases L1 Control characters for Unix If you are running
10. Flag 10 ROOFW ACTIVE NOS Flag 10 ROOFW ALL Flag 10 ROVE System Command 1 9 33 35 PS Editorcommand 15 PSTATUS System Command 3 10 PT Editorcommand 15 PULL NEG Editor command 16 PULLNEG Inference Rule 19 22 PUSH System Command 4 PUSH NEG Editor command 16 PUSH NEGATION 56 PUSHNEG Inference Rule 19 23 31 PW System Command 12 PWSCOPE System Command 12 PWTYPES System Command 13 UU UU tO voIouvsvovo Vy UD g Quitting 63 See also END PRFW EXIT LEAVE OK R Editorcommand 15 R PRIME RESTR 55 RECONSIDER System Command 9 RECURSION 41 ED Editorcommand 52 EM Editor command 54 EMARK System Command 9 UMBERALL System Command 13 ESTORE WORK System Command 11 13 ESTOREPROOF System Command 2 11 UME SAVE System Command 2 11 UME WORK System Command 2 EW System Command 14 EW EQUIV Editor command 16 IGHTMARGIN Flag 14 P Editorcommand 16 PALL Editorcommand 16 ULEC Inference Rule 19 23 31 ULEP Inference Rule 18 19 30 32 44 ULEP DELUXE Function 19 ULEP MAINEN Flag 19 RULEP SIMPLE Function 19 RW Editor command 51 D D UVU zal Z Ae nn ti DD D Ia S 55 SAME Inference Rule 18 20 SAME MODULO EQUALITY 55 SAVE Editor command 54 SAVE WORK System Command 2 3 7 11 31 SAVEPROOF System Command 2 11 SCRIBEPROOF System Command 12 SCRIPT System Command 3 11 SETEQUIV 40 ETFLAG System Command 14 ETINTERSECT 40 ETUN
11. Qb b lt 1 gt mp D2 LINE Line with Implication 6 gt 2 D3 LINE Line with Succedent of Implication 30 gt 52 PI LINE Line with Antecedent of Implication 29 gt 29 1 4 FORALL y Pay lt 2 gt pplan PLINE PLINE Print planned line 29 gt 1 1 FORALL x FORALL y P x y IMPLI 3 I FORALL y P b y IMPLIES Q b b 4 1 4 FORALL z P a z AND P b z 6 1 4 Pay 7 1 4 Pby 29 1 4 FORALL y Pay lt 3 gt ugen P2 LINE Universally Quantified Line 29 P1 LINE Line with Scope of Universal Quantifier 28 gt 6 lt 4 gt pplan PLINE PLINE Print planned line 97 gt 36 UI y 4 Conj 5 Conj 5 Hyp UI al UI by Hyp Cony 5 Conjt s PLAN5 PLAN9 PLAN8 PLANII Hyp UI b 1 Hyp Conj 5 Conj 5 PLANII Chapter 4 Sample Proofs 1 1 FORALL x FORALL y P x y IMPLIES Q x x Hyp 3 iL FORALL y P b y IMPLIES Q b b VE s bwl 4 1 4 FORALL z P a z AND P b z Hyp 6 1 4 Pay Eonj s 7 1 4 Pby Conj 5 29 1 4 FORALL y Pay UGen y 6 52 1 4 Qaa MP 29 2 97 1 4 bb PLAN8 lt 5 gt mp D2 LINE Line with Implication 52 gt 3 D3 LINE Line with Succedent of Implication 75 gt 97 PI LINE Line with Antecedent of Implication 74 gt 74 1 4 FORALL y P by PLAN14 lt 6
12. Replaces the current wff by the wff supplied A Edn gt SUBST term var Substitute a term for the free occurrences of variable in a gwff Bound variables may be renamed using the function in the global variable REN VAR FN lt Edn gt SUBSTYP typevar typesym Substitute typevar with typesym 2 12 6 Negation movers lt Edn gt NEG Negates current wff erasing double negations lt Edn gt NNF Return the negation normal form of the given wff lt Edn gt PULL NEG Pulls negations out one level lt Edn gt PUSH NEG Pushes negation through the outermost operator or quantifier 16 3 Inference Rules 3 1 How to Read Inference Rules The user works within a proof outline which is a sequence of lines Each line is either a hypothesis a consequence of lines with lower numbers or an unjustified planned line In general a line of the proof has the following form n H H assertion justification wffs l monn li n is a number which serves as a label for the line Each of the H s is the number of a line asserting a hypothesis stands for the turnstyle and l are the numbers of the lines which are used to justify this line Every description of a logical inference rule states that certain lines of a proof may be inferred from certain other lines provided that certain restrictions are satisfied and notes the change which the rule effects on the proof status see Section 2 5 Inferen
13. Rule to infer a line from one which is equal up to lambda conversion using eta rule but NOT beta rule and alphabetic change of bound variables D1 H FA D2 H E B Beta Rule D1 Restrictions WFFEQ AB ETA A B Transformation pp D1 ss gt pp D2 ss Rule to put an inferred line into Lambda normal form using both beta and eta conversion D1 H t A D2 H LNORM A Lambda DI Transformation pp D1 ss gt pp D2 ss LCONTR BETA LCONTRX LEXPD Rule to put an inferred line into beta normal form D1 H tA D2 H LNORM BETA A Lambda DI Transformation pp D1 ss gt pp D2 ss ETA Rule to put an inferred line into eta normal form D1 H tA D2 H LNORM ETA A Lambda DI Transformation pp D1 ss gt pp D2 ss Rule to put a planned line into Lambda normal form using both beta and eta conversion P1 H LNORM A P2 H A Lambda PI Transformation P2 ss gt P1 ss 26 Chapter 3 Inference Rules LEXPD BETA Rule to put a planned line into beta normal form P1 H LNORM BETA A P2 H A Lambda PI Transformation P2 ss gt P1 ss H EXPD ETA Rule to put a planned line into eta normal form P1 H LNORM ETA A P2 H A Lambda PI Transformation P2 ss gt P1 ss 27 ETPS User s Manual 28 4 Sample Proofs The following are transcripts of proo
14. foo work enter afs andrew usrlil adn0z foo work KEKE KKK KKK KKK KK KKK KKK KKK KKK KKK KK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KK KK KK KKK KK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK ANNOUNCING as well ETPS can now be run on the sun3_35 workstation type as on the Microvax The more memory on the machine the faster ETPS will run check the amount of memory available on a Sun 3 type etc dmesg grep avail in your typescript KKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK To Loading changes done Loading afs andrew cmu edu math etps etps ini Finished loading afs andrew cmu edu math etps etps ini If you are using ETPS in an environment where proofwindows are available issue the BEGIN PRFW command now to open proofwindows lt l gt exercise x2108 100 FORALL x EXISTS y P x IMPLIES P y PLANI Since this theorem is universally quantified we will first use universal generalization Note that to accept the defaults that ETPS offers we just hit a Return lt 2 gt ugen P2 LINE Universally Quantified Line 100 gt PI LINE Line with Scope of Universal Quantifier 99 gt 99 EXISTS y P x IMPLIES P y PLAN2 As we will see later the justification of line 100 has been changed from PLAN1 to UGen which stands for universal generalization Now the formula we are trying to prove is existentially qu
15. restarting ETPS After your work has been restored by RESTORE WORK ETPS will continue to save subsequent work into the same file by appending it to the end If you would like to prevent that give the STOP SAVE command right after RESTORE WORK better yet use the EXECUTE FILE command When commands are read from a save work file most errors such as illegal arguments or logical mistakes are faithfully re executed since some of them have side effects Only Lisp errors will lead to an abort of the RESTORE WORK and the state of the proof will be the same as after the last correct command read from the file You may edit the save work file in Emacs to delete wrong commands or correct illegal arguments but you ll be skating on thin ice It s easy to make a mistake in editing the save work file and you may not be able to recover the proof you wanted to restore The inquisitive user may note that lines beginning with a semi colon are ignored when the proof is being restored There are several options you have when using this auto save feature You may switch off saving with the STOP SAVE command Also you can explicitly save into a different file with the SAVE WORK command To check whether your work is being saved use the system command PSTATUS You also have the option of keeping a complete record of the session including the system responses in a file If you want to prepare such a cop
16. 3 5 below ETPS User s Manual Suppose the proof originally contains the line P3 H A gt B PLAN4 and we apply the command lt n gt DEDUCT P3 H1 D2 Here e P3 stands for the planned line that you are trying to prove e H1 stands for the number of the line which asserts the new hypothesis the wff A in this case e D2 stands for the number of the new planned line whose assertion is B in this case After the rule is applied the proof will contain the lines H1 H A F A Hyp D2 H A B PLAN5 P3 A ADB Deduct D2 3 2 Quick Reference to Rules Here is a list of the most generally useful rules of inference available in ETPS for quick reference Some additional rules of inference may be found by typing or LIST RULES in ETPS See the page indicated for a precise description of each rule listed below You can also type HELP rule in ETPS The rules of inference in ETPS are applicable to both first order logic and higher order logic The user who is interested only in first order logic should ignore the rules for higher order logic Special Rules RULEP 19 Justify a line by Rule P ASSERT 20 Assert a theorem known to ETPS ADD HYPS 20 Weaken a line to include extra hypotheses DELETE HYPS 20 Delete some hypotheses from the given line Miscellaneous Rules HYP 20 Introduce a new hypothesis line into the proof outline LEMMA 20 Introduce a Lemma SAME 20 Use the fact that two lines are
17. Apa Ix p x 40 Successor One Finite u Natural No NC Recursion yi Chapter 5 Type Theory in ETPS SUCC A EV LE XP x A n At t x Ap t ONE SUCC Os FINITE Apa Fey NAT n A np MU Ap THAT x NAT x A p x A FORALIN y p y D x lt y AT Angon VE Pw ZERO A Yx P x D p SUCCo X D pn Ng Muso APop 2 Esoprep P RECURSION Magog AJo AN ey THAT m VWa W ZERO g A Vx Vy w x y D w SUCC z h x y Dwnm SIGMA1 LAP Ya Poa y UNITSET Ax Ay x y 5 1 3 Some Examples of Higher Order Wffs Here are some examples of higher order wffs The first line shows how the formula is printed in the logic book the second line shows how it could be entered into ETPS as a string and the third line shows how ETPS would print it with type symbols for example with the PWTYPES command Look at these carefully and make sure you understand how to type in wffs of higher order logic LOU JE Vs aou ouo oi o o1 df VS 9x S x D S f S EXISTS f FORALL S EXISTS x S x IMPLIES S f S EXISTS f I OI FORALL S OI EXISTS x I S x IMPLIES S f S Ax S x D S f S EXISTS f OI O OI FORALL S EXISTS x S x IMPLIES S f S EXISTS f OI O OI FORALL S O OI EXISTS x OI S x IMPLIES S f S df VS Ix S x D S f S EXISTS f FORALL S EXISTS x A S x IMPLIES S f S EXISTS f A OA FORALL S OA EXISTS x A S
18. First Order Logic X2106 Vx Rx DP x A Vx Qx DR x DVx P x vOxXx X2107 Raba Yx Vy Rx yD Ry KAQxXxy A Vu Vv Quvdguu l o5oQoa adnaQbb X2108 Vx dy P x DPy X2109 dx pA Q x pA FFOQXx X2110 dx R x A Vy Ry D4dzQy2z AV Vy Qx y DQ x x D Ax dy Q x ya Ry X2111 Vx dy P x y D VyQ x y A Vz dy Pz y D Vy Vx Oxy X2112 dv Yx P x v A Vx S x D Jy Q y x AV Vy P xyo2o OQx y D Ju S u X2113 Vy dw R y w A dz Vx P xD Rz x D Ax P x X2114 Vx R x b A Yy IZ Ry z DRaa y DJu Vv Ruv X2115 Vx dy P x y D Vz P z z A Vu dv P uvvMu A DOQ fuv A Ww Qw gt D M g w D Vu Jv P gu vA APuu X2116 Vx dy P x DR x g h y A P y A Vw P wD P g w A P h w D Vx P x D Jy RxyA AP y X2117 Vu Vv R u u R u v A Vw Vz R ww R z w D 4dx Rx xD VyRyy X2118 Vx PAQxV pARxX D Vx Q xv Vx Rx X2119 dy Vx P yDPx X2120 Vu Vv Vw PE uvvPBvw gt Jx Vy P xy X2121 Jv Vy dZ BPB ay h yl v Pv y fy DBPvy z X2122 dx Rx xODVy Ry yD du VveRuudRvyv X2123 dy P y gt Q x DIVW P y DQOYy X2124 dx P x D Q x Vx P x D 3x QO x X2125 dx Vy P x P y 4x P x Vy Py 57 ETPS User s Manual X2126 X2127 X2128 X2129 X2130 X2131 X2132 X2133 X2134 X2135 X2136 X2137 X2138 Vx P x dy P y Vx P x dy Py dx Vy P y P x D Vx P x v Vx P x Vx P x Vy P y 4x P x Vy Py dx Vy P x P yl dx Q x Vy Pyl dx Vy 0 x Q y 4dx P x Vy Q y Vx Pox Dwe dy O cy Vo Az og DB Oe 2 Vx P x Ddy Vx VzQxyzD Vz Pza Qyyz Vw
19. NIL L UOl 58 Appendix IV X6106 FINITE Ax T gt Jj X6201 Jra VS VY VZ Jw E X WA rxxA rxyoryzorxz 5D wooo Ya VYoa gg Wa RXWA RXXARXYDRY ZDRXZ X8030A g T A g L Vx g x Vesi TD BB 01 ol 59 60 0 Editor command 15 System Command 4 9 14 A Editor command 15 AB AB ABE AB A ABS ABU DD DV D xX Al Al Alias 7 A Al Al Editor command 15 Inference Rule 19 23 Inference Rule 19 23 ORM Editor command 51 BORT 4 URD Inference Rule 18 22 Inference Rule 19 23 HYPS Inference Rule 18 20 ICE System Command 1 9 13 LIAS System Command 9 49 40 THING Argument Type 5 Argument Types ANYTHING 5 BOOK THEOREM 6 BOOLEAN 5 E E E F XERCISE 6 XISTING LINE 5 XISTING LINELIST 6 ILESPEC 5 GVAR LIST 7 GVAR 6 GWFFO 6 GWFF 5 6 GWFFLIST 7 I NTEGER 5 LINE RANGE LIST 6 LINE RANGE 5 LINE 5 LINELIST 6 OCCLIST 6 P P P S S T T LINE 5 OSINTEGER 5 RACTICE 6 TRING 5 YMBOL 5 EST PROBLEM 6 YPESYM 6 YESNO 5 ASRB Editor command 53 ASRB Editor command 53 ASS ASS ASS ASS ASS BEG ERT Inference Rule 18 20 L Editor command 53 L Editor command 53 R Editor command 53 R Editor command 53 N PRFW System Command 1 10 BETA Inference Rule 26 BOO BOO CAS CHE THEOREM Argument Type 6 LEAN Argument Type 5 ES Inference Rule 18 20 CK STRUCTURE System Command 13 CLEANUP S
20. S PLAN2 lt 3 gt ugen 98 POWERSET D OA INTERSECT E OA S OA POWERSET D INTERSECT POWERSET E S PLAN3 lt 4 gt ext 0 P2 LINE ine with Equality 98 gt PI LINE Line with Equivalence 97 gt 97 POWERSET D OA INTERSECT E OA S OA EQUIV POWERSET D INTERSECT POWERSET E S PLAN4 5 implics equiv P2 LINE Line with Equivalence 97 PI LINE Line with Implications in Both Directions 96 gt 96 POWERSET D OA INTERSECT E OA S OA IMPLIES POWERSET D INTERSECT POWERSET E Si AND POWERSET D INTERSECT POWERSET E S IMPLIES POWERSET D INTERSECT E S PLANS 42 Chapter 5 Type Theory in ETPS lt 6 gt iconj 48 POWERSET D OA INTERSECT E OA S OA IMPLIES POWERSET D INTERSECT POWERSET E S PLANT 95 POWERSET D OA INTERSECT POWERSET E OA S OA IMPLIES POWERSET D INTERSECT E S PLAN6 In this example we will prove only line 95 It may be a a good exercise to try to prove line 48 lt 7 gt subproof PLINE PLINE Line to prove 48 gt 95 lt 8 gt deduct 49 49 POWERSET D OA INTERSECT POWERSET E OA S OA Hyp 94 49 PO
21. We are closing in You can now see that line 97 follows immediately from line 3 by existential generalization Therefore we use the EGEN command and display the proof with the PALL command lt 7 gt egen P2 LINE Existentially Quantified Line 97 gt P1 LINE Line to be Existentially Generalized 96 gt 3 t GWFF Term to be Generalized Upon No Default gt x lt 8 gt pall 1 1 EXISTS x FORALL y P x y Hyp 2 1 2 FORALL yP x y Choose x 3 Zili 21 P Xx y ULS y 2 97 1 2 EXISTS x Pxy EGen x 3 98 1 l EXISTS x P x y RuleC 1 97 99 1 FORALL y EXISTS x P x y UGen y 98 100 EXISTS x FORALL y P x y IMPLIES FORALL y EXISTS x P x y Deduct 99 This is what our completed proof looks like Let s make sure that we are done and print the proof into a file before exiting ETPS lt 9 gt done You completed the proof Since this is not an assigned exercise the score file will not be updated lt 10 gt texproof FILENAME FILESPEC Filename examplel tex gt Written fil xamplel tex lt 10 gt exit 4 3 Example 3 gt etps etps for issar Version from Saturday September 23 1989 at 5 59 15 c Copyrighted 1988 by Carnegie Mellon University All rig KKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK WARNING Be sure that you when you begin ETPS your curre one for which you have write access 9 your KEKE KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KK KK KKK KKK KKK KKK KKKKEKK KKKKKKKKKKKKKKKKKKKKK
22. Y x A P2 H Vx A Restrictions FREE FOR y x A NOT FREE IN y A Transformation P2 ss gt P1 ss Rule of Existential Generalization P1 H H LCONTR Ax A tal P2 H Ix A Transformation P2 ss gt P1 ss Rule C D1 H E Ix B H2 H H2 LCONTR Ax BI Yal D3 H H2 FA P4 H FA Restrictions IS VARIABLE Ya NOT FREE IN HYPS Ya NOT FREE IN y 9x B NOT FREE IN y A Transformation P4 D1 ss gt D3 H2 ss Rule of Universal Generalization P1 H FA P2 H E Vx A Restrictions NOT FREE IN HYPS Xa Transformation P2 ss gt P1 ss 23 Neg DI AB AB AB EGen Choose Rulec UGen ie a DI x DI DI PI Pl D3 Pl ETPS User s Manual UI Rule of Universal Instantiation D1 H E Vx A D2 H H LCONTR Ax A tal I S DI Transformation pp D1 ss gt pp D2 DI ss 3 8 Substitution Rules SUBSTITUTE Rule to substitute a term for a variable D1 H HA D2 H r S t X A Subst t x DI Restrictions NOT FREE IN HYPS x FREE FOR t x A Transformation pp DI ss gt pp D2 ss D1 3 9 Equality Rules EXT Rule of Extensionality P1 H VIE x Ga X P2 H EE Gg Ext Pl Transformation P2 ss gt P1 ss EXT 0 Rule to derive an equality at type o from an equivalence
23. from the given line This may leave the given line as a planned line The user is given the option of also deleting some hypotheses from lines after the given line If possible the user is given the option of deleting some hypotheses from lines before the given line so that the given line does not become a planned line 3 4 Miscellaneous Rules HYP Introduce a new hypothesis line into the proof outline 81 H1 HA P2 H F B Transformation P2 ss gt P2 H1 ss LEMMA Introduce a Lemma P1 H FA P2 H E B Transformation P2 ss gt P2 P1 ss P1 ss SAME Use the fact that two lines are identical to justify a planned line D1 H FA P2 H tA Transformation P2 DI ss gt 3 5 Propositional Rules CASES Rule of Cases D1 H HA YB H2 H H2 A P3 H H2 PC 84 H H4 B P5 H H4 FC P6 4H Gs Transformation P6 D1 ss gt P3 H2 ss P5 H4 ss 20 Same as Case 1 Case 2 Hyp D1 D1 D1 Cases D1 P3 P5 DEDUCT The deduction rule H1 4H H1 t A D2 4H H1 E B P3 H FA DB Transformation P3 ss gt D2 H1 ss DISJ IMP Rule to replace a disjunction by an implication D1 H bt A v B D2 H EA DB Transformation pp D1 ss gt pp D2 ss ECONJ Rule to eliminate a conjunction by inferring its two conjuncts D1 H HA AB D2 H HA D3 H B Transformation pp D1 ss gt pp D2 D3 ss EQUIV
24. gt ugen P2 LINE Universally Quantified Line 74 gt PI LINE Line with Scope of Universal Quantifier 73 gt 7 The proof is complete Let s look at the entire proof lt 7 gt pall 1 1 FORALL x FORALL y P x y IMPLIES Q x x Hyp 2 1 FORALL y P a y IMPLIES Q a UI al 3 1 FORALL y P b y IMPLIES Q b UI boul 4 1 4 FORALL z P a z AND P bz Hyp CS 4 1 Pay ANDP by UI y 4 6 1 4 Pay Con js 5 7 1 4 Pby Conj 5 29 1 4 FORALL y Pay UGen y 6 52 1 4 Qaa MP 29 2 74 1 4 FORALL y P by UGen y 7 97 1 4 Q bb MP 74 3 98 1 4 Q a a AD O bb Cony 02 97 99 1 FORALL z P a z AND P b z IMPLIES Qaa AND QO bbD Deduct 98 100 FORALL x FORALL y P x y IMPLIES Q x x IMPLIES FORALL z P a z AND P b z IMPLIES Q a a AND Q Db Deduct 99 We ll next use SQUEEZE to remove gaps from the proof structure We could also have used MODIFY GAPS 1 1 lt 9 gt squeeze Let s see how the proof looks now lt 10 gt pall 1 1 FORALL x FORALL y P x y IMPLIES Q x x Hyp 2 1 FORALL y P a y IMPLIES Qa a UT at 3 J FORALL y P b y IMPLIES Q b UI b 1 4 1 4 FORALL z P a z AND P b z Hyp 5 4 1 Pay ANDP by UI y 4 6 1 4 Pay Cony 5 7 1A BY Conj 5 8 1 4 FORALL y Pay UGen y 6 9 1 4 Qaa MP 8 2 10 1 4 FORALL yP by UGen y 7 ik 1 4 Qbb MP 10 3 12 1 4 QaaANDQDb Conj 9 11 13 1 FORALL z P a z AND P b z IMPLIES Q a a AND QO bD Deduct 12 14 FORALL x FORALL y P x y IMPLIES Q
25. identical to justify a planned line Propositional Rules CASES 20 Rule of Cases DEDUCT 21 The deduction rule DISJ IMP 21 Rule to replace a disjunction by an implication ECONJ 21 Rule to eliminate a conjunction EQUIV IMPLICS 21 Rule to convert an equivalence into twin implications ICONJ 21 Rule to introduce a conjunction IMP DISJ 21 Rule to replace an implication by a disjunction IMPLICS EQUIV 21 Rule to convert twin implications into an equivalence INDIRECT 21 Rule of Indirect Proof INDIRECTI 22 Rule of Indirect Proof using one contradictory line INDIRECT2 22 Rule of Indirect Proof using two contradictory lines MP 22 Modus Ponens Negation Rules ABSURD 22 From falsehood deduce anything 18 Chapter 3 Inference Rules ENEG 22 Eliminate a negation INEG 22 Introduce a negation PULLNEG 22 Pull out negation PUSHNEG 23 Push in negation Quantifier Rules AB 23 Rule to alphabetically change embedded bound variables ABE 23 Rule to change a top level occurrence of an existentially quantified variable ABU 23 Rule to change a top level occurrence of a universally quantified variable EGEN 23 Rule of Existential Generalization RULEC 23 RuleC UGEN 23 Rule of Universal Generalization UI 24 Rule of Universal Instantiation Substitution Rules SUBSTITUTE 24 Rule to substitute a term for a variable Equality Rules EXT 24 Rule of Extensionality EXT 0 24 Rule
26. information about the proofwindows type HELP BEGIN PREW BEGIN PREW Begin proofwindow top level open Current Subproof Current Subproof amp Line Numbers and Complete Proof windows END PRE W End proofwindow top level close all the proofwindows If you forget to use the END PRFW command before issuing the EXIT command to leave ETPS the proofwindows may not disappear To get rid of such a window put the cursor into it and hit C control C 2 5 The Current Subproof ETPS maintains a list which contains the status information for the current proof outline The status information consists of the planned lines lines not yet justified and the lines called sponsoring lines which ETPS thinks you may wish to use in the proof of the associated planned line The planned line which is the focus of current attention and its sponsoring lines constitute the Current Subproof This is displayed in the windows mentioned in Section 2 4 and can be printed on the screen by using the P command The following commands allow you to examine and modify the current subproof and the status information PSTATUS This will print the status information in the form Py bay eee pl ve Pa ft ewe fin where p Pm are the planned lines and the rest of each list are the sponsors for the planned line The first list corresponds to the current plan In addition it ll issue a message if you are currently saving work 10 Chapte
27. only means of identification available to ETPS is the userid of the account from which it is run It will credit all work to the owner of that account and to no other user Thus in order to receive credit for an exercise you must run ETPS from your own account Run it from a private directory so that the files which ETPS creates containing your proofs will not be accessible to others Start work on an exercise with the command EXERCISE exercise name see Section 2 2 Next construct a complete proof using the inference rules described in Chapter 3 However some of the more powerful inference rules may not be allowed for certain exercises To find out which rules are prohibited you should invoke the HELP command on the exercise If you cannot figure out what the next step in a proof should be you may get hints by using the ADVICE command but beware these hints are not always helpful and can be misleading A partially completed proof will be called a proof outline or simply an outline When you start proving a theorem with the EXERCISE or PROVE command ETPS will create an outline for you which contains a single line the theorem you would like to prove It is not yet justified since you are only planning to prove it In place of the justification there will be the word PLAN1 This last line of the outline is therefore called a planned line Lines ETPS User s Manual which are justified can be introduced by
28. x 56 59 49 59 S OA x A Hyp 89 49 59 D OA x A AND E OA x PLAN21 We don t need the universally quantified sponsoring lines any more in order to prove line 89 so let s use UNSPONSOR lt 6 gt unsponsor PLINE PLINE Planned line 89 gt LINELIST EXISTING LINELIST Sponsoring lines 59 58 56 57 55 gt 55 56 lt 7 gt rulep lt 8 gt pall 48 POWERSET D OA INTERSECT E OA S OA IMPLIES POWERSET D INTERSECT POWERSET E S PLANT 49 49 POWERSET D OA INTERSECT POWERSET E OA S OA Hyp Chapter 5 Type Theory in ETPS 50 49 POWERSET D OA S OA AND POWERSET E OA S Defn 49 51 49 POWERSET D OA S OA Conj 50 52 49 POWERSET E OA S OA Conj 50 53 49 S OA SUBSET D OA Defn 51 54 49 S OA SUBSET E OA Defn 52 55 49 FORALL x A S OA x IMPLIES D OA x Defn 53 56 49 FORALL x A S OA x IMPLIES E OA x Defn
29. x x 37 ETPS User s Manual IMPLIES FORALL z P a z AND P b z IMPLIES Q a a AND QO bb Deduct 13 lt 1l gt done You completed the proof Since this is not an assigned exercise the score file will not be updated The proof is complete Let s print it into a file so we can print it later lt 2 gt printproof FILENAME FILESPEC Filename example2 prt gt Written fil xample2 prt lt 3 gt exit 38 5 Type Theory in ETPS 5 1 Using ETPS for Type Theory ETPS can be used for higher order logic as well as for first order logic Wffs of type theory are written essentially as they are expressed in the logic book There are a few additional inference rules and the parsing and printing of wffs is slightly different while everything else described in the previous chapters is still valid 5 1 1 Types in Higher Order Logic There is a very direct translation from the way types are represented in the logic book and the way types are represented in ETPS Since Greek subscripts are not available on most terminals the Greek letters are transliterated to uppercase Roman letters The most commonly used types are I fort O for o S for A fora B for 8 C for y The same conventions for parentheses are used as in the logic book i e association to the left is assumed Note however that the outermost pair of parentheses must be preserved in order to distinguish types from identifiers Types are entered a
30. 2 Verifies that wff2 follows from wffl by Rule R possibly iterated using the equality term term2 II 3 Substitution S term var inwff Substitute a term for the free occurrences of variable in a gwff III 4 Basic Abbreviations CONTAINS DEFN wff Tests whether the argument contains a definition INST DEF inwff Instantiate the first abbreviation left to right 55 ETPS User s Manual III 5 Lambda Calculus LNO LNO LNO LCONTR reduct Lambda contract a top level reduct RM wff RM B Put a wff into lambda normal form equivalent to LNORM BI ETA wff Put a wff into beta normal form RM ETA wff Put a wff into eta normal form II 6 Negation movers PUSH NI EGATION gwff Pushes negation through the outermost operator or quantifier 56 ETA followed by LNORM ETA Appendix IV Appendix IV Theorems and Exercises IV 1 Book Theorems Substitution instances of the theorems below can be inserted into a proof by using the ASSERT command DESCR Axiom of description at all types t Yal Y EXT Axiom of extensionality at all types VX Eg X Jap X Df g REFL Reflexivity of Equality A A SYM Symmetry of Equality A B DB A T5302 Symmetry of Equality X Ve Y X T5310 Theorem about descriptions Ya B 2S pay T5310A Theorem about descriptions MZ P 2 E ZEN BA py ou IV 2
31. 98 L EXISTING LINELIST List of Lines 5 4 gt 5 lt 2 gt squeeze lt 3 gt cleanup No lines can be deleted CLEANUP will remove unnecessary lines and hypotheses from your finished proof lt 4 gt pall EL 1 FORALL x EXISTS y P x IMPLIES P y Assume negation 2 1 EXISTS x EXISTS y P x IMPLIES P y Neg 1 3 3 L EXISTS y P x IMPLIES P y Choose x 4 3 FORALL y P x IMPLIES P y Neg 3 5 3 P x IMPLIES P x UI x 4 6 3 FALSEHOOD RuleP 5 7 ik FALSEHOOD RuleC 2 6 8 FORALL x EXISTS y P x IMPLIES P y Indirect 7 Have we finished lt 5 gt done Score file updated Yes Let s make a nice copy of this proof Note that we have to specify a new file name to keep ETPS from overwriting the first file we made lt 6 gt texproof FILENAME FILESPEC Filename x2108 tex gt x2108b Written file x2108b tex If you have open proofwindows close them now with the command END PRFW lt 7 gt exit File x2108b work written 4 2 Example 2 gt etps etps for issar Version from Saturday September 23 1989 at 5 59 15 c Copyrighted 1988 by Carnegie Mellon University All rights reserved KKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK WARNING Be sure that you when you begin ETPS your current directory is one for which you have write access g your home directory KKEKKKKKKKKK
32. AVE to stop saving into the file When you subsequently use ETPS you can use EXECUTE FILE to automatically execute all the commands in the work file to set the flags and define the aliases 1 7 Bugs and Error Messages Typing or logical errors are usually noticed by ETPS which issues an appropriate diagnostic message and typically throws you back to top level Most bugs in ETPS itself will be caught by an error handler which appends an appropriate message to a file in the teacher s area This of course only applies to real bugs in the ETPS software or Common Lisp not typing errors which are caught by the command interpreter You may try again after you get a bug error message and often you will discover that you just made a mistake which was not caught by the usual error handling routines If you still get an error send mail to the teacher or send a message with the REMARK command If you think that you have discovered a bug in ETPS don t delete the WORK file for that session but rename that file say to Yexercise number work so that your work is not overwritten then allow read access for it and send mail to the teacher with a pointer to that file ETPS User s Manual 2 System Commands 2 1 Communication HELP subject Will list help available on the subject The help messages for inference rules can be very long you may wish to set the flag SHORT HELP to T to prevent this The default value of this flag is NIL
33. BED AL Editor command 52 MBED AR Editor command 52 MBED E Editor command 52 MBED E1 Editorcommand 52 MBED F Editor command 52 MBED IL Editor command 52 MBED IR Editor command 52 MBED L Editor command 52 MBED OL Editor command 52 MBED OR Editor command 52 MBED QL Editor command 52 MBED QR Editorcommand 52 MBED L Editor command 52 MBED R Editor command 52 MIN SCOPE Editor command 53 MODIFY GAPS System Command 13 37 MOVE System Command 13 MOVE System Command 13 MP Inference Rule 18 22 36 37 MRG Editor command 53 MRG Editor command 53 Mu 41 MU BIND 39 AME Editorcommand 51 AT 41 C 41 EG Editorcommand 16 EWS System Command 9 NF Editor command 16 NON ATOMIC 55 NOT 39 NOT FREE IN 55 NOT FREE IN HYPS 55 O Editor command 54 OCCLIST Argument Type 6 OK Editorcommand 15 ONE 41 OP Editor command 52 OR 40 Editorcommand 15 ALL System Command 10 12 30 32 34 37 L System Command 12 L System Command 12 LAN System Command 12 Planned 10 PLINE Argument Type 5 PLINE System Command 12 PMUT Editorcommand 53 PMUT Editor command 53 POP System Command 4 POSINTEGER Argument Type 5 POWERSET 40 PP Editorcommand 15 PLAN System Command 12 36 RACTICE Argument Type 6 RINTEDTFILE Flag 54 RINTEDTFLAG Flag 54 RINTLINEFLAG Flag 10 RINTPROOF System Command 12 38 RINTTYPES Flag 6 ROBLEMS System Command 1 5 6 9 ROOFLIST System Command 9 ROOFW ACTIVE
34. EQUALITY P R s t Transformation pp D2 ss gt PI ss pp D3 ss P1 D2 SYM Rule of Symmetry of Equality P1 H FA B P2 H B A Sym PI Transformation P2 ss gt P1 ss 3 10 Definition Rules EDEF Rule to eliminate first definition left to right D1 H t A D2 H t INST DEF A Defn DI Restrictions CONTAINS DEFN A Transformation pp D1 ss gt pp D2 ss EQUIV WFEFS Rule to assert equivalence of lines up to definition D1 H HP D2 H R EquivWffs DI Restrictions WFFEQ DEF P R Transformation pp D1 ss gt pp D2 ss IDEF Rule to introduce a definition P1 H INST DEF A P2 H t A Defn P1 Restrictions CONTAINS DEFN A Transformation P2 ss gt P1 ss 25 ETPS User s Manual 3 11 Lambda Conversion Rules LAMBDA BETA ETA LCONTR Rule to infer a line from one which is equal up to lambda conversion using both beta and eta rules and alphabetic change of bound variables DI H t A D2 H Be Lambda DI Restrictions WF FEQ AB LAMBDA A B Transformation pp Dl ss gt pp D2 ss Rule to infer a line from one which is equal up to lambda conversion using beta rule but NOT eta rule and alphabetic change of bound variables D1 H t A D2 H B Beta Rule DI Restrictions WEFEQ AB BETA A B Transformation pp D1 ss gt pp D2 ss
35. ETPS User s Manual 2010 February 12 Frank Pfenning Sunil Issar Dan Nesmith Peter B Andrews Hongwei Xi Matthew Bishop Chad E Brown Version for Basic Logic Mathematical Logic I and II Copyright 2010 Carnegie Mellon University All rights reserved This manual is based upon work supported by NSF grants MCS81 02870 DCR 8402532 CCR 8702699 CCR 9002546 CCR 9201893 CCR 9502878 CCR 9624683 CCR 9732312 CCR 0097179 and a grant from the Center for Design of Educational Computing Carnegie Mellon University Any opinions findings and conclusions or recommendations are those of the author s and do not necessarily reflect the views of the National Science Foundation 1 ETPS User Interface 1 1 Introduction You may find the Table of Contents at the end of this manual ETPS is a program which is designed to help you do your logic homework It was developed from TPS an ongoing research project in automated theorem proving It is written in Common Lisp To do your homework on the computer first enter ETPS It is highly recommended that you run ETPS in an X window on a Unix or Linux system or use the Java interface for ETPS if these facilities are available on your system so that formulas can be printed on the screen using special fonts which contain logical symbols and so that the proof you are developing can be printed and updated in special proofwindows as you work You can start the Java interface for ETPS using the JA
36. ETPS sends only a partial record of your session to a file on the teacher s area You must submit a printed copy of the finished proof as well To make this copy first print the proof into a file using the TEXPROOF command When you have exited from ETPS run this file through TEX Then print the press file generated by TEX and hand this output to your teacher A word of advice to the user ETPS is intended to aid you in learning logic but if you use it thoughtlessly you might be able to do exercises without learning much ETPS does not allow you to use the rules of logic in an incorrect manner but it s important that you learn for yourself how to apply the rules correctly By allowing only correct applications of the rules ETPS encourages the user to spend more time learning the techniques of proving theorems in logic It is strongly recommended that when ETPS does not allow you to do something you think about why what you tried was incorrect 1 2 Saving and Restoring Your Work ETPS saves your work automatically as you try to prove a theorem This facility is very similar to Emacs auto save feature ETPS commands SAVE WORK STOP SAVE RESUME WORK and RESUME SAVE allow you to explicitly use this feature ETPS also provides the commands SAVEPROOF and RESTOREPROOF for saving your proofs Unlike the automatic saving facility which saves everything typed by the user and later re execute
37. ETPS under Unix or Linux you may be able to use the following control characters in addition to those discussed in Section 1 4 CEri s Freeze output Ctril Q Proceed with output Ctrl Z Suspend the current program ETPS and return to the monitor Ctrl R Redisplay the current input line 1 2 Command Sequences You may enter a series of commands on the same command line by using the ampersand amp as a separator This is analogous to the C shell s use of the semicolon That is entering 0 command amp command amp amp command will cause ETPS to sequentially execute command through command as though you had typed them in one at a time For example after you have finished a proof you may want to enter the sequence lt 0 gt cleanup amp squeeze amp done amp texproof 1 3 History Substitutions It is often convenient to be able to refer to commands and arguments that you have already typed As in the C shell the exclamation point is used to indicate a history substitution with two exceptions An exclamation point that is followed by whitespace will not be interpreted as a history reference nor will an exclamation point that is immediately preceded by a a backslash Any input line that contains history substitutions will before execution be echoed on the screen as it would appear without the history references In ETPS each command line is given a unique number this number is par
38. FN is set to RULEP SIMPLE RULEP will merely ensure that the planned line follows by Rule P from the specified support lines When RULEP MAINFN is set to RULEP DELUXE which is the default RULEP will find a minimal subset of the support lines which suffices to prove the planned line by Rule P if any Note that RULEP DELUXE will be somewhat slower than RULEP SIMPLE In order to check the setting of RULEP MAINEN merely enter ETPS User s Manual RULEP MAINEN at the top level You will be prompted for a new value and the current value will be displayed Hit lt return gt to accept the current value or enter the new value ASSERT Assert a theorem known to ETPS Use a theorem known to ETPS see Appendix IV as a lemma in the current proof Such a theorem can only be used if allowed by the teacher for that exercise The first argument is the name of the theorem the second argument is the line number If the line already exists ETPS will check whether it is a legal instance of the theorem schema otherwise it will prompt for the metavariables in the theorem schema usually x or P Q ADD HYPS Weaken a line to include extra hypotheses Adding the hypotheses to the line may cause some lines to become planned lines If possible the user is given the option of adding hypotheses to lines after the given line so that no lines will become planned DELETE HYPS Delete some hypotheses
39. IMPLICS Rule to convert an equivalence into twin implications D1 H EP ER D2 H H P D R ARDP Transformation pp D1 ss gt pp D2 ss ICONJ Rule to introduce a conjunction by inferring it from two conjuncts P1 H FA P2 H B P3 H FA AB Transformation P3 ss gt P1 ss P2 ss IMP DISJ Rule to replace an implication by a disjunction D1 H EA DB D2 H bt Av B Transformation pp D1 ss gt pp D2 ss IMPLICS EQUIV Rule to convert twin implications into an equivalence P1 H iP Ps Ro AcR SP P2 H EPER Transformation P2 ss gt P1 ss INDIRECT Rule of Indirect Proof H1 H H t a P2 H H1 L P3 H t A Transformation P3 ss gt P2 H1 ss 21 Chapter 3 Inference Rules Hyp Deduct D2 Disj Imp DI Conj DI Conj DI EquivImp DI Conj Pl P2 Imp Disj DI ImpEquiv PI Assume negation Indirect P2 ETPS User s Manual INDIRECTI Rule of Indirect Proof using one contradictory line H1 4H H1 Teer Pe Assume negation P2 H Hl1 FB A B P3 H PA Indirect P2 Transformation P3 ss gt P2 HI ss INDIRECT2 Rule of Indirect Proof using two contradictory lines H1 4H H1 ENA Assume negation P2 H HI F B P3 H H1 t 8B P4 H PA Indirect P2 P3 Transformation P4 ss gt P2 HI ss P3 H1 ss MP Modus Ponens P1 H HA D2 H EA DB D3 H B MP P1 D2 Transformati
40. ION 40 HORT HELP Flag 9 HOWNOTYPES System Command 14 HOWTYPES System Command 14 IGMA1 41 ponsor 10 SPONSOR System Command 11 SQUEEZE System Command 13 30 32 37 Status 10 17 STOP SAVE System Command 2 3 7 11 13 31 STRING Argument Type 5 B Editor command 16 BEQ Editor command 53 BEQ Editor command 53 B B B a LA en IM Editor command 53 IM Editor command 53 JECTS System Command 14 BPROOF System Command 11 43 BSET 40 UBST Editor command 16 BST EQUIV Inference Rule 19 25 BST Inference Rule 19 24 BST L Inference Rule 19 25 BST R Inference Rule 19 25 BSTITUTE Inference Rule 19 24 BSTYP Editor command 16 cc 41 SUMMARY System Command 9 SYM Inference Rule 19 25 SYMBOL Argument Type 5 C Gq es Ert C ANNNNANNANNANNNHANN L em E a TEST PROBLEM Argument Type 6 TEXPROOF System Command 12 30 32 34 THAT 39 TP Editor command 54 TRUTH 6 40 See also T TYPESYM Argument Type 6 UGEN Inference Rule 19 23 29 36 37 42 44 UI Inference Rule 19 24 31 35 44 UNALIAS System Command 10 49 UNDO 13 UNDO Editor command 15 UNION 40 UNITSET 41 UNSCRIPT System Command 11 UNSPONSOR System Command 11 44 WFFEQ AB 55 WFFEQ AB BETA 55 WFFEQ AB ETA 55 WFFEQ AB LAMBDA 55 WFFEQ DEF 55 WFFP Editor command 54 XTR Editor command 15 YESNO Argument Type 5 ZERO 40 Editor command 15 P Sys
41. ISTS y P x IMPLIES P y Neg 1 We use the P command to show the lines which are now relevant lt 6 gt p 2 1 EXISTS x EXISTS y P x IMPLIES P y Neg 1 99 1 FALSEHOOD PLAN2 RULEC is often required when trying to prove a statement from an existentially quantified line It is probably the most complicated rule you will use so you might wish to study the description of RULEC in the previous chapter first as well the description in the textbook lt 7 gt rulec P4 LINE Conclusion without Additional Hypothesis 99 D1 LINE Existentially Quantified Line 2 gt D3 LINE Conclusion with Additional Hypothesis 98 H2 LINE Hypothesis with Chosen Variable 3 gt y GWFF Chosen Variable Name No Default gt x 3 1 3 EXISTS y P x IMPLIES P y Choose x 98 1 3 FALSEHOOD PLANS The last command created a negated statement so we can use PUSHNEG again lt 8 gt pushneg 3 4 4 3 1 FORALL y P x IMPLIES P y Neg 3 lt 9 gt ul D1 LINE Universally Quantified Line 4 gt D2 LINE Instantiated Line 5 gt t GWFF Substitution Term No Default gt x 5 1 3 P x IMPLIES P x UI x 4 31 ETPS User s Manual lt 10 gt p 4 3 1 FORALL y P x IMPLIES P y Neg 3 5 1 3 P x IMPLIES P x UI x 4 98 1 3 FALSEHOOD PLAN5 Note that line 5 is a contradiction so we can use it to justify line 98 by RULEP Line A isn t necessary for this step lt 1l gt rulep
42. KKKKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK 32 Chapter 4 Sample Proofs WARNING You cannot use the Unix convention in specifying file names Use the full pathname instead e g instead of entering foo work enter afs andrew usrill dn0z foo work KK KK KKK KKK KKK KK KKK KKK KKK KKK KKK KKK KKK KKK KK KKK KKK KKK KKK KKK KK KKK KKK KKK KK KKK KKKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKAKKKKKK ANNOUNCING ETPS can now be run on the sun3 35 workstation type as well as on the Microvax The more memory on the machine the faster ETPS will run To check the amount of memory available on a Sun 3 type etc dmesg grep avail in your typescript KKEKKKKKKKKKKKKKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK Loading changes done Loading afs andrew cmu edu math etps etps ini Finished loading afs andrew cmu edu math etps etps ini lt 1l gt prove WEF GWFFO Prove Wff No Default gt exists x forall y P x y implies forall y exists x P x y PREFIX SYMBOL Name of the Proof No Default gt examplel NUM LINE Line Number for Theorem 100 gt 100 EXISTS x FORALL y P x y IMPLIES FORALL y EXISTS x P x y PLAN1 If we were trying to prove one of the exercises in the text we would have used EXERCISE instead of prove
43. KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK WARNING You cannot use the Unix convention in specifyi Use the full pathname instead e g instead of hts reserved KKKKKKKKKKKKKKKKK nt directory is home directory KKEKKKKKKKKKKKKKKK KKKKKKKKKKKKKKKKK ng file names entering foo work enter afs andrew usril adn0z foo work KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKAKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK ANNOUNCING ET E PS can now be run on the sun3_35 workstation type as well as on the Microvax The more memory on the machine the faster ETPS will run To check the amount of memory available on a Sun 3 type iye etc dmesg grep avail in your typescript 34 Chapter 4 Sample Proofs kkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkxkkxkxkxkxkxkxkxkxkkxkxkxkkkkkkxkx k Loading changes done Loading afs andrew cmu edu math etps etps ini Finished loading afs andrew cmu edu math etps etps ini lt 1l gt prove WEF GWFFO Prove Wff No Default gt forall x forall y P x y implies Q x x implies forall z P a z and P b z implies Q aa and Q b b PREFIX SYMBOL Name of the Proof No Default gt example2 NUM LINE Line Number for Theorem 100 gt
44. ONJ 18 21 36 IDEF 19 25 43 44 IMP DISJ 18 21 IMPLICS EQUIV 18 21 42 INDIRECT1 18 21 INDIRECT2 18 22 INDIRECT 18 21 31 INEG 19 22 LAMBDA 19 26 LCONTR BETA 26 LCONTR ETA 26 LCONTR 19 26 62 LEMMA 18 20 LET 19 24 LEXPD BETA 26 LEXPD ETA 27 LEXPD 19 26 MP 18 22 36 37 PULLNEG 19 22 PUSHNEG 19 22 31 RULEC 19 23 31 RULEP 18 19 30 32 44 SAME 18 20 SUBST EQUIV 19 25 SUBST 19 24 SUBST L 19 24 SUBST R 19 25 SUBSTITUTE 19 24 SYM 19 25 UGEN 19 23 29 36 37 42 44 UI 19 23 31 35 44 INST Editor command 51 INST DEF 55 INST1 Editorcommand 51 INSTALL Editor command 51 INTEGER Argument Type 5 INTERSECT 40 INTRODUCE GAP System Command 13 IS VARIABLE 55 JAVAWIN System Command 1 10 L Editorcommand 15 LAMBDA 39 LAMBDA Inference Rule 19 26 LCONTR 56 LCONTR Inference Rule 19 26 LCONTR BETA Inference Rule 26 LCONTR ETA Inference Rule 26 LEAVE System Command 14 LEMMA Inference Rule 18 20 LET Inference Rule 19 24 LEXP Editorcommand 51 LEXPD Inference Rule 19 26 LEXPD BETA Inference Rule 27 LEXPD ETA Inference Rule 27 LINE Argument Type 5 LINE RANGE Argument Type 5 LINE RANGE LIST Argument Type 6 LINELIST Argument Type 6 LIST System Command 14 LIST RULES System Command 9 LNORM 56 LNORM Editorcommand 51 LNORM BETA 56 LNORM BETA Editor command 51 LNORM ETA 56 LNORM ETA Editor command 51 52 M
45. P1 H tP R P2 H FP R Ext P1 Transformation P2 ss gt P1 ss LET Rule to produce a new variable which will represent an entire formula during part of a proof D1 H FA A Refl D2 H Ax x A EGen x D1 H3 H H3 Piti A Choose x P4 H H3 P5 H FC RuleC D2 P4 Restrictions NOT FREE IN HYPS x NOT FREE IN x C Transformation P5 ss gt P4 ss D1 D2 H3 SUBST Substitution of Equality Performs whichever of the SUBST L and SUBST R rules is appropriate P1 H EP D2 H bs ty D3 H t R Sub P1 D2 Restrictions SAME MODULO EQUALITY P R s t Transformation pp D2 ss gt PI ss pp D3 ss Pl D2 24 Chapter 3 Inference Rules SUBST L Substitution of Equality Replaces some occurrences of the left hand side by the right hand side P1 H E P D2 H E sa t D3 H ta Subst P1 D2 Restrictions R PRIME RESTR s P t R Transformation pp D2 ss gt PI ss pp D3 ss P1 D2 SUBST R Substitution of Equality Replaces some occurrences of the right hand side by the left hand side P1 H EP D2 H Fon s D3 H t R Subst P1 D2 Restrictions R PRIME RESTR s P t R Transformation pp D2 ss gt PI ss pp D3 ss Pl D2 SUBST EQUIV Substitution of Equivalence Useable when R and P are the same modulo the equivalence s EQUIV t P1 H EP D2 H Fa Sst D3 H R Sub equiv P1 D2 Restrictions SAME MODULO
46. STING LINE Argument Type 5 EXISTING LINELIST Argument Type 7 EXISTS 39 EXISTS1 39 EXISTSN 39 EXIT System Command 3 9 10 32 34 38 EXPAND Editorcommand 51 EXT Inference Rule 19 24 42 EXT 0 Inference Rule 19 24 42 FARR AMORA FALSEHOOD See also L FB Editorcommand 15 6 40 FI Editor command 15 FILESPEC Argument Type 5 FINITE 41 Flag 7 Flags 14 FORALL 39 FORALLN 39 FREE FOR 55 Gaps 13 GVAR Argument Type 6 GVAR LIST Argument Type 7 GWFF Argument Type 5 6 GWFFO Argument Type 6 GWFFLIST Argument Type 7 HEAD Editor command 53 Help See also HELP System Command 1 9 36 HISTORY System Command 9 48 HISTORY SIZE Flag 9 47 HVARS Editor command 53 HYP Inference Rule 18 20 Editor command 15 ONJ Inference Rule 18 21 36 EF Inference Rule 19 25 43 44 L Editorcommand 54 P DISJ Inference Rule 18 21 PLICS EQUIV Inference Rule 18 21 42 PLIES 40 DIRECT Inference Rule 18 21 31 D D Baw con RECT1 Inference Rule 18 22 RECT2 Inference Rule 18 22 EG Inference Rule 19 22 Inference Rules AB 19 23 ABE 19 23 ABSURD 18 22 ABU 19 23 ADD HYPS 18 20 ASSERT 18 20 BETA 26 CASES 18 20 DEDUCT 18 20 33 35 43 44 DELETE HYPS 18 20 DISJ IMP 18 21 ECONJ 18 21 36 43 EDEF 19 25 43 EGEN 19 23 29 34 ENEG 18 22 EQUIV IMPLICS 18 21 EQUIV WFFS 19 25 ETA 26 EXT 0 19 24 42 EXT 19 24 42 HYP 18 20 IC
47. T PROBLEM A potential test problem Several argument types are lists or pairs of other types They are specified in parentheses for example 1 2 99 The empty list is specified by Pairs are entered as two element lists where the two elements are separated by a period For example you might enter the pair x y Do not put commas into your input We list the most common of the composite argument types below OCCLIST A list of occurrences counted left to right of a subwff in a wff This list may be entered as a list of positive numbers or the symbol ALL ALL refers to all occurrences of the subwff LINELIST A list ofnumbers of lines LINE RANGE LIST A list of line ranges Chapter 1 ETPS User Interface EXISTING LINELIST A list of numbers of lines in the current outline GWFFLIST A list of GWFFs GVAR LIST A list of GVARs 1 6 Flags and Amenities Many aspects of ETPS are controlled by flags See section 2 11 for some information about flags ETPS incorporates several features of the Unix C shell csh top level These features include various control characters command sequences a history mechanism and aliases See Appendix I for details You may wish to set certain flags and define certain aliases each time you run ETPS A good way to do this without having to repeat the commands is to start a work file using SAVE WORK then set the flags and define your aliases then use STOP S
48. TPS The extension of filename defaults to WORK STOP SAVE Stops saving into the current save work file All commands that have been given but not yet saved will be written out to the file RESTORE WORK filename show lines exec print outfile Executes commands from filename and continues to save in that file When the end of the file is reached you will be back at ETPS command level show lines controls whether proof lines will be shown when restoring the proof This is very time consuming therefore the default is NO exec print controls whether printing commands will be executed when restoring the proof These are commands like PLINE PRINTPROOF HELP or PROBLEMS The default is NO outfile is the name of a file where the commands and the output is echoed to while they are re executed The default is TTY the terminal so you can see how far ETPS has progressed To speed up the process you may select NUL RESTORE WORK will not re execute any of the following EXIT RESUME SAVE RESTORE WORK EXECUTE FILE SAVE WORK STOP SAVE They usually don t make sense when reading commands from a save work file If you aborted a command with a Ctrl C the Ctrl C will be in the file and will abort the execution of the commands RESUME SAVE Use this command to resume saving commands into the most recent save work file Unlike RESTORE WORK this command doesn t execute commands from t
49. VAWIN command see Section 2 3 If you are running ETPS in an X window equipped with the special fonts used to print logical symbols you need to tell ETPS that you want to use the special fonts for output At the ETPS prompt issue the command setflag style then at the subsequent prompt xterm This will cause the special symbols to appear when any wffs are printed by ETPS If for some reason the special symbols won t print properly just change the style back from xterm to generic If you are running ETPS in an X window or using the Java interface you will probably also wish to use the BEGIN PRFW command to start up windows containing the current subproof and the complete proof see Section 2 4 You may need to iconify a window or move it up on your screen by the usual methods for manipulating windows so that you will have room to issue ETPS commands You can eventually close the proofwindows with the END PRFW comand See Section 2 5 for commands which control what is regarded as the current subproof To help you learn how to use ETPS transcripts of sample sessions are provided in Chapter 4 Just follow these examples exactly on your own computer and you will soon have a general idea of what to do You can also do some practice unassigned exercises which you can find with the aid of the PROBLEMS command and make frequent use of the ADVICE command which will offer suggestions about what to do next You should note that the
50. WERSET D OA INTERSECT E OA S OA PLAN8 Now we eliminate the POWERSET S is in the powerset of DOE iffSisasubsetof D A E lt 9 gt idef 93 49 S OA SUBSET D OA INTERSECT E OA PLAN9 Now we eliminate the INTERSECT from the justified line 49 We therefore have to use the command symmetric to IDEF which is EDEF lt 10 gt edef 50 49 POWERSET D OA S OA AND POWERSET E OA S Defn 49 1 5P 50 49 POWERSET D OA S OA AND POWERSET E OA S Defn 49 93 49 S OA SUBSET D OA INTERSECT E OA PLAN9 lt 2 gt econj 51 49 POWERSET D OA S OA Conj 50 52 49 POWERSET E OA S OA Conj 50 From here on we go through a sequence of routine elimination of definitions lt 3 gt edef 53 49 S OA SUBSET D OA Defn 51 lt 4 gt edef D1 LINE Line with Definition 53 gt 52 D2 LINE Line with Instantiated Definition 54 gt 54 49 S OA SUBSET E OA Defn 52 lt 5 gt P 53 49 S OA SUBSET D OA Defn 51 54 49 S OA SUBSET E OA Defn 52 93 49 S OA SUBSET D OA INTERSECT E OA PLAN9 We are on the right track From S DandS T Ewe should be able to infer thatS C DOE lt 6 gt edef 53 D2 LINE Line with Instantiated Definition 55 gt 3 5 49 FORALL x A S OA x IMPLIES D OA x Defn 53 lt 7 gt edef 54 D2 LINE Line with Instantiated Definition 56 gt 43 ETPS User s Manual
51. addition the bracketing conventions used in the logic textbook are used in ETPS and the symbol can be used as an abbreviation for NOT thus forall x P x y implies Q x or Q y represents the same gwff as FORALL x P x y IMPLIES NOT Q x OR Q y In general you may type wffs just as they appear in the logic text See Chapter 4 for some examples of typed wffs and variables and Chapter 5 especially Section 5 1 3 for examples of wffs of higher order logic type theory For more examples execute the command PROBLEMS in ETPS with style GENERIC and answer yes when you are asked if you wish to see ETPS User s Manual definitions Superscripts can be used but unlike the textbook they are not used to indicate the arity of functions Instead they are used to distinguish variables Superscripts are indicated by using a Valid superscripts must follow these rules e Only strings of the form 0 9 can be superscripts e The user will explicitly indicate a superscript by the use of the E g x40 foo 1234567 A which is not followed by a legal superscript is treated as any non logical constant character would be Thus x is legal input as is or NAA or xy e A superscript can only be used at the end of a variable not in the middle Hence xAly will be parsed as x41 ID y D x 1 applied to y not as x 1y I a single variable e Generic style will show the superscripts with the i e if
52. and suggests their deletion These lines are deduced lines which have not been used to justify another line and are no longer supports for any planned line In addition CHECK STRUCTURE looks for extraneous hypotheses in each of the lines of the proof 2 10 Higher Order Logic PWTYPES gwff Print wff with type symbols 13 ETPS User s Manual SHOWTYPES From now on show the types of all wffs SHOWNOTYPES From now on suppress types of all wffs 2 11 Flags and Review Many aspects of ETPS are controlled by flags Most of the time you can ignore these but if you wish to change some aspect of ETPS such as the widths of the lines in a proof you may be able to do so by changing the value of a flag such as RIGHTMARGIN HELP flag will provide information about a particular flag Use the REVIEW top level to find what flags are available Enter for a list of all the commands in this top level the following is just a selection of those available REVIEW Enter the review top level SETFLAG Change the value of a flag SUBJECTS Each flag is associated with one or more subjects this command lists all the known subjects Some of these subjects may be irrelevant to ETPS but used in a larger system of which ETPS is a component you can ignore them LIST subjects List all the flags associated with these subjects LEAVE Return to the main top level 2 12 ETPS Editor The ETPS editor can be us
53. antified so we use the appropriate rule lt 3 gt egen P2 LINE Existentially Quantified Line 99 gt 29 ETPS User s Manual P1 LINE Line to be Existentially Generalized 98 gt t GWFF Term to be Generalized Upon No Default gt ED 99 Let s use the editor to pick out the term we want from line 99 lt Ed1 gt p EXISTS y P x IMPLIES P y Here s the current formula lt Ed2 gt d P x IMPLIES P y We move inside the quantifier lt Ed3 gt 1 d We use two commands to get to x x lt Ed4 gt o0k Return x as the GWFF we were asked for 98 P x IMPLIES P x PLAN3 All that remains is an easy application of RULEP lt 4 gt rulep P1 PLINE Plan Line 98 gt L EXISTING LINELIST List of Lines gt lt 5 gt squeeze SQUEEZE removes any unnecessary gaps Now we take a look at the completed proof lt 6 gt pall 1 P x IMPLIES P x RuleP 2 EXISTS y P x IMPLIES P y EGen x l 3 FORALL x EXISTS y P x IMPLIES P y UGen x 2 lt 7 gt done Score file updated The DONE command is crucial Not only does it verify that the proof is complete it also ensures that you get credit for doing it Now let s make a nice copy of the proof lt 8 gt texproof FILENAME FILESPEC Filename x2108 tex gt Written file x2108 tex ISAZ Let s interrupt ETPS and print the current proof gt tex x2108 This is TeX Version 3 14159 C ve
54. ce commands apply inference rules and they may be used in various ways to complete the proof They may generate either new planned or sponsoring lines or close up a proof by justifying planned lines with sponsoring lines However there is usually a most natural way to use a rule This is indicated in the statement of the rule by labelling those lines which are usually sponsors before or after the rule is applied with a D for deduced followed by a number Similarly those lines the rule expects to be planned lines are labelled with a P followed by a number The transformation statement in an inference rule description indicates the change in the proof status effected by the most natural use of the rule The lists before the arrow gt are matched against the initial status those after the arrow describe what the new status should be The first element of a list is always a planned line and the remaining elements are its sponsors Each element of a list is either a label for a line in the rule pp or ss The symbol pp refers to all matched planned lines and the symbol ss to all other sponsoring lines for each of the matched planned lines Certain lines in a rule description are expected to exist in the proof before the rule is applied these are indicated by an asterisk If a line does not already exist when you apply an inference command and its corresponding line in the rule asserts a wff which cannot be formed from the wffs in rule lines corres
55. d by the SAME rule This command is applicable only if the proof is complete CLEANUP asks for confirmation before actually deleting lines DONE Signals that you think that you have completed the current proof ETPS will not believe you if you are not really done The DONE command appends a message to the recordfile in the teacher s directory If you fail to use it you may not get credit for your work SUMMARY Tells the user what exercises have been completed EXIT Leave ETPS See Section 1 3 for some information on reentering ETPS This command will automatically close open work files HISTORY n reverse Show history list Shows the N most recent events N defaults to the value of HISTORY SIZE showing entire history list REVERSE defaults to NO if YES most recent commands will be shown first ALIAS name def Define an alias DEF for the symbol NAME Works just like the alias command in the Unix csh If the value of NAME is ALL all aliases will be printed if the value of DEF is the empty string then the current alias definition of NAME will be printed See UNALIAS ETPS User s Manual UNALIAS name Remove an alias for the symbol NAME Like the Unix csh unalias except that NAME must exactly match the existing alias no filename completion is done See Section I 4 for more discussion of aliases 2 3 Starting the Java Interface There is a Java interface for ETPS running under Allegro Lisp version 5 0 or great
56. ding to their binding priority and abbreviations marked with abb Improper symbols A LAMBDA The A binder v FORALL 3 EXISTS 3 EXISTS1 sent AXa Bo EXISTSN Jz NAT z A A FORALLN Yz NAT z gt A u U BIND MA po AZo Ay THAT L AZ A Unary operators with equal binding priority except NOT which has the least binding priority A NOT 39 ETPS User s Manual abb NE ae AX rz dt x t Avg SENSE P owa abb POWERSET ABA e E P M abb SETINTERSECT AS sxoay Zo Y Bay po pe Intersection of a collection of sets U abb SETUNION AS oA Pou S PAP x Union of a collection of sets L FALSEHOOD T TRUTH Binary operators strongest binding first M abb INTERSECT AP AAA P X A GX Intersection of two sets U abb UNION APAIA P XV GX Union of two sets c abb SUBSET AP ANN XP XD qx Equality at type a oua S abb SETEQUIV AB AG P Eaa ASP Equality between sets S abb EQUIVS AP a ARa YZP XERE Elementwise equality between sets This is equivalent to equality between sets if one assumes extensionality lt abb Ax Ay DYE oo X Yz Pp Z D p SUCCe Zl DP Y Less than or equal to for natural numbers A AND v OR IMPLIES abb EQUIV Equality at type o Other abbreviations Conditional COND Ax Ay Ap THAT q p A x qv pAy a Equipollence EQP AP SAIS VA P xX D q s x JA Vy qd Y DAx p x Ay s x Zero ZERO
57. done amp pall amp texproof T lt 156 gt finish myproof mss 50 x Appendix II A pendix II More Editor Commands The most commonly used editor commands were listed in Section 2 12 Here we list the rest of the commands available in the editor Note that some of the commands available within the editor are needed for type theory and may be ignored by the user who is interested only in first order logic IL1 Labels lt Edn gt DELWEAK label Replace all occurrences of the label in the current edwff by the wff it represents Edn DW Replace a top level occurrence of label by the wff it represents lt Edn gt DW Replace all labels in a wff by the wffs represented by them lt Edn gt NAME label Assign a label to the edwff and replace the edwff with this label lt Edn gt RW label Makes current edwff the new value of label which must already exist II 2 Basic Abbreviations lt Edn gt EXPAND Instantiates all equalities A Edn gt INST gabbr Instantiate all occurrences of an abbreviation The occurrences will be lambda contracted but not lambda normalized A Edn INSTI Instantiate the first abbreviation left to right A Edn gt INSTALL exceptions Instantiate all definitions except the ones specified in the second argument II 3 Lambda Calculus lt Edn gt ABNORM Convert the gwff to alphabetic normal form lt Edn gt ETAB gwff Eta expands until or
58. ed to construct new formulas and extract subformulas from formulas already known to ETPS You can enter the editor with the top level command ED Use ed gwff when asked for a GWFF This will prompt you with lt Edn gt The wff you are editing will be referred to as EDWFF Using the editor commands move to a subformula and or modify the EDWFF until you have the GWFF you desire Then exit the editor by using the command OK the current value of EDWFF will be returned For example suppose that ETPS has asked you for a GWF F and the GWFF you would like to supply is B a subwff of the assertion in line 1 whichis A AND B IMPLIES C Enter ed 1 to enter the editor with that formula Then use the following sequence of commands lt Ed1 gt L This moves to the left of the implication sign A AND B lt Ed2 gt R This moves to the right of the conjunction B lt Ed3 gt 0OK Since we have what we want we exit the editor This is of course a trivial example but if B had been a very complicated formula using the editor would have been both faster and less susceptible to error than typing it in would have been You can also use multiple commands on a single editor input line which will save more time We could have done the above example as follows lt Ed1l gt L R OK When ETPS is running under X windows or through the Java interface see Section 2 3 the command ED will also start up two windows which display the top f
59. er Special symbol fonts proofwindows see Section 2 4 and editor windows see Section 2 12 are available when using the Java interface JAVAWIN Start the Java interface This should open a Java window with menus a display area for ETPS output and possibly a prompt at the bottom of the window All ETPS output after the Java window opens will be printed into the Java window Also all user input must be entered via the Java window either using the menus or using the prompt at the bottom of the window To enter input into the prompt the user may need to click on the prompt area to bring it into focus 2 4 Proofwindows When ETPS is running under X windows or through the Java interface see section 2 3 it is possible to start up separate windows displaying the current subproof which is described in Section 2 5 and can be printed on the screen with the P command the current subproof plus line numbers which can be printed with the PN command and the complete proof which can be printed with the PALL command These windows will be automatically updated as commands are issued to modify the proof interactively By scrolling up in these windows you can see the previous displays The windows may be moved around and resized by the usual methods for manipulating windows PSTATUS will update the proofwindows Printing in the proofwindows can be modified by changing the flags PROOFW ACTIVE PROOFW ALL PROOFW ACTIVE NOS and PRINTLINEFLAG For more
60. fs of sample theorems obtained by using script before starting ETPS Remarks are added in italics It may be a good idea to look ahead a little bit i e look at the final proof first to see what we are trying to obtain You can execute these proof steps on your own computer and use the PALL command frequently to get a good picture of how the proof grows or if you are running ETPS under X windows or using the Java interface use the BEGIN PRFW command to open proofwindows and watch the proof grow in them As mentioned in Section 1 1 you will probably find it best to set the style flag to xterm and have logical formulas displayed with logical symbols if you can However in this chapter we display formulas in generic style 4 1 Example 1 gt etps etps for issar Version from Saturday September 23 1989 at 5 59 15 c Copyrighted 1988 by Carnegie Mellon University All rights reserved KKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK WARNING Be sure that you when you begin ETPS your curre one for which you have write access Gar your KEKE KKK KKK KKK KK KKK KKK KKK KKK KKK KKK KEK KKK KKK KKK KKK KKK KKK KKKKEKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK WARNING You cannot use the Unix convention in specifyi nt directory is home directory KKEKKKKKKKKKKKKKKK KKKKKKKKKKKKKKKKK ng file names Use the full pathname instead e g instead of entering
61. gt D For an expression like P x y move to the rightmost element in this example y For a quantified expression move to the scope of the quantifier lt Edn gt FB _ Find the first binder left to right Edn FI Find an infix operator lt Edn gt L For an infix operator move to the left argument lt Edn gt R For an infix operator move to the right argument lt Edn gt UNDO Moves up like 0 but throws away any editing since your last downward moving command typically A D L or R lt Edn gt XTR Makes the current edwff the top wff lt Edn gt Move upwards through enclosing wffs all the way to the top 2 12 5 Substitution lt Edn gt AB newvar Alphabetic change of variable at top level A Edn gt IB term Instantiate a top level universal or existential binder with a term 15 ETPS User s Manual lt Edn gt REW EQUIV gwff Replaces each equivalence in the gwff with a conjunction of implications lt Edn gt RP rep sym rep by Replace one occurrence of a symbol rep sym such as AND by a predefined equivalent wff involving the symbol rep by such as A p A q p 2 q In this example rep sym is AND and rep by is IMPLIES To see if a symbol can be replaced using this command enter HELP symbol any such replacements will be listed under the heading Replaceable Symbols lt Edn gt RPALL rep sym rep by Replace all occurrences of a symbol by a predefined equivalent wff lt Edn gt SUB gwff
62. he file but simply appends subsequent commands to the file You may not use this command if you are already saving work Also you may run into trouble if you forgot to save some commands EXECUTE FILE filename show lines exec print outfile Works like RESTORE WORK but does not continue saving into a file after executing the commands in the file SCR H PT scriptfile if exists append Saves a transcript of session to a file UNSCRIPT Closes the most recent file opened with the SCRIPT command 11 ETPS User s Manual 2 7 Printing DEPTHn nis a number This command causes all subformulas at depth greater than n to be printed as amp For example the wff FORALL x FORALL y FORALL z P x y z will be printed as below after the command DEPTH 4 FORALL x FORALL y FORALL z amp This command may save time in printing huge formulas particularly in higher order logic PW gwff Print gwff PWSCOPE gwff Print gwff with all brackets restored This is sometimes useful if you are not sure which connective has precedence over another PLINE line Print a specified line PL lower upper Print all lines in the range from lower to upper U L print ranges Print all proof lines in given ranges U PLAN pline Prints the planned line pline and all of its sponsors A similar effect can be achieved with the P provided pline is the current planned line SUBPROOF will cha
63. his command also has a recursive form ASRB lt Edn gt ASSL Applies the left associative law changing A B C to A B C This command also has a recursive form ASSL lt Edn gt ASSR Applies the right associative law changing A B C to A B C This command also has a recursive form ASSR lt Edn gt CMRG Deletes the constants TRUTH and FALSEHOOD from a wff see the help message for examples This command also has a recursive form CMRG lt Edn gt CMUT Applies the commutative laws to a formula see the help message for examples This command also has a recursive form CMUT lt Edn gt CNTOP connective or quantifier Changes the outermost connective or quantifier to that specified lt Edn gt DIST CTR Applies the laws of distributivity to a wff in the contracting direction see the help message for examples This command also has a recursive form DIST CTR lt Edn gt DIST EXP Applies the laws of distributivity to a wff in the expanding direction see the help message for examples This command also has a recursive form DIST EXPX lt Edn gt DNEG Removes a double negation from a wff This command also has a recursive form DNEG lt Edn gt MRG Merges redundant connectives in a wff see help message for examples This command also has a recursive form MRG A ti Q n gt PMUT Permutes the two components of an infix operator This command also has a recurs
64. iginal wff is part of a wff of base type lt Edn gt ETAC Reduces lambda x fx to f at the top lt Edn gt ETAN Reduces lambda x fx to f from inside out lt Edn gt ETAX Performs one step of eta expansion of the gwff lt Edn gt LEXP var term occurs Converts the wff into the application of a function to the term The function is formed by replacing given valid occurrences of a term with the variable and binding the result lt Edn gt LNORM Put a wff into lambda normal form equivalent to LNORM BETA followed by LNORM ETA lt Edn gt LNORM BETA 51 ETPS User s Manual Put a wff into beta normal form lt Edn gt LNORM ETA lt Edn gt R ED Put a wff into eta normal form exactly equivalent to ETAN Lambda contract a top level reduct Bound variables may be renamed II 4 Quantifier Commands lt Edn gt DB Delete the leftmost binder in a wff lt Edn gt EP Delete all essentially existential quantifiers in a wff lt Edn gt OP Delete the leftmost binder in a wff Delete all essentially existential quantifiers in a wff II 5 Embedding Commands There are a range of embedding commands which take the current edwff and embed it below a quantifier or connective These commands all begin MBED and then have a suffix denoting the quantifier or connective and a further suffix if appropriate denoting whether the current wff is to beco
65. is the way they are invoked Simply type the name of the command you may use lt Esc gt to complete its name and then type lt Return gt The command may be printed in either upper or lower case If the command takes arguments ETPS will prompt you in succession for each argument The prompt takes the general form argument name argument type help default gt For example lt 1 gt PROVE WFF GWFFO Prove wff No Default gt PREFIX SYMBOL Name of the proof No Default gt NUM LINE Line number for theorem 100 gt You may also specify command arguments on the command line itself ETPS will then prompt you only for the arguments you haven t specified This is a useful option for commands like PL 2 50 which directly prints every line in the range from 2 to 50 After ETPS issues a prompt you have the following options for your reply besides typing in the argument lt Return gt This selects the default if there is one This selects the default not only for this argument but all remaining arguments This can also be used on the command line itself This gives help about the type of the argument ETPS is waiting for This gives help about the command for which you are supplying arguments In particular when applying an inference rule this will give you the statement of the rule ABORT Aborts current command PUSH Temporarily suspend whatever you re doing and start a new top level The command POP
66. ive form PMUT lt Edn gt SUBEQ Reduces an equivalence to a conjunction of implications This command also has a recursive form SUBEQ lt Edn gt SUBIM Reduces an implication to a disjunction This command also has a recursive form SUBIM II 7 Miscellaneous A ti Q n gt CNF Find the conjunctive normal form of a wff A kri Q n gt HEAD Finds the head of a gwff n gt HVARS Returns all the head variables of a gwff A ti Q lt Edn gt MIN SCOPE Minimises the scope of quantifiers in a gwff 53 ETPS User s Manual II 8 Wellformedness lt Edn gt DUPW connective Duplicates a wff across a connective lt Edn gt EDILL Finds a minimal ill formed subformula lt Edn gt ILL Returns a list of messages each describing the error in a minimal ill formed subformula Edn TP Returns the type of a gwff lt Edn gt WFEP Tests for a gwff general well formed formula II 9 Saving and Recording Wffs Saving wffs into a file is governed by the two flags PRINTEDTFILE and PRINTEDTFLAG which determine the name of the file being written and whether or not wffs are currently being written to it respectively lt Edn gt O Toggles recording on and off i e inverts the current value of PRINTEDTFLAG lt Edn gt REM string Writes a comment into the current output file lt Edn gt SAVE label Saves a gwff by appending it to the file savedwffs
67. justifying a planned line introducing a hypothesis or deriving consequences of already justified lines Proofs may be built down from the top adding consequences of established lines or up from the bottom justifying planned lines by asserting new planned lines It is a good idea to work up from the bottom as much as possible so that ETPS will already know about most of the wffs you need and you will not have to type them in ETPS was originally developed for use with the textbook An Introduction to Mathematical Logic and Type Theory To Truth Through Proof by Peter B Andrews A second edition was published by Kluwer Academic Publishers in 2002 and is now available from Springer which which has taken over Kluwer Exercises from this textbook are available in ETPS However the inference commands available in your version of ETPS may depend on the particular logical system chosen by your teacher Inference commands are specified as inference rules and are listed in Chapter 3 Ideally after repeatedly applying rules to planned and deduced lines they will meet and every planned line will be justified The examples in Chapter 4 should make all this clearer When you have finished the proof issue the DONE command This will record the completion of the exercise if you used the EXERCISE command The PROVE command lets you prove arbitrary wffs but it will not give you credit for any exercises to which these wffs correspond
68. me the left or right side of the new formula They are lt Edn gt MBED AL Embed the current wff below AND on the left side lt Edn gt MBED AR Embed the current wff below AND on the right side lt Edn gt MBED E Embed the current wff below an EXISTS quantifier lt Edn gt MBED E1 Embed the current wff below an EXISTS1 quantifier lt Edn gt MBED F Embed the current wff below a FORALL quantifier lt Edn gt MBED IL Embed the current wff below IMPLIES on the left side lt Edn gt MBED IR Embed the current wff below IMPLIES on the right side lt Edn gt MBED L Embed the current wff below a LAMBDA binder lt Edn gt MBED OL Embed the current wff below OR on the left side lt Edn gt MBED OR Embed the current wff below OR on the right side lt Edn gt MBED QL Embed the current wff below EQUIV on the left side lt Edn gt MBED QR Embed the current wff below EQUIV on the right side lt Edn gt MBED L Embed the current wff below on the left side lt Edn gt MBED R Embed the current wff below on the right side 52 Appendix II II 6 Changing and Recursive Changing Commands Many of these commands operate only on the current wff but have a recursive form that will perform the same operation on the current wff and all of its subwffs lt Edn gt ASRB Absorbs unnecessary AND and OR connectives see the help message for examples T
69. nge the current planned line See Section 2 5 for more information on SUBPROOF AP Same as PPLAN for the current planned line Note that P is not a control character but two characters P followed by a lt Return gt PN As for P but also prints the line numbers only of all the other lines of the proof PN is not a control character but three characters P and N PALL Print all the lines in the current outline PRINTPROOF filespec This will print the current proof into a file SCRIBEPROOF filespec This will also print the current proof into a file but uses special symbols In order to print this file you must first run it through SCRIBE filespec has the same format as in PRINTPROOF The extension defaults to MSS TEXPROOF filespec Print the current proof into a tex file After leaving tps run this tex file through TeX and print the resulting file 2 8 Rearranging the Proof This section describes commands which rearrange the proof outline which is described in Section 3 1 The first two commands are frequently useful for starting over a part of the proof after you realize you have tried a wrong approach DELETE existing linelist Delete the lines in existing linelist from the proof If you delete a hypothesis line all lines which use this hypothesis will also be deleted If a line justifying another line is deleted the justification of that line is changed to PLANn Lines are shown as they a
70. on pp D2 ss gt PI ss pp D3 ss P1 3 6 Negation Rules ABSURD From falsehood deduce anything P1 H t L P2 H t A Absurd P1 Transformation P2 ss gt P1 ss ENEG Eliminate a negation D1 H t A P2 H FA P3 H H L NegElim D1 P2 Transformation P3 D1 ss gt P2 ss INEG Introduce a negation H1 HHI A Hyp P2 H HI HL P3 H SA NegIntro P2 Transformation P3 ss gt P2 HI ss PULLNEG Paull out negation P1 H PUSH NEGATION A P2 H H A Neg PI Restrictions NON ATOMIC A Transformation P2 ss gt P1 ss 22 PUSHNI EG Push in negation D1 H E A D2 H PUSH NEGATION Restrictions NON ATOMIC A Transformation pp D1 ss gt 3 7 Quantifier Rules AB ABE ABU EGEN RULEC UGEN Chapter 3 Inference Rules EAT o pp D2 ss Rule to alphabetically change embedded bound variables D1 H t A D2 H t B Restrictions WFFEQ AB A Transformation pp D1 ss B gt pp D2 ss Rule to change a top level occurrence of an existentially quantified variable D1 H dx A D2 H Fay S Y X A Restrictions FREE FOR y X A NOT FREE IN y A Transformation pp D1 ss gt pp D2 ss Rule to change a top level occurrence of a universally quantified variable P1 H H Vy O S
71. ormula and the current formula in the editor These windows are automatically updated as commands are issued to modify the formula and they will disappear when you use OK to leave the editor By scrolling up in these windows you can see the previous displays The windows may be 14 Chapter 2 System Commands moved around and resized by the usual methods for manipulating windows To prevent the windows from appearing modify the flags EDWIN TOP and EDWIN CURRENT The following sections give brief descriptions of the most commonly used editor commands Other editor commands are listed in Appendix II 2 12 1 Top Levels lt Edn gt OK Exit the editor with the current wff 2 12 2 Printing lt Edn gt P Print the current expression in short format i e some subformulas will be replaced by amp lt Edn gt PP Pretty print a wff lt Edn gt PS_ Print a wff showing all brackets and dots lt Edn gt PT Print a wff showing types 2 12 3 Labels lt Edn gt Cw label Assigns a label to the edwff but does not change the edwff You can use the label to refer to this wff later 2 12 4 Moving Commands lt Edn gt 0 Move up one level i e undo the last L R D or A command Note that 0 stands for the numeral zero lt Edn gt A For an expression like P x y delete the rightmost element in this example the result will be to make Px the current expression For a quantified expression move to the quantified variable lt Edn
72. pathname instead e g instead of entering foo work enter afs andrew usrll adn0z foo work KEKE KKK KKK KKK KK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KKK KK KK KK KKK KKKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKK KKK K ANNOUNCING ETPS can now be run on the sun3 35 workstation type as well as on the Microvax The more memory on the machine the faster ETPS will run To check the amount of memory available on a Sun 3 type etc dmesg grep avail in your typescript KKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK Loading changes done Loading afs andrew cmu edu math etps etps ini Finished loading afs andrew cmu edu math etps etps ini lt l gt Exercise X5209 100 POWERSET D OA INTERSECT E OA POWERSET D INTERSECT POWERSET E PLANI lt 2 gt ext P2 LINE Line with Equality 100 gt PI LINE Universally Quantified Equality 99 x GWFF Universally Quantified Variable No Default gt S OA 99 FORALL S OA POWERSET D OA INTERSECT E OA S POWERSET D INTERSECT POWERSET E
73. ple This is a remark Strings may contain lt Return gt but no double quotes FILESPEC A file specification of the form lt dir gt name ext name ext or simply name For example lt FP01 gt EXAMPLE1 MSS The defaults for dir and ext are usually correct and it is enough to specify name LINE The number of a line LINE RANGE A range of lines from M through N written M N where M and N are positive integers and M N As shortcuts one may write M which represents the range M M M which stands for the range from line M through the last line of the current proof and N which represents the range from the first line of the proof through line N Hence represents the range consisting of every line in the proof EXISTING LINE The number of a line in the current outline PLINE The number of a planned line GWFF A well formed formula wff ETPS prompts you for a GWFF if it needs a wff term or variable and it will usually tell you which one of these it expects in the brief help message in the prompt A GWFF can be one of the following 1 A string representing a wff in double quotes Strings may contain lt Return gt s for formatting purposes Case does matter for variables and constants like x y P For example x is not the same as X Case is ignored however for special keywords like quantifiers connectives etc All logical symbols must be separated by spaces In
74. ponding to existing proof lines then the wff asserted by that new line will have to be entered Thus in order to avoid typing in long wffs you should try to organize your work often by working up from the bottom so that such lines will be introduced before they are needed ETPS automatically applies the metatheorem that if H AandH c H thenH A so that normally you do not have to worry about expanding sets of hypotheses before applying inference rules Some rules use wffops operations on well formed formulae in their descriptions For example a rule might form the assertion of one line by substituting a term t for all free occurrences of a variable x in a wff A asserted in another line The new assertion would then be S t x A where S is the wffop performing the substitution The backquote tells ETPS that the application of a wffop is being asserted and not a wff However this substitution will only be allowed when t is free for x in A Thus the form FREE FOR t x A would appear in the restrictions for the rule FREE FOR is the wffop which checks that t is free for x in A A catalogue of the wffops used in inference rules is provided in Appendix III It is included in this manual only to help you understand the descriptions of the inference rules Now we shall give an example which demonstrates how to read a command Before proceeding the reader should look at the description of DEDUCT in Section
75. r 2 System Commands SUBPROOF pline Tells ETPS that you now wish to focus on the planned line pline This changes the current subproof it mainly affects the displays in the proofwindows the results of the P and PN commands and the defaults offered for outline manipulations commands SPONSOR pline existing linelist Tells ETPS to add the lines in the list existing linelist of existing proof lines to the list of sponsors for the planned line pline UNSPONSOR pline existing linelist Tells ETPS to remove the lines in the list existing linelist of existing proof lines from the list of sponsors for the planned line pline 2 6 Saving Work SAVEPROOF filename Saves the current natural deduction proof to the specified file in a form in which it can be restored Use RESTOREPROOF to restore the proof Overwrites the file if it already exists ROOF filename Reads a natural deduction proof from a file created by SAVEPROOF and makes it the current proof A security feature prevents the restoration of saved proofs which have been altered in any way RESTORE Ti mj SAVE WORK filename Starts to save subsequent commands in the save work file filename Notice that this is not necessary unless you want to specify your own filename before starting an exercise or if you did a STOP SAVE some time before A typical use would be to switch save work files when you are done with one exercise and are starting the next one without leaving E
76. re deleted DELETE ranges Delete ranges of lines from the proof outline PLAN existing line Change a justified line back to a planned line The next few commands allow you to change the numbers of lines in the proof or even change the order of lines as long as the conclusion of a rule of inference comes after the justifying lines All references to line numbers are 12 Chapter 2 System Commands changed automatically whenever the numbers are changed MOVE from to Moves a line in the proof ETPS checks to make sure the move is legal i e the lines justifying a given line appear before it in the proof MOVE range to move new start Move all proof lines in given range to begin at new start number but preserving the relative distances between the lines RENUMBERALL increment Renumbers all the lines in the proof with an increment of increment As a proof is constructed new lines must be inserted into the outline and given new line numbers between occupied line numbers A space allotted for this task is called a gap Gaps are indicated in the outline by ellipses and may be adjusted by the command MODIFY GAPS INTRODUCE GAP existing line increment Introduce a new gap or increase an existing gap above existing line by increasing the line numbers by increment of all lines beginning with line existing line MODIFY GAPS lower upper Removes unnecessary gaps in line numbers from the proof st
77. reted as deduct 100 Ifthe alias for pr was prove 1 foo 100 then pr x2106 would become prove x2106 foo 100 Note that any occurrences of in the alias definition that are meant to be expanded when the alias is invoked must be escaped with a backslash to keep them from being interpreted as history substitutions when the alias is defined If an alias is found the token transformation of the input text is performed and the aliasing process begins again on the new input line Looping is prevented if the first word of the new text is the same as the old by flagging it to prevent further aliasing The command ALIAS can be used to create or display an alias or to display all existing aliases The command UNALIAS can be used to delete an existing alias The following example will illustrate We define an alias lt 135 gt alias d deduct VIN 1 NI We show its definition lt 136 gt alias d deduct 1 lt 137 gt exercise x2106 lt 138 gt d 49 ETPS User s Manual This expands to deduct 1 but here is 0 TPS error while reading 1 Bad arg selector Last of range is less than first We ll remove this definition and try again lt 139 gt unalias d The selector is what we want lt 140 gt alias d deduct NUI lt 141 gt d This expands to deduct which is what we intend Suppose now that we have finished the proof lt 155 gt alias finish cleanup amp squeeze amp
78. rsion 6 1 x2108 tex Hyphenation patterns for english german loaded afs cs project tps tps doc lib tps tex 1 Output written on x2108 dvi 1 page 628 bytes Transcript written on x2108 log gt dvips x2108 o x2108 ps This is dvipsk 5 58f Copyright 1986 1994 Radical TeX output 1998 09 04 1219 gt x2108 ps lt tex pro gt 1 Eye Software gt lpr Pprinter x2108 ps We ll now resume our ETPS session The unix command fg continues the last job that was interrupted 30 Chapter 4 Sample Proofs gt fg Let s now prove this same theorem in a different way and save it in a new file lt 1l gt stop save File x2108 work written lt 2 gt save work SAVEFILE FILESPEC SAVE WORK file work work gt x2108b work lt 3 gt exercise x2108 100 FORALL x EXISTS y P x IMPLIES P y PLANI lt 4 gt indirect P3 LINE Line to be Proven by Contradiction 100 gt P2 LINE Line with Contradiction 99 gt H1 LINE Line with Assumed Negation 1 gt 1 1 FORALL x EXISTS y P x IMPLIES P y Assume negation 99 j FALSEHOOD PLAN2 We can always use indirect proof As you can see line 1 is negated so let s push in that negation lt 5 gt pushneg D1 LINE Line with Negation 1 gt D2 LINE Line after Pushing in Negation one Step 2 gt 2 1 EXISTS x EX
79. ructure Also gaps with length less than lower have their length increased to lower while gaps with length greater than upper have their length decreased to upper lower must be less than or equal to upper 7 SQUI EZE Removes unnecessary gaps in line numbers from the proof structure Leaves necessary gaps those just above planned lines alone There is no UNDO command in ETPS Usually one can undo the results of commands fairly easily by such measures as deleting lines from the proof However if this seems complicated the following procedure can often be used to restore the proof to one of its previous states ETPS is probably creating a save work file Execute the STOP SAVE command make a backup copy of the save work file for safety edit the save work file by deleting the commands you wish you had not executed then start a new ETPS and use RESTORE WORK with the edited save work file 2 9 Proof Assistance ADVICE Initially gives hints based on the current structure of the proof The next time it is executed it suggests the inference command based on the previous hint It repeats this flip flopping between hints and suggestions until it has no more suggestions Advice may not be available for some exercises ETPS will tell you if advice cannot be given and ask for confirmation if the advice would deduct points from your score CHECK STRUCTURE Finds those lines which are not integrated into the proof
80. s every command in the file this feature only saves a proof and later restores this proof thus avoiding the re execution of everything that was done to achieve this state It is however up to you to decide when to save a proof Although the auto saving feature starts to save your work whenever you start an exercise you need to explicitly use the command SAVEPROOF when you wish to save a proof Typically you will want to save the proof whenever you need to interrupt a session in which you are constructing a proof and wish to continue this proof later ETPS commands associated with saving work are described in Section 2 6 AS soon as you start an exercise but not a proof of your own theorem ETPS will save your commands with the appropriate arguments in a file The name of this file will be exercise work where exercise is the first exercise attempted in your current session with ETPS When ETPS is saving work it echoes every character you type in a stream obtained by opening the save work file The echo stream is closed only when the user issues the command STOP SAVE or the command EXIT to exit ETPS in the usual way The save work file is not available until ETPS closes this stream Chapter 1 ETPS User Interface One more caution When starting the same exercise in two different sessions the same filename will be used The work for the new attempt will overwrite the old file exercise work To save the old attempt rename it before
81. s strings such as O OA typically they are substrings of a string representing a wff and serve to give type information about the symbols in that wff e g p O OA If entered separately the opening and closing double quotes must still be provided Indeed all of the string input rules apply for example carriage returns may be embedded For more examples of entering typed wffs see Section 5 1 3 ETPS has a powerful type inference mechanism which makes explicit typing mostly unnecessary within wffs Often the type of one variable is enough to uniquely determine the type of every identifier in a wff Within a wff all occurrences of a variable are assumed to have the same type unless the contrary is specifically indicated If the type of a variable remains undetermined after all other type information has been used 1 is assumed Take care to specify types if you use type variables like a Also note that type inference is local i e the type of an identifier is determined anew for each wff parsed by ETPS 5 1 2 Abbreviations and Special Symbols ETPS allows polymorphic abbreviations These are abbreviations with variable type which may have multiple occurrences with different types in the same wff Since their special symbols cannot be typed on most keyboards there is a long form of each of them which has to be used in ETPS The following is a temporary list of special symbols the binary operators ordered accor
82. stitutions in italics 38 prove A and B and C implies B or C foo 100 39 deduct 99 50 deduct 100 99 50 40 econj 39 econj 50 41 e 0 econj 42 texproof implies 2 proofl mss texproof foo_proofl mss One cautionary note It is unwise to use absolute references to input line numbers e g 25 in your work files because when the file is executed again it is unlikely that a particular line numbered n will be the same as line n was when the work file was created You may wish to know what a command history substitution will look like without executing it In order to do that merely choose a word that is not a command such as foobar and prefix your history substitution by that word ETPS will first echo the substituted line then just complain that foobar is an unknown command I 4 Aliases ETPS maintains a list of aliases which can be created printed and removed by the ALIAS and UNALIAS commands Each input line is separated into distinct commands and the first word of each command is checked to see if it has an alias If it does then the text which is the alias for that command is reread with the history mechanism available as though that command were the previous input line The resulting tokens replace the command and argument list If no history references appear then the argument list is not changed As an example if the alias for ded is deduct the command ded 100 would be interp
83. t of the top level prompts A certain number of previous commands are saved by ETPS the number saved is determined by the flag HISTORY SIZE The previous command is always saved In addition each line is parsed into a series of tokens Unlike the C shell these tokens are not distinguished simply by surrounding whitespace but rather by their Lisp syntax All that the user needs to know is that in general each argument entered on a command line will be considered a separate token On each input line the tokens are numbered from left to right beginning at 0 For example the input line lt n gt rulep 27 1 2 7 14 would be parsed into three tokens rulep 27 and 1 2 7 14 which would be numbered 0 1 and 2 47 ETPS User s Manual respectively The HISTORY command is used to examine the list of input lines that have been saved by ETPS It takes two arguments the first being the number of lines to show defaulting to the entire list and the second being whether to show them in reverse numerical order defaulting to no The number of each input line is also given The lines are saved in the history list as they appear after all history substitutions are made Previous lines can be referred to using the following input line specifiers In the command line whose number is n t n the input line that was entered n lines above the current one ka the previous line str the most recent command that begins with the string str 2str
84. tem Command 10 12 31 32 33 43 PN System Command 10 12 64 Table of Contents 1 ETPS User Interface 2 1 1 Introduction 1 2 Saving and Restoring Your Work 1 3 Exiting and Reentering ETPS 1 4 Top level Interaction 1 5 Using Commands and Defining Wffs 1 6 Flags and Amenities 1 7 Bugs and Error Messages System Commands 2 1 Communication 2 2 Starting and Finishing 2 3 Starting the Java Interface 2 4 Proofwindows 2 5 The Current Subproof 2 6 Saving Work 2 7 Printing 2 8 Rearranging the Proof 2 9 Proof Assistance 2 10 Higher Order Logic 2 11 Flags and Review 2 12 ETPS Editor 2 12 1 Top Levels 2 12 2 Printing 2 12 3 Labels 2 12 4 Moving Commands 2 12 5 Substitution 2 12 6 Negation movers 3 Inference Rules 4 5 3 1 How to Read Inference Rules 3 2 Quick Reference to Rules 3 3 Special Rules 3 4 Miscellaneous Rules 3 5 Propositional Rules 3 6 Negation Rules 3 7 Quantifier Rules 3 8 Substitution Rules 3 9 Equality Rules 3 10 Definition Rules 3 11 Lambda Conversion Rules Sample Proofs 4 1 Example 1 4 2 Example 2 4 3 Example 3 Type Theory in ETPS 5 1 Using ETPS for Type Theory 5 1 1 Types in Higher Order Logic 5 1 2 Abbreviations and Special Symbols 5 1 3 Some Examples of Higher Order Wffs 5 2 Example of a Proof of a Higher Order Theorem ere SANRWWNe Appendix I Amenities L1 Control characters for Unix I 2 Command Sequences
85. the most recent command that has a token containing the substring str Here are some examples Suppose we had the following output from the HISTORY command lt 10 gt history 5 exercise x2106 pstatus p pall history 5 Ow OID Then as input line 11 we could refer to line 7 by ps or 4 or even by tat Used alone the above references merely insert every token of the line referred to into the the current input line In order to select particular tokens from an input line a colon follows the input line specifier along with a selector for the intended tokens Here is the syntax for the token selectors where x and y indicate arbitrary token selectors 0 first command word n n th argument first argument i e 1 last argument word matched by immediately preceding str search x y range of words from the x th through the y th y abbreviates 0 y abbreviates or nothing if only 1 word in input line referred to x abbreviates x x like x but omitting word The separating the event specification from the token selector can be omitted if the token selector begins with a 5 or Going back to our example we can then create the input line II help x2106 by entering help 5 orhelp ex orhelp 2 48 Appendix I Here is a longer example of the use of history substitutions We will omit the output of the commands themselves showing only the results of history sub
86. to derive an equality at type o from an equivalence LET 24 Rule to produce a new variable which will represent an entire formula during part of a proof SUBST 24 Substitution of Equality Performs whichever of the SUBST L and SUBST R rules is appropriate SUBST L 25 Substitution of Equality Replaces some occurrences of the left hand side by the right hand side SUBST R 25 Substitution of Equality Replaces some occurrences of the right hand side by the left hand side SUBST EQUIV 25 Substitution of Equivalence SYM 25 Symmetry of Equality Definition Rules EDEF 25 Rule to eliminate first definition left to right EQUIV WFFS 25 Rule to assert equivalence of lines up to definition IDEF 25 Rule to introduce a definition Lambda Conversion Rules LAMBDA 26 Convert between two equivalent lambda expressions LCONTR 26 Rule to put an inferred line into Lambda normal form LEXPD 26 Rule to put a planned line into Lambda normal form 3 3 Special Rules RULEP Justify a line by Rule P Infer B from Al and and A provided that A A AA 2B isa substitution instance of a tautology As a special case infer B if it is a substitution instance of a tautology The first argument must be the line to be justified the second argument must be a list of lines possibly empty from which this line follows by Rule P The flag RULEP MAINEN controls which of two functions will be used by RULEP When RULEP MAINE
87. to use ABORT Q trl U Delete current input line Ctrl W Delete last input word ETPS User s Manual The next three characters are special on the top level only and are currently not to be used when typing in arguments to commands Complete the name of the current command If COMPLETION OPTIONS is NIL this works only if there is a unique completion if it is T you will be offered a list of completions to choose from lt Escape gt Exactly equivalent to This character can confuse some terminals we recommend using instead 2 When typed at the top level ETPS will list all the available commands Note that must be followed by a lt Return gt lt Linefeed gt This starts a new line on the terminal without terminating the input This is useful for long command arguments 1 5 Using Commands and Defining Wffs The commands available in ETPS are classified into system commands and inference commands The system commands which are discussed in Chapter 2 deal with communication facilities starting and finishing a session with ETPS the Java interface proofwindows the current subproof saving work printing rearranging the proof getting assistance displaying types in higher order logic setting flags and locating and constructing wffs The inference commands which are discussed in Chapter 3 correspond to inference rules They transform one proof outline into another by applying the rules Common to all commands
88. will return you to the point at which you typed PUSH Ctrl G lt Return gt or Ctrl C To abort This is a system dependent feature and one or the other or both may not work on your Chapter 1 ETPS User Interface system Using this command may cause problems for any save work file that is being created so it may be better to use ABORT If a mistake in an argument can be detected right away ETPS will complain and let you try again Sometimes ETPS will note that something is wrong after all the arguments are typed in You will then get an error message and be thrown back to the top level of ETPS The argument name is usually only important when typing in arguments to inference commands If you are in doubt what wff you are supposed to type in now look at the description of the inference rule The name of the argument will be the same as the name of a wff in the rule description The argument type tells you what kind of object ETPS expects The most important argument types are listed below You may omit most of the rest of this section when first reading this manual However be sure to read the description of GWFF ANYTHING Any legal LISP object SYMBOL Any legal LISP symbol BOOLEAN A Boolean value NIL for false T for true YESNO y or yes to mean YES n or no to mean NO INTEGER A nonnegative integer POSINTEGER A positive integer STRING A string delimited by double quotes For exam
89. x IMPLIES S f S b Ae ke AP Ss ADe pg p EQUIV a p 0 VA 3 VP FORALL A O FORALL A O VA Jf VP o oo 0 00 EQUIV LAMB o ay E EQ EXISTS f FORALL P P LAMBDA p A EQUIV P f EXISTS f OI FORALL P EQUIV LAMBDA r LAMBDA s r IMPLIES s AND s IMPLIES r p q UIV q 0 DA r O LAMBDA s O r IMPLIES s AND s IMPLIES r pa P Ap A P f O OI P LAMBDA p I A EQUIV P f P Ap A P f 41 ETPS User s Manual FORALL A O EXISTS 00 FORALL P P LAMBDA p A EQUIV P f FORALL A O EXISTS 00 FORALL P O 00 P LAMBDA p O A EQUIV P f 5 2 Example of a Proof of a Higher Order Theorem The following is an annotated transcript of part of a proof in type theory Basic familiarity with ETPS is assumed gt etps etps for issar Version from Saturday September 23 1989 at 5 59 15 c Copyrighted 1988 by Carnegie Mellon University All rights reserved KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKK WARNING Be sure that you when you begin ETPS your current directory is one for which you have write access g your home directory KKEKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKK KKK KKK K WARNING You cannot use the Unix convention in specifying file names Use the full
90. y issue the ETPS command SCRIPT Note however that the file obtained this way cannot be used to restore your work as described earlier in this section 1 3 Exiting and Reentering ETPS If you wish to end a session with ETPS or temporarily interrupt your work use the EXIT command This allows ETPS to halt gracefully and to close an open save work file If you are running ETPS under Unix and wish to interrupt a session temporarily you can also use Ct r1 Z This will return you immediately to the monitor if you are currently saving work the save work file will not be closed Thus any work will be lost unless you return to ETPS Once out of ETPS you can run other programs such as TEX To reeneter ETPS use the Unix command fg 1 4 Top level Interaction In ETPS every command line is identified with a statement number shown in angle brackets After a while command line numbers are reused i e commands issued long ago are forgotten The following is a list of useful control characters and their meaning in ETPS Some of them may not work under certain operating systems or display environments Additional control characters are discussed in Section I 1 Rubout gt Delete the last character and back over it A Ctri C Quit current command and return to top level In some implementations of ETPS you must use Ctrl G instead Using this command may cause problems for any save work file that is being created so it may be better
91. you enter x 1 I then it will print as x 1 I when the style is generic and PRINTTYPES is T e Entering x1 results in x1 not x 1 i e superscripts will not be created from the user s input unless explicitly indicated 2 A number of a line in the proof for example 100 ETPS will replace it with the wff asserted in that line Ow A label referring to a wff or the name of an exercise or lemma A label can be assigned by the CW command see page 15 4 ed gwff which allows you to locate a sub expression of another GWFF For example ed 100 can be used to extract a subformula from the assertion of line 100 See Section 2 12 for an explanation of how to use this option A A backquoted form calling a wffop For example S x y A is the wff resulting from the substitution of x for y in A See Appendix III for the most commonly used wffops GWFFO A gwff of type o Two special constants of type o are provided TRUTH and FALSEHOOD These gwffs act just as you might expect e g TRUTH pv p and FALSEHOOD pa p After running a proof through SCRIBE TRUTH will print as T and FALSEHOOD will print as L GVAR A gwff which must be a logical variable TYPESYM The string representation of a type symbol See Section 5 1 1 BOOK THEOREM A theorem in the book See the PROBLEMS command page 9 EXERCISE An exercise which may be assigned PRACTICE An unscored practice exercise TES
92. ystem Command 9 32 CMRI G Editor command 53 61 CMRG Editor command 53 CMUT Editor command 53 CMUT Editor command 53 CNF Editor command 53 CNTOP Editor command 53 COMPLETION OPTIONS Flag 4 COND 40 CONTAINS DEFN 55 Control characters 3 47 Current subproof 10 CW Editor command 6 15 D Editor command 15 DB Editor command 52 DEDUCT Inference Rule 18 21 33 35 43 44 DELETE System Command 12 DELETE System Command 12 DELETE HYPS Inference Rule 18 20 DELWEAK Editor command 51 DEPTH System Command 12 DISJ IMP Inference Rule 18 21 DIST CTR Editorcommand 53 DIST CTR Editor command 53 DIST EXP Editorcommand 53 DIST EXP Editor command 53 DNEG Editor command 53 DNEG Editorcommand 53 DONE System Command 9 30 32 34 38 DUPW Editor command 54 DW Editorcommand 51 DW Editorcommand 51 ECONJ Inference Rule 18 21 36 43 D 30 D System Command 14 DEF Inference Rule 19 25 43 DILL Editor command 54 DWIN CURRENT Flag 15 DWIN TOP Flag 15 GEN Inference Rule 19 23 29 34 D PRFW System Command 1 10 EG Inference Rule 19 22 P Editorcommand 52 EQP 40 EQUIV 40 EQUIV IMPLICS Inference Rule 18 21 EQUIV WFFS Inference Rule 19 25 EQUIVS 40 ETA Inference Rule 26 ETAB Editorcommand 51 ETAC Editorcommand 51 ETAN Editor command 51 52 ETAX Editor command 51 EXECUTE FILE System Command 7 11 EXERCISE Argument Type 6 EXERCISE System Command 1 9 29 31 33 42 EXI

Download Pdf Manuals

Related Search

Related Contents

Infotainment System  Jabra BIZ 2400 Mono, 3-in-1  Frigidaire 318200404 Range User Manual  "user manual"  DT-212 DT-213 DT-214  Manuel de Formation Produits    National Instruments NI 9229 User's Manual  Delta Electronics S36SS User's Manual  Je me réveille  

Copyright © All rights reserved. Failed to retrieve file