### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# Discrete and Foundational Mathematics MATH 387

BSU

GPA 3.72

### View Full Document

## 13

## 0

## Popular in Course

## Popular in Mathematics (M)

This 259 page Class Notes was uploaded by Breanne Schaden PhD on Saturday October 3, 2015. The Class Notes belongs to MATH 387 at Boise State University taught by Melvin Holmes in Fall. Since its upload, it has received 13 views. For similar materials see /class/217989/math-387-boise-state-university in Mathematics (M) at Boise State University.

## Reviews for Discrete and Foundational Mathematics

### What is Karma?

#### Karma is the currency of StudySoup.

#### You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 10/03/15

Math 387 Lecture Notes M Randall Holmes March 17 2004 Contents 1 Introduction 4 2 Monday January 12 4 21 Basic operations of propositional logic 4 22 The method of truth tables 6 23 Tautology entailment and equivalence 7 24 Informal introduction to natural deduction 8 3 Natural deduction formally introduced 9 31 Rules for conjunction 10 32 Rules for implication 10 33 An example 11 34 Rules for negation 12 35 Rules for disjunction 12 36 Rules for the biconditional 13 37 Derived rules 14 4 Wednesday January 14 20 5 Friday January 16 23 6 Tuesday Jan 20 25 61 Derived rules 25 62 Soundness and completeness 26 63 Expressive completeness 26 64 A digression one point basis 27 65 Development of algebraic rules 28 7 Wednesday January 21 31 71 Alternative interpretations and duality 32 8 Friday January 23 32 9 Monday January 26 sequent calculus introduced 36 10 Tuesday January 26 39 101 Sequent calculus continued 39 102 Natural deduction rules for quanti ers 42 11 Wednesday January 28 44 12 Friday January 30 44 13 Monday February 2 46 131 Sequent examples 46 132 Understanding a rule of sequent calculus as a distributive law in boolean algebra 48 14 Notes on the cut rule written Monday but not lectured Tues day 49 141 The relationship between the sequent calculus and natural de duction 49 15 Tuesday February 3 completeness of natural deduction 52 16 Wednesday February 4 58 161 Deriving rules for new logical operations 58 162 Translating natural deduction proofs into sequent proofs the need for the cut rule 60 163 Quanti ers reintroduced 62 164 Sequent rules for quanti ers 65 17 February 6 2004 65 18 February 9 2004 66 19 Tuesday February 10 20 Wednesday February 11 21 Friday February 13 22 Tuesday February 17 de Morgan laws for quanti ers 23 February 18 2004 231 first proof 232 second proof 24 February 20 2004 25 February 23 2004 251 first proof 252 second proof 26 February 24 2004 27 February 27 2004 28 March 1 2004 substitution and equality 281 Substitution 282 Equality 29 March 2 2004 30 March 3 2004 301 Equality rules for natural deduction 302 Numerical quanti ers 303 Completeness of sequent calculus 31 March 5 2004 Arithmetic Made Dif cult 32 Monday March 8 2004 commutativity of addition 33 March 9 2004 34 March 10 2004 68 68 69 77 80 80 82 83 98 101 106 111 35 Friday March 12 112 36 March 15 2004 set theory prerequisites for counting 115 1 Introduction This document contains the lecture notes for the foundational part of Math 387 section 1 spring 2004 The notes are organized by day I will provide the notes for each day either just before or just after lecturing If I provide them early I may of course not complete the planned lecture in which case I will insert the new date heading at the appropriate point 2 Monday January 12 21 Basic operations of propositional logic For the moment we use capital letters such as P Q R to represent state ments The only thing that interests us about the statements represented by capital letters is their truth value whether they are true or false We de ne operations on statements correspon 1ing though sometimes not precisely to certain conjunctions in English IP means not P or it is not the case that P The operation rp resented by I is called negation The English is unambiguous we can be certain that if P is true IP will be false and if P is false IP will be true We can summarize this in the following truth table P IP T F F T P Q means P and Q The operation represented by is called conjunction Again this is unambiguously determined by the English PVQ means P or Q The operation represented by V is called disjunc tion Here English is ambiguous If P is true and Q is false or vice versa it is clear that P V Q should be true and if P and Q are both false it is clear that P V Q should be false but it is not clear What truth value to assign if P and Q are both true The usual convention in mathematics is to use the inclusive or with the following truth table The operation exclusive or or xor will be represented by the notation EB and has the following truth table The notation P gt C2 is said to denote if P then Q It is a matter of philosophical debate Whether the meaning of if P then Q really depends only on the truth values of P and Q In mathematics the convention is to suppose that it does An expression of the form P gt C2 is called an implication The truth table for implication is The notation P ltgt Q is defined as denoting P if and only if Q which is often abbreviated as P iff Q This is true exactly when P and Q have the same truth value An expression of the form P ltgt Q is called a biconditional The truth table for the biconditional is 0 Order of operations I binds most tightly followed by A then V then gt then ltgt and EB the latter will seldom be used We can also use associa tivity of V and to drop some parentheses H and EB are also associative for what it is worth It never hurts to use redundant parentheses to make your meaning clear 22 The method of truth tables We have already seen truth tables used to de ne propositional operations They can also be used to analyze the behavior of complex propositions built using these operations For example we can use truth tables to show that P gt Q has the same meaning as IP V Q our convention on order of operations lets us write this instead of IP V Q Compare this with the truth table for P gt Q We give an example of a logical truth PAQ gt P which can be written P C2 gt P by order of operations veri ed by truth tables A different table style avoids the necessity of copying out many subex pressions in a truth table here we write the values of each subexpression below the symbol for its top level operation 6 23 Tautology entailment and equivalence In this section we introduce a new kind of variable script variables A B C a script variable stands for any expression of propositional logic not just a single propositional letter Strictly speaking we could have used script variables in our de nitions of propositional connectives IA is a formula of propositional logic for any expression A not just for propositional letters P as our less careful usage above might suggest For any formula A we say that A is a tautology symbolically l A if A is true no matter what values are assigned to the propositional letters appearing in A For example we showed l P C2 gt P above We have special terminology for tautologies which are implications or bicon 1itionals l A gt B may be written A l B and read A entails B The example just shown can be written in the form P Q l P l A ltgt B may be written A E B and read A is logically equivalent to B For example our argument that P gt Q has the same meaning as IP VQ could also be used to show that P gt C2 ltgt IP V Q is a tautology and so tlxatPaQE IPVQ It is important to notice that l A A l B and A E B are not formulas of propositional logic lIoreover A l 8 means something different from A gt B and similarly A E 8 means something different from A ltgt B For example P gt C2 is a sentence of propositional logic which may be true or false depending on what values are assigned to P and Q while P I Q is a statement about propositional logic which is false because P gt C2 is not a tautology 24 Informal introduction to natural deduction The method of truth tables is a complete technique for finding logical truths tautologies and determining entailments and equivalences in propositional logic However it is not very practical because the truth table for a formula containing 7 propositional variables will contain 2quot rows The truth table description of the behaviour of a logic circuit with 100 different inputs not 100 different logic gates as I mistakenly said in class would have 2100 N 1030 rows which can t be implemented in practice A peculiar feature of a proof by truth table is that all proofs of formulas with the same number of variables are essentially the same size since every possible assignment of values to the variables must be consi 1ered in 1ivi 1ually There are techniques of proof in propositional logic that can be more efficient it is unknown whether there is a technique of proof for propositional logic that is always more efficient for all known methods of proof in propositional logic the worst case bound for the proof of a tautology is the same 2quot as it is for the method of truth tables it is suspected but is not known that this will be true for any technique of proof it would be very exciting if a truly efficient proof technique could be found The method which we briefly and quite informally introduce here is called natural 1e 1uction there are various systems of natural 1e 1uction someone else s formalization could differ in detail from mine For each operation of propositional logic natural de 1uction provides a strategy for proving propositions with that operation as their top level op eration and a method for using propositions with that operation as their top level operation to deduce new conclusions For example to prove A B we prove A then prove B If we have a premise A B we can deduce A and B as conclusions To prove A gt B assume A add it as a new premise and prove B If we have A and A gt B as premises we can draw the conclusion 8 this is called the rule of modus ponens We present a natural de 1uction proof of P gt QQ gt R gt P gt R Goal top P gt Q Q gt R gt P gt R Assume 1 P gt Q Q gt R for Goal 1 P gt R Assume P 2 for Goal 2 R from 1 get 3 P gt Q from 2 and 3 get 4 Q by modus ponens from 1 get 5 Q gt R from 4 and 5 get R by modus ponens which is goal 2 and completes the proof of goal 1 which in turn completes the proof of the top goal This is not in our nal formalism but has the right structure Compare this with the truth table proof of the same tautology NQH w wwwwssss wwsswwss wewswsws wwwwssss sssswmssi wwsswwssg sswswwwsgt MMHHMMSSE sswssswsl wewswswsa ssssssssl wwwwssssg sssswswsl wewswswsa The natural de 1uction proof is smaller and implements a more intelligent and in some sense natural approach to proving the result 3 ZNaturaldeductknl nwna y39hmroduced In this section we present the formal details of our system of natural deduc tion Later on I plan to prove that every tautology and only the tautologies of propositional logic can be proved using natural 1e 1uction Each logical operation conjunction implication negation disjunction has two kinds of rules associated with it introduction rules which allow con clusions built with that operation to be proved and elimination rules which allow information to be extracted from premises built with that operation In this section I will usually not make the distinction between proposi tional variables P and script variables A standing for complex expressions which I intro 1uce 1 above the rules of natural deduction are valid if complex expressions are substituted for the letters appearing in them 31 Rules for conjunction Conjunction introduction P Q P Q Conjunction elimination P Q P or P Q Q In each rule the items above the line are premises which can be taken from earlier lines of proofs The item below the line is the conclusion a new line for the proof The rules can be abbreviated ci and ce the two different forms of ce could be called ce 1 and ce 2 but this seems too pedantic 32 Rules for implication Implication elimination modus ponens P H Q This rule may be abbreviated either ie or mp according to taste 10 Implication introduction This rule has a rather different structure 1 P hypothesis for implication introduction Goal Q representing an unknown number of proof lines n Q we don t know what rule we use to get the conclusion n1 P gt C2 implication intro 1uction lines 1 11 The box indicates a subproof with the additional hypothesis P No line of the subproof can be used outside the subproof Lines outside the subproof may be used in the subproof unless they belong to some other subproof which does not contain the given subproof This rule embodies the natural strategy for proving an implication P gt C2 assume P and prove Q this proof allows you to conclude that P gt C2 is true whether P is true or not if P is true we use the auxiliary proof to show that Q is also true so P gt C2 is true if P is false P gt C2 is vacuously true The line labelled Goal is a comment it tells us what conclusion we need to close the subproof 33 An example We use the rules for implication and conjunction to prove P gt C2 C2 gt R gt P gt R this is the formalization of the last example in the previous section Goal P gt C2 C2 gt R gt P gt R Since this is an implication we attempt to apply implication intro 1uction 11 1 P gt gt R hypothes1s for 11 Goal P gt R Once aga1n we attempt 11 2 P hypothesis for 11 Goal R 3 P gt Q e l1ne 1 4 Q mp l1nes 23 5 6 Q gt R e l1ne 1 R mp l1nes 45 7 P gt R 1mpl1cat1on 1ntro 1ut1on l1nes 2 6 8 P gt gt R gt P gt R 11 l1nes 1 7 34 Rules for negation We resume the development of rules for the other log1al operat1ons negation introduction Th1s 1s another rule of the same form as 1mpl1ca t1on 1ntro 1ut1on 1 P hypothes1s for negat1on 1ntro 1ut1on Goal ontrad1ct1on represent1ng an unknown number of proof l1nes n Q IQ we don t know what rule we use to get the onclus1on n1 IP negat1on 1ntro 1ut1on l1nes 1 n We prove that P 1s false by assum1ng P and deduc1ng a ontra 11t1on There 1s a negat1on el1m1nat1on rule but 1t 1s l1sted among the der1ved rules below 35 Rules for disjunction Each of the rules for 11sjunct1on 1s l1ke the rule of onjunct1on el1m1nat1on 1n hav1ng two symmetr1c forms We w1ll not requ1re use of separate names for the two forms of each rule 12 Disjunction elimination Either pvo ng I pvo Q Disjunction introduction Either 1 IP hypothesis for disjunction intro 1uction Goal Q representing an unknown number of proof lines n Q we don t know what rule we use to get the conclusion n1 P V Q disjunction intro 1uction lines 1 11 I 1 Q hypothesis for disjunction intro 1uction Goal P representing an unknown number of proof lines n P we don t know what rule we use to get the conclusion n1 P V Q disjunction intro 1uction lines 1 11 36 Rules for the biconditional For now our of cial rules for the biconditional amount to a de nition of PHQasP gtQQ gtP Biconditional introduction wakoam PHQ 13 Biconditional elimination P ltgt Q 1 gt Q A Q gt P The following set of rules might be found more natural These are the elimination rules P w t t w t O39UQ 39UQQ O39UQ l l Tl is is the inrrm lncrirm rule 1 P hyp for biconditional intro 1uction ii Q n1 Q hyp for biconditional intro 1uction ni P ni1 P ltgt Q bicon 1itional intro 1uction lines 1 n n1 ni These rules can be derived from the of cial de nition this is left as an exercise for the reader 37 Derived rules The rules already given are the basic rules of our system but of course there are many simple rules of inference that are equally basic to reasoning in practice In this subsection we derive some of them 14 Excluded middle Goal P V IP 1 IP hypothesis for disjunction intro luction 2 IP copy line 2 3 P V P disjunction intro luction lines 1 2 We can use this to prove any statement of the form P IP and rather than reproduce this proof Whenever we do this we use the new rule PVIP which we call excluded middle or exc mid Note that this rule does not require any premises Double negation Under this heading we prove the rules for intro luction and elimination of double negations and introduce the method of proof by contra liction Double negation introduction 1 P Goal IIP 2 IP hypothesis for negation intro 3 P IP ci lines 12 4 IIP negation intro lines 2 3 This justi es the rule of double negation intro luction dni P p Double negation elimination 1 P Goal P 2 P V IP exc mid 3 P Lil lines 12 This justi es the rule of double negation elimination dne p P Proof by contradiction Goal P 1 IP hypothesis for n i n Q Q n1 IIP negation intro lines 1 n n2 P 1ne line n1 justi es the rule of proof by ontra 1ition which is just one line shorter Goal P 1 IP hypothesis for proof by contradiction i112 Q n1 P proof by ontra 1ition lines 1 n Modus tollens The rule of modus tollens mt is the additional implica tion elimination rule P gt C2 rQ IP It is justi ed by the following proof 1 P gt C2 2 Q Goal IP 3 P hypothesis for n i 4 Q mp lines 13 5 Q Q i lines 24 16 6 IP ni lines 3 5 Simple disjunction introduction The rules of simple disjunction intro duction are 71 P Q and Q P Q The formal proofs follow 1 P Goal P V Q 2 Q hypothesis for disjunction intro Goal P 3 P copy line 1 4 P V Q di lines 2 3 The other proof is very similar 1 Q Goal P V Q 2 IP hypothesis for disjunction intro Goal Q 3 Q copy line 1 4 P V Q di lines 2 3 The simple disjunction rules sdi are often presented as the basic disjunction intro 1uction rules In this case one will also need reasoning by cases the next derived rule as an elimination rule and excluded middle Our choice of basic disjunction rules is more economical Reasoning by cases The rule of reasoning by cases cases for short is PVQ P gtR Q gtR The formal proof follows 1 P v Q 2 P gt R 3 C2 gt R Goal R IR hypothesis for proof by contra 1iction IP mt lines 24 Q de lines 15 R mp lines 36 R IR ci lines 4 905130er 9 R proof by contradiction lines 4 8 negation elimination P P Q This expresses the idea that anything can be deduced from a contra diction any proposition is implied by a false proposition as is clear from the truth table for implication 1 P premise 2 IP premise Goal Q 3 Q hyp for proof by contra 1iction 4 P IP ci lines 12 5 Q proof by contradiction lines 3 4 This proof might make one vaguely ill since the contra 1iction derived in the box has nothing to do with the hypothesis intro 1uce 1 in the box but it is formally correct 18 16 Morgan rules T110 10 Morgan 111108 2110 as follows M pA Q 1 IP V Q pr0mis0 Goal IP IQ Goal IP 2 P 11yp for 111 3 P V Q sd1 11110 2 4 P V P V 01 14 5 IP 111 111108 2 4 Goal IQ 6 Q 11yp for 111 7 P V Q sd1 11110 6 8 P V IP V 01 17 9 Q 111 111105 6 8 10 IP IQ 01 59 pA Q pVQ 1 IP IQ pr0mis0 Goal IP V Q 2 P V Q hyp for 111 3 IP 00 11110 1 4 Q 00 11110 1 5 P 10 111108 24 6 P IP 01 111108 53 7 P V 111 111108 2 6 M pv Q 19 1 IP Q premise Goal IP V IQ 5 3 IIP hyp for 11 Goal IQ Q hyp for 111 P d11e line 3 P Q 1 lines 54 4 5 6 7 P IP 1 lines 16 8 Q 111 lir1es 4 7 9 IP V IQ 11 lir1es 3 8 p v Q quot1 Q 1 IP V IQ premise Goal IP Q P Q hyp for 111 P e line 2 IIP 1111 line 3 Q 1e li11es 41 Q e line 2 Q Q 1 lines 56 rlgvsleswso 8 P 111 lir1es 2 7 4 Wednesday January 14 Today we 111 proofs in class and we will continue on Friday The theorems proved today were IAB IAVIB with the following proof Goal IA B gt A V IB 20 1 A B 11ypfor11 G 2311 A B 2 IIA 11yp for 11 G 211 B 3 B 11yp for 111 Goal contradiction 4 A 1110 11110 2 5 A B 01 111108 34 6 A B IA B 01 16 7 B 111 111108 4 6 8 IA V B 111 111108 2 7 9 A B gt IAV B 11 111108 1 8 and PVQ gtRlt gtP gtRAQ gtR Goal PVQ gtRlt gt P gtRQ gtR A conjunctive goal can b0 b1ok0n into two subgoals Goal PVQ gt R gt P gt R Q gt R 1 P V gt R 11yp for 11 Goal P gt R C2 gt R G 211 P gt R 2 P 11yp for 11 3 P V Q sd1 11110 2 4 R mp 111108 13 5 P gt R 11 111108 2 4 Goal C2 gt R 6 Q 11yp for 11 7 P V Q sd1 11110 6 8 R mp 111108 17 9 C2 gt R 11 111108 6 8 7 P gt R C2 gt R 01 111108 59 8 PVQ gtR gtP gtRQ gtR Goal P gtRQ gtR gtPVQ gtR 21 1b P gt R gt R l1yp for 11 Goal P V C2 gt R 2b P V l1yp for 11 Gal R 3b IR l1yp for proof by contradiction Goal contradiction 4b P gt R 00 11110 1b 5b IP modus toll0ns lin0s 3b4b 6b Q 10 lin0s 2b6b 7b C2 gt R 00 11110 1b 8b R modus pon0ns lin0s 6bb 9b R IR 01 lin0s 3b8b 10b R proof by contradiction lin0s 3 9 11b P V gt R 11 lin0s 1 9 12b P gt R gt R gt P V gt R 11 lin0s 1 11 13111 gt RWQ gt R gt two gt RPVQ gt R gt P gt R Q gt 01 lin0s 8 12b 14P gt R C2 gt R ltgt P V C2 gt R biconditional introduction 11110 13 0110 issu0 which cam0 up 111 class which is worth r00ording is how to l1andl0 tl10 situation of a conjunction as a goal Goal A B I us0d tl10 script l0tt0rs to 0mpl1asiz0 tl10 fact that tl10s0 ar0 unknown but compl0x 0xpr0ssions tl10y ar0 c0rtainly not propositional l0tt0rsl Wl1il0 w0 ar0 doing natural d0 1uction I won t usually draw this distinction Th0 structur0 of tl10 proof will b0 Goal A 8 Goal A 111 A Goal 8 11 B n1 A B 01 lin0s 11111 Th0 proof of a biconditional will l1av0 this form if w0 us0 tl10 rul0 for boconditionals giv0n 111 tl10 l1om0work 22 Goal A ltgt 8 Goal A gt B m A gt 8 Goal 8 gt A n B gt A n1 A gt B B gt A i lines mn n2 A ltgt l3 biconditional intro from homework The rule you develop in homework problem 3 should involve subproofs something resembling the reasoning I give here could be used to justify the rule you develop 5 Friday January 16 We did more proofs at the board The tautologies which we proved were PAQ gtRltgtP gtQ gtR Goal PAQ gtRlt gtP gt Q gtR Goal P Q gt R gt P gt C2 gt R 1 P gt R hyp for ii Goal P gt C2 gt R 2 P hyp for ii Gwl C2 gt R 3 Q hyp for ii Goal R 4 P Q i lines 23 5 R mp lines 15 6 C2 gt R ii lines 3 5 7 P gt gt E ii lines 2 6 8 P gt R gt P gt gt R ii lines 1 Goal P gt C2 gt R gt P Q gt R 23 9 P gt gt R 11yp for 11 Goal P C2 gt R 10 P Q 11yp for 11 Goal R 11 P 00 11110 10 12 C2 gt R 1np 11n0s 9 11 13 Q 00 11110 10 14 R modus pon0ns 11n0s 12 13 15 P gt R 11 11n0s 10 14 16 P gt gt R gt P gt R 11 11110s 9 15 17 P gt C2 gt R ltgt P C2 gt R biconditiona1 introduction 11n0s 816 and AABVAAIB gtA Ga1 A B A IB gtA 1 A B V A IB 11yp for 11 G a1 A 2 IA 11yp for proof by contradiction Goal contra 1iction Goal IA B to 11s0 With 10 With 11110 1 3 A B 11yp for 111 4 A 00 11110 3 5 A IA 01 11n0s 24 6 A B 111 11110s 3 5 7 A B 10 11n0s 16 8 A 00 11110 7 9 A IA 01 11110s 28 10 A proof by contradiction 11n0s 2 9 11 A B V A B 11 11n0s 1 10 This is t110 proof W0 did 111 class At that tim0 W0 had not y0t intro 1uc0 1 t110 r1110 of proof by cas0s Wit11 proof by cas0s you g0t a 11111011 0asi0r proof W11ic11 W0 10av0 as an 0x0rcis0 24 6 ThesdayJan 20 6 1 Derived rules Here is a brief discussion of how to introduce and use a new rule At this point we do not discuss rules that involve subproofs boxes A rule such as P P gtQ is used in the following situation a P b P gt C2 c Q mp lines ab or more typically in a situation like this a A B b AAB gtCD c C V D mp lines ab Here the letters P and Q in the rule are replaced by the expressions AAB and C VD respectively All of our rules have the property that the letters in them can be replaced by arbitrary expressions as long as every occurrence of the same letter in the rule is replaced by the same expression The same is actually true of any proof in our system To prove a new rule such as vWAQ IP V IQ we can give a proof which has the expressions above the bar as premises and the expression below the bar as conclusion 1 P Q premise Goal P V IQ 2 IIP hyp for 11 Go 1 Q 3 Q hyp for 111 4 P dne line 2 5 P Q 1 lines 34 6 P IP 1 lines 16 7 Q 8 J V IQ 11 2 7 This completes the proof of the derived rule We give it the name deM 1 it is one of the de Morgan rules It can be used just like the basic rules a IIR U V V b IR V U V V deM 1 line a l39otice that the letters in the original rule have been replaced with com plex expressions The derived rule could be eliminated from the proof by in serting the complete proof from above with the appropriate substitutions using derived rules can make proofs much shorter We will give a formal treatment of how to develop rules with subproofs later you can see examples of such derivations above 62 Soundness and completeness A proof system for an area of mathematics is sound if all the statements it proves are correct It is complete if it can prove as a theorem every statement expressible in its language which is actually true We will prove later that our system of natural deduction is sound and complete We point out that we already have a sound and complete proof technique for propositional logic the method of truth tables What we will do today is develop an algebraic system of logic which we can prove to be sound and complete because it can be seen to implement the method of truth tables 63 Expressive completeness We use truth tables to demonstrate how any function of propositions which has a truth table can be expressed in terms of the operators A V and I For example 26 39 39 39 i i i i39 39 i i39 39 i i wswswswsm 39 39 i i39 ig The function fPQR this is a purely temporary notation can be represented by the expression PAQARPAIQARPAIQAIRVIPQIR This expression is a disjunction of conjunctions of propositional letters and negations of propositional letters Each conjunction represents one of the rows of the truth table There is one special case if all rows of the truth table are F we can use the contra 1ictory expression PIP to represent its value We also introduce the notations T and F for the truth values into our language We say that an expression in which negation is applied only to single letters and no disjunction appears as part of a conjunction is in disjunctive normal form DNF The expressions we derive from truth tables have the additional features that each conjunction contains the same letters in the same order sometimes negated and no conjunction or disjunction contains duplicated terms 64 A digression onepoint basis De ne a new propositional operation P l Q as IPQ I used a downward arrow for this in class but I don t know how to typeset it P l Q can be read Neither P nor Q in English We point out the following equivalences pspip PVQE W39U VQE PlQEU lQHU lQ 27 PAQE l J V Q E J l IQEU lmHQlQ The l operation can be used to express I and V so it can be used to de ne all propositional operations de ned by truth tables This is more amusing than practicall An exe ise is to show that the operation PgQ de ned as P Q can also be used to de ne all other propositional operations 65 Development of algebraic rules We will develop a set of rules for calculation with propositional operations which will enable us to transform any expression written with the proposi tional operations and or and not into DNF then transform it into the form representing its truth table We begin with rules needed to put conjunctions and disjunctions in de sired order and remove duplicate items commutative laws PAQEQAP PVQEQVP associative laws PAQREPQR PVQVREPVQVR idempotent laws PAPEP PVPEP contradiction P J E F Note that this rule also allows elimination of duplicated letters in con junctions 28 identity law PVFEP This law allows contradictions appearing as terms of disjunctions to be ignored zero law PAFEF This law allows conjunctions containing contradictions to be reduced to F l39ow we introduce rules to enable reduction of any expression to DNF de Morgan laws IPQ E IPV IQ PvQE pA Q double negation J E P Repeated use of these rules will cause all negations to be applied to single propositional letters distributivity of conjunction over disjunction PAQVREPQVPR Use of this rule will eliminate all conjunctions with disjunctions as com ponents combined with commutativity of conjunction in order to deal with disjunctions appearing on the left of A It should be clear that enough applications of the last four rules will reduce any expression to DNF The rules above allow us to convert any term in DNF to one in which each conjunction contains at most one occurrence of each letter Occurrences of P or IP twice are eliminated by idempotent laws and occurrences of P and IP together allow the entire conjunction to be reduced to F and then eliminated completely using an identity law unless the whole expression converts to F 29 Further we can put letters in each conjunction in the same order using associative and commutative laws Suppose that we have an expression in letters P Q and R which contains a conjunction which is too short for example P Q We can replace this with the following disjunction of conjunctions containing all the letters PAIQARVPIQIR The same process can be iterated to add more missing letters as needed The equivalence needed to justify this is P E P Q V P Q We can justify this by making the following calculation PEPTEPAQVIQEPQVPIQ Each of the steps in this calculation is justified if we add the following two equivalences another identity law PATEP excluded middle P V IP E T So we have shown that any expression can be converted to an expression in Dl39F coding its truth table Finally we show that any tautology can be reduced to T A tautology has a truth table containing all possible conjunc tions If the three letters P Q and R are used we will for example have P Q R and P Q IR as two disjuncts of the DNF term they can be moved next to each other using associativity and commutati ity of V then we can apply the same result we used to add extra letters to conjuncts above to reduce the disjunction PAQARVPQIR to P Q Similarly every occurrence of R can be eliminated Similarly one letter after the other can be eliminated until just one is left P V IP E T 30 7 Wednesday January 21 I list the axioms of boolean algebra pqqp pqqp pq 7 p QH m pq7 ppp ppp 27 27 1 pH 0 p0p 2712 p11 p00 PQ739P 1P7 pqr p9p7 pqpq pqpq pp If we interpret 0 as F 1 as T p as Ip pq as p q and p q as p V q all the axioms are interpreted as logical equivalences All of the equivalences used in the previous section are found here plus some extras We reviewed the argument of the previous section that boolean algebra allows any expression to be converted into a form which represents its truth table and further allows the truth table of a tautology to be converted to T or 1 We carried out the proof of the tautology P C2 gt R gt P gt C2 gt I m going to give the short proof here p gt q is equivalent to Ip V q or p q Using this we translate PAQ gt R gt P gt C2 gt R to PQ R P Q R l39ow observe that PQ R PQR PQR so the whole expression can be written PQR P Q R l39ow observe that PQR Q R so we can write the whole expression as PQR PQR 1 The proof of the tautology is complete l39otice that our style of reasoning here is that of algebra as we learned it in high school the rules are not quite the same but the way the rules are used is the same Each rule is a universal statement in a rule like p q q p we can replace p and q with any desired expressions and we are allowed to substitute equal subexpressions for one another By way of contrast in natural de 1uction we are not allowed as yet to use logical equivalences to make substitutions for deeply embedded subexpressions though we could v 31 add a rule which allows this all of our rules work on the top levels of expressions 71 Alternative interpretations and duality There are other possible interpretations of boolean algebra of which we give two If we were to allow 1 to mean F and 0 to mean T instead of the reverse it is straightforward to check that pq would now mean qu and pq would mean p q It is interesting to observe that the axioms of boolean algebra remain axioms if addition is interchanged with multiplication and 1 is interchanged with 0 This duality can also be explained using truth tables If T is replaced with F everywhere in the truth table for A we obtain the truth table of V with the lines in a different order similarly the table for transforms to a table for V and the table for I to a different table for I Further if we take two logically L e pie ion and tran f orm them both in this way we still get logically equivalent expressions which suggests that the procedure of interchanging I and V and xing I in ex pressions with no other operators should convert logic equivalences to other logical equivalences as we see in the case of the axioms of boolean algebra in the standard interpretation Another interpretation is in terms of sets addition could be union of sets multiplication could be intersection of sets and negation could be comple ment relative to some xed universe while 0 would be the empty set and 1 would be the universe 8 Friday January 23 Our topic today is another algebraic approach to propositional logic The idea is to use the operations of arithmetic mod 2 to implement the operations 32 of propositional logic The following tables express well known properties of even and odd integers if we let representative elements 0 and 1 stand in for the classes 0 0 0 1 1 0 0 0 1 0 The only unexpected result is 1 1 0 and what this means is an odd number plus an odd number is an even number which is unexceptional The following algebraic rules are inherited from the algebra of the integers HOquot OI AI A myym mywmyz my my ar0ar 3713 myarz There are two additional special rules which clearly hold 2 0 2 In the lecture in class I included m0 as an axiom but in fact m0 y 0 proves this from the axioms given If we interpret 1 as true and 0 as false then multiplication will be inter preted as and addition will be interpreted as EB the exclusive or We now show how to define other logical connectives in terms of this algebraic interpretation 17 1 is easily checked mVy21IarIy 11ar1y 11arymyaryary establishes the definition of V y y my mvy myb y1my1my 1aryyyar1armg 33 establishes the definition gt y 1 3769 atwhyW 1mmy1yym 2 1yyarararyarymaryaryymyyar 2 1ary in the last step the terms cancel in pairs As an example we prove that P C2 gt R is logically equivalent to P gt C2 gt R PAQ gtRPQ gtR1PQPQR P gtQ gtR1PPQ gtR 1PP1QQR1PPPQPQR1PQPQR and this establishes the desired equivalence Just as in the case of boolean algebra there is a dual interpretation of this algebraic system as logic In the dual interpretation 0 represents true 1 represents false addition represents ltgt and multiplication represents V The representation of GB or ltgt by addition mod 2 gives a quick argument that these operations are commutative and associative It also allows us to quickly determine the rather surprising meaning of expressions rather like P1 EB P2 EB 65 P7 which does not mean that exactly one of the Pn s is true or P1 ltgt P2 ltgt Pn vhich does not mean that all the H s are equivalent A sum an 777 of mod 2 integers will be equal to 1 precisely if an odd number of the are odd In the original interpretation this means that P1 EB P2 EB 65 P7 is true just in case an odd number of the H s are true In the dual interpretation we find that P1 ltgt P2 ltgt P is false just in case an odd number of the H s are false so true just in case an even number of the H s are false l39ow we present a proof of the completeness of our algebraic presentation it is obvious that the rules we have given are sound but it remains to be shown that every tautology can be reduced to 1 using our rules 1 llultiplication distributes over both multiplication and addition My z 37W my m 34 2 Case analysis myvmymy1mymyymym justifying the rule C We define where A and a are any expressions and is a variable as the result of substituting a for in A are For any expression A mA 2 aA1 The procedure for showing this is to distribute the factor over every product and sum in the term A so that every variable or occurrence of 0 or 1 is multiplied by Then replace each occurrence of with the logically equivalent m1 then undo the distribution giving arA1 For any expression A A IarA0 This is proved in the same way as the previous equation but one uses the identity m1ar mar0m0 instead of 2 m1 It follows that any expression A satisfies A 2 mA u A 2 We give example calculations ymygt my may m1 myltm1gtltmygt m y 1y illustrates the way that substitutions are proved mymyar1y1yIat0y0y area111ltwgtlt1010meta100gtlt ygtlto000gtgt x91 y Wyl WM WW and the last expression codes the truth table of the original expression in an obvious way If all of the final factors of 0 or 1 in the expression coding the truth table then repeated use of the identity murar1ar1 35 will reduce this expression to 1 which establishes completeness of this system This kind of completeness proof will actually work using boolean algebra as well boolean multiplication distributes over both addition and multipli cation y V is an identity and the proof that 7714 mAll and 0314 works the same way too so this method of simulating truth table reasoning will also work in boolean algebra 9 h40ndayJanuary 265equentcahn usin troduced Today I am introducing yet another and the last system of proof for propo sitional logic that we will consider It is called sequent calculus A sequent is a notation F l A where F and A are finite sets of propo sitions in our usual notation We adopt the convention that a proposition P can stand for the finite set with P as its only element and that a notation like F P will stand for the set F U P sets are just represented as comma separated lists The fact that our lists represent sets allows us to ignore order of items in lists and allows items to be duplicated in lists harmlessly We say that a sequent F l A is valid if any assignment of truth values to propositional letters in the sequent which makes all propositions in the set F true makes some proposition in the set A true A simple example of a valid sequent is P l P More generally any sequent F P l P A in which there is a proposition which appears in both sets is valid if all propositions on the left are true then P is true and P is one of the propositions on the right as well We introduce basic rules for negation and conjunction and use them to derive rules for disjunction and implication FFAA D AFA DAPA Fk AA The negation rules simply cause the negated expression to be moved across the turnstile 36 To see for example that the rst rule is valid suppose that the sequent above the bar is valid so that any assignment of truth values to propositional letters which makes all sentences in F true either makes A true or makes some sentence in A true This implies that any assignment of truth values to propositional letters which makes all sentences in F true and also makes IA true must make some sentence in A true which is the condition of validity of the sequent below the bar DAABFA DABPA FPAA FPBA rkAAaA We present the derivation of an obviously valid sequent PlP R Pk PAIPl W A sequent l P asserts that P is a tautology if every proposition in the empty set is true vacuously true then P is true Similarly a sequent P l asserts that P is contra 1ictory The sequent with which we start is valid because it has P on both sides The sequent is built from the bottom an advantage of the sequent calculus is that the construction of proofs is driven by the form of the statement to be proved this is partially true in natural deduction proofs We now present the derivation of rules for disjunction and implication The derivation F P l A P Q l A F l IP A F I Q A F l IP Q A F I IP Q l A DPVQFA justi es the rule F P l A P Q l A DPVQFA 37 The derivation F l P Q A F P I Q A F IP Q l A F P Q l A 1 l P Q P l P v Q A justi es the rule F l P Q A F l P v Q A it is not acci 1ental l39otice the symmetry between the rules for the dual operations and V The derivation F P I Q A 1 l IP Q A F l P v Q A F l P gt Q A justi es the rule TPlQA r l P gt Q A Set A 0 in this rule and get F P I Q 1 l P gt Q If you read this carefully you will see that this is basically the implication intro 1uction rule of our natural deduction system The derivation F l P A F P l A F Q l A F P v Q l A 1 P gt Q l A 38 justifies the rule rtnA thA DPanA This rule will look quite peculiar understan 1ably We do not usually use P gt Q as a premise all by itself we use it in the context of a rule like modus ponens with an additional hypothesis We demonstrate that modus 90718716 is provable using this rule APAB ABtB AAaBkB The two premises of this deduction are both valid because they have an identical letter on both sides of the turnstile The conclusion is the rule of modus 90716713 The whole deduction is an example of the second rule for implication with T 2 A A 2 B P 2 A and Q 2 B 10 39TuesdayJanuary 26 101 Sequent calculus continued Another way to view sequents is to consider the circumstances under which a sequent is invalid F l A will be invalid if there is an assignment of truth values which will make all sentences in F true and all sentences in A false The strategy of proof in sequent calculus can then be viewed as an attempt to invalidate the sequent we start with We outline this approach First we consider the basic rules We only need to consider the rules for I and A because we know that all other operations can be de ned in terms of these two and also because we know that the rules for the other propositional operations have been derived from these F l A A F IA l A If we aim to make all sentences in F true 2A true and A false this is exactly the same thing as to make all sentences in F true and to make A and all sentences in A false 39 DAPA FFAAA If we aim to make all sentences in F true and to make IA and all sentences in A false this is exactly the same thing as to make all sentences in F and A true and to make all sentences in A false DAABFA DABPA To make all sentences in F and the sentence A B true and make all sentences in A false is exactly the same thing as to make all sentences in F true along with A and B and to make all sentences in A false FPAA FPEA FFAAB To make all sentences in F true and to make A B and all sentences in A false is the same thing as to be able to do one or both of the following either make all sentences in F true and make A and all sentences in A false or make all sentences in A true and make B and all sentences in A false It follows from this consi 1eration of the individual basic rules and similar arguments can be made for each of the rules derived above that if we have a partial proof tree of a sequent we can invalidate that sequent if and only if we can invalidate some sequent at the top of the proof tree This means that if the top of the proof tree contains only axioms sequents of the form F P l P A then the sequent at the base of the proof cannot be invalidated and of course this is what we mean by having a complete proof Further notice that every application of a rule makes the sentences in the sequents simpler if we continued applying the rules long enough all top sequents would consist only of single letters we don t always do this because the sequents may become axioms before they are completely atomized in this way If every top sequent is an axiom we of course have a proof If we have a top sequent which is not an axiom then we can invalidate the sequent at the base by assigning all propositional letters to the left of the turnstile the value true and all propositional letters to the right the value false To be more precise on any branch of the tree going up the structure of the rules guarantees that a logical operation will be eliminated at each step Thus in a number of steps no greater than the number of logical operations 40 in the base sequent of the tree we will arrive at a sequent containing no logical operations just letters Every branch of the tree will be of uniform height bounded by the number of logical operations involved The potential size of the tree grows exponentially with the number of logical operations in the base sequent due to the possibility of branching at each step This is a completeness proof for this system for every tautology P there is a proof of l P in sequent calculus and for every non tautology there is a partial proof tree from which we can extract a counterexample showing that it is not a tautology Examples done in class we did two proofs of P C2 gt R gt P gt C2 gt R and used a proof tree to find a truth assignment showing that the bogus sentence P Q V R gt P R V Q R from the original version of assignment 2 is not a tautology RQPRR RQPQR Pan PAQLR FAQR2P2QlR PAQ gtRPI Q gtR PAQ gtRlP gtQ gtR I PQ gtR gtP gtQ gtR PQRlR Typesetting this so that it doesn t over ow takes some ingenuity I apol ogize if the result is not beautiful The main strategic choice I want to call attention to is the use of the rule for implication on the right instead of the left at the second step counting from the bottom of the tree The second example will show what happens if we use the left rule instead causing the tree to branch at the second level PQlPR PQIQR QlPAQLR PalPAQ7QgtR l PAQMPMQWD PAQgtRl PgtQgtR I PQ gtR gtP gtQ gtR RPQlR RPl Q gtR RI P gtQ gtR I m amazed that this one typeset inside the page l39otice that we still succeed in proving it if we choose to use the branching rule at the second 41 stage but the proof is a little larger Sequent calculus proofs like proofs in any known system of propositional logic can but don t always expand ex ponentially in size with the size of the formula being proved when explosion occurs it occurs because one is forced to use many branching rules rules like the rule for conjunction on the right which have more than one premise Finally we contruct a proof tree for the non tautology P Q V R gt P R V Q R and extract a truth assignment from it which makes this sentence false nor mag PQlRR P Ql P QAR PQI RQR PRlPRQR RQFPAEQAR PQVRlPRVQR PAQVRlPRVQR PAQVR gtPRVQR All the top level sequents in this proof tree are valid except P Q l R R from which we extract the information that if P and Q are true and R is false we can conclude that P Q V R gt P R V Q R is false as it is easy to check 102 Natural deduction rules for quanti ers The quanti ers for all Pat and for some Par or there exists such that Par are assumed to be familiar We will extend our natural deduction system and our sequent calculus with rules for reasoning with quantifiers algebraic reasoning with quantifiers is less common but I will try to put something in the notes about it eventually In this subsection I introduce the natural deduction rules for the universal quantifier V and the existential quantifier El I avoid technicalities about substitution which will enter into a final technically accurate statement of these rules To prove a statement of the form for all Par the standard strategy in a mathematical proof written in English is Let a be an arbitrary object prove Pa This strategy is captured by the universal quantifier intro 1uction rule ui now presented 42 Goal 1 a a hyp for ui must be new it cannot occur in any line which can be copied into the box n Pa n1 universal quanti er intro lines 1 11 The use of equality in the hypothesis line is purely arti cial it has the harmless side effect that is provable using just ui The restric tion on use of the variable a can be enforced in two ways we can either require that a not appear in any line which is usable inside the box it might appear in some other closed box this is our of cial rule The alternative is to restrict copying no line mentioning some other 0 outside the box may be copied into the box The universal quanti er elimination rule ue is very simple Pa If we have for all Par then we certainly have Pa for any particular The existential quanti er intro 1uction rule ei is similarly simple Pa If we have Pa this witnesses For the existential quanti er it is the elimination rule ee which is more complex m n Pa hyp for ee on line m must be new as in the ui rule ni Q Q must not include any occurrence of ni1 Q existential quanti er elimination lines m n nii This rule captures the idea that if we have an existential hypothesis Sarf we can introduce a speci c object a such that Pa Any state ment we can prove using the existential hypothesis which does not mention the named witness is uncon 1itionally proved 43 The use of a box here is optional we could adopt the convention that we can simply introduce a witness to any existential hypothesis and keep it around permanently However we believe that the named witness in this kind of proof is just as much a locally declared object as the arbitrary object in the universal intro 1uction rule s subproof 11 Wednesday January 28 On Wednesday I presented examples of the use of my computer software for sequent calculus I will create a section of notes on this session at some point in any event a manual will be available when we go to the computer lab with this next week 12 Friday January 30 Today we did sequent calculus proofs at the board I noted in class that it would be a good idea to attempt proofs of these tautologies using the other techniques that we have learned An easy one P Q l P P I Q gt P I P gt Q gt P Another easy one A l A I A 1A l IA w l Sticking with easy Pl P 1 151 l Pv IP Verging on trivial 44 A B l A B W A B l A v B l A B gt A v B It s tempting to do the left conjunction and right disjunction rules at the same time This is one direction of the de 1uction of one of dellorgan s laws AFAB BPAB FABmA FABmB PAVBwA kAvB B kAva A B Avmk AA 3 P Avaa AA B Here s the last example we did in class QPQP RQPP 39quot QIP PV Q gtPQp Pvmtm vagQ M g MQ M In this example I use the style of circling the sentences to which rules are applied actually I use boxes since that s What my typesetting program supports but it s not too pretty because I can t gure out how to keep the boxes from sticking to the line above I m sure there is a solution which I will nd eventually I made a remark during class about the application of certain rules which might be helpful In the branching rules FPAA FPBA rkAAaA DPFA DQPA DPVQPA 45 I PIQA FI P gtQA we may think of the procedure as follows In the conjunction rule on the left make two copies of the sequent and replace the conjunction with the first conjunct in one of them and with the second conjunct in the other In the disjunction rule on the left similarly make two copies of the sequent but replace the disjunction with the first disjunct in one of them and with the second disjunct in the other The left implication rule is a little trickier make two copies of the sequent omitting the implication on the left then in one of them add the hypothesis on the right and in the other add the conclusion on the left We discussed writing these up I suggested that a good way to document what rule is being used is to circle the sentence to which the rule is being applied at each step and indicate axioms by linking the identical sentences appearing on both sides of the turnstile I illustrated the circling in one of the examples above 13 Monday February 2 131 Sequent examples We did the following examples in class Proofs will be inserted into the notes Another deMorgan example IPQ gtIPIQ lP Pl V gt V Extract a counterexample from the proof tree of this classic non tautology waoawam 46 Q Pa P Q Q l P P QLQhP W hm FWQMQM From either of the invalid sequents at the top of the proof tree we read off the only counterexample the case when Q is true and P is false I said originally Prove the following tautology a natural deduction proof of this would also be of interest PVQIQVR gtP gtR RIMQR QJ lQJE PvQPI QR PvQRPI R PVQ239Q2P l R PVQLEQVRLPFR PVQIQVRPlR PVQIQVR l P gtR PVQIQVR gt P gtR But in fact this was not a tautology and we extract a counterexample The one invalid sequent at the top of the tree tells us that the only coun terexample is the case where P is true and Q and R are false The intended tautology was pvQMvam m vm and we did prove this together QFQRR neevmrn QWQPRR QRFRR eccvmrna wv mevmrn3 vaLvamkaR PVQA IQVRIPVR I PVQ IQVR gtPVR 132 Understanding a rule of sequent calculus as a dis tributive law in boolean algebra This example is provided as a way to understand what branching rules really are and also as motivation for possible future exercises The sequent P V Q R l S T is valid i quot P V Q R gt S V T is a tautology In boolean algebra notation this is P QR S T Apply de Morgan to get PQRST Further apply deborgan to get PQ R S T l39ow apply distributivity of addition over multiplication to get PRSTQRST and de Morgan again to get PR S TQR S T which in propositional logic is PAR gtSVTQR gtSVT This is a tautology precisely if the conjuncts P R gt S V T and Q R gt S V T are tautologies and this is true precisely if the sequents P R l ST and Q R l S T are valid This presentation is better than what I did in class because it shows that the division of the sequent into two simpler sequents really is the result of a single application of a distributive law There was another irrelevant application of distributivity in my class presentation 48 14 Notes on the cut rule written Monday ln n0tlectured39Tuesday 141 The relationship between the sequent calculus and natural deduction We started this topic at the end of the day lV Ionday These notes are not in final form but you are welcome to look them over We first discuss conversion of natural de 1uction proofs into a notation which looks more like that of sequent calculus A rule like P 7xe with no use of subproofs and more than one premise can be written in a style more like that of natural 1e 1uction 1 Q P Q This is clearly just a notational variation More useful is the conversion of rules involving subproofs For example the rule of implication intro 1uction becomes P I Q P gt C2 The line P I Q says that Q can be proved if P is added as an additional assumption The next step is to convert all lines to sequents This can be done by putting in front of every line of the natural de 1uction proof a turnstile and to the left of the turnstile putting all the assumptions needed for that line to follow these will be any premises of the whole argument plus the hypotheses of any subproofs The rules given above can then be written in a fully sequent form rep FPQ FPPAQ 49 F P I Q P l P gt Q It is easy to see that these rules are valid in the sequent calculus and provable using our rules Additional consi 1eration is required to justify the use of previous lines of a proof in natural 1e 1uction We can copy lines from parts of the proof with fewer assumptions from outside current boxes Fl P FUAlP It s actually easy to see that the following more general rule of weaken ing is valid in sequent calculus F l A F U F2 l A U A2 If it follows from all sentences in F being true that some sentence in A is true it certainly follows from all sentences in F U F2 being true that some sentence in A which will also be in A U A2 will be true We can add stuff to sequents freely on both sides and they stay valid l39otice that this is automatically enforced by our rules because axioms stay axioms and applications of rules stay valid applications of rules if the contexts F and A are enlarged The disjunction intro 1uction rules take the following form in sequent style notation FkaP FkaQ FpPkQ FkaQ These forms are not precisely what we would want both sequent and conclusion cry out for proof using the sequent F l PQ but the natural deduction context does not so far suggest a use for multiple conclusions A convention to the effect that additional conclusions on the right stand in for the negations of these conclusions on the left could be useful but 50 it does mean that a sequent with multiple conclusions has several different meanings depending on which conclusion is to be proved FPPAQ FkP FFPAQ F I Q are clearly valid inferences in sequent calculus They go against the grain from our sequent calculus standpoint because they prove simpler conclusions from more complex hypotheses l39otice that a sequent proof of F l P Q from our rules seems to require the existence of sequent proofs of F l P and F I Q already in existence as prerequisites rk p FkaQ er and Tk Q FkaQ FkP have the same unsatisfactory property from our sequent calculus stand point of having more complex premises than conclusions In the first case the existence of sequent proofs using our rules of the premises seems to require the existence of sequent proofs of F P l and so by weakening of F P I Q and of F l P Q The second case admits of a similar analysis F l P F l P gt Q P I Q has the same unsatisfactory characteristic But notice that a sequent proof using our rules of the two premises seems to require a proof of F l P and so by weakening of F l P Q and a proof of F P I Q A look at the negation intro 1uction rule will give the clearest indication of what we are lacking here DAFPA P Fk A 51 A proof tree on the premise of this reasoning has the following structure r rpk DAPP TEQT DAFPA P Fk A All of the translations of natural deduction reasoning given above would become valid in our system if we adopted the following rule called the cut rule FPRA DPFA FPA In the negation intro 1uction example we could use cut to deduce F A l and then F l IA from the sequents at the top of the proof tree just given This rule is clearly valid But it is certainly incompatible with the phi losophy of our sequent calculus any number of extra logical operations may be intro 1uce 1 in the expression P whose structure is not motivated in any way by the structure of the sequent F l A The actual situation is that the rule is useful for interpreting natural deduction rules sound but not required anything that can be proved with the cut rule can be proved without it and in fact we already know this because we know that every valid sequent can be proved using our sequent rules 15 Tuesday February 3 completeness of nat uraldeduc on In this section I present the proof of completeness of natural deduction The strategy is to interpret sequents as making assertions about the ex istence of natural deduction proofs then show that the new definition of sequent has the same axioms and satisfies the same rules of inference as the original de nition If P is a tautology the meaning of l P under the new interpretation will be there is a natural deduction proof of P We already know that the sequent calculus is complete so if this program works every tautology has a natural deduction proof The new interpretation is this we interpret F l A A as meaning there is a proof of A with premises all the sentences in F and the negations of all the sentences in A This is quite suspect because there is no special way to pick out one element of the right set in a sequent as the conclusion before we can use this definition we need to show that all the different interpretations of F l A A are equivalent We first show the following if F IA l B is valid under the new inter pretation then F B l A is valid under the new interpretation The same is true for the old interpretation and it is also possible though it takes a little more work than you might think to show that if one sequent has a proof using our sequent rules so does the other We can be sure of this though because we actually know that the valid sequents in the old sense are exactly the ones that have proofs since one sequent is valid in the old sense iff the other is valid it is also the case that one has a proof iff the other does F IA l B says There is a natural de 1uction proof of B from the premises in F and A Pictorially we have a proof of the form IA B F B l A says There is a natural deduction proof of A from the premises in F and B We can construct such a proof from the proof above IA hyp for contradiction here we copy the box from the proof above B B IB ci A contradiction by preceding box This result allows us to work only with sequents of the form F l C with exactly one conclusion In case there is more than one conclusion in a sequent we handle the additional ones by negating them and moving them across the turnstile If we want to apply a right rule to one of these negated conclusions we use the rule above to swap it with the of cial conclusion apply the rule then swap it back If there is no conclusion we convert F A l 53 to F A IIA I clearly equivalent by using the double negation elimination rule then to FA l IA So in any case we can restrict ourselves to the case with a unique conclusion which makes life easier for use when thinking about natural deduction Axioms are clearly valid F A l A is valid under our new interpretation since there is certainly a proof of A from premises which include A It might be necessary to convert a sequent of the form I AIA l C to the form F A C l A using the previous result in order to recognize an axiom l39ow we need to check the validity of the rules for the various operations All rules are presented with their conclusions having single conclusions F l A C F IA l C These sequents are equivalent by the convention indicated above so the left negation rule is already taken care of by our treatment of multiple con clusions DAI Fk A The premise F A l is equivalent to F A l IA by the discussion above This sserts the existence of a proof like this A IA This can be converted to a proof of IA from F as follows A V IA exc mid A here we copy the box from the proof above IA A gt A ii IA IA copy previous line IA gt A ii IA proof by cases DABFC DAABPC The premise asserts the existence of a proof A B C in which we suppose that there are no lines between the hypothesis A of the outer box and the box with hypothesis B any such lines could be moved inside the box with hypothesis B and repro 1uced after that box if needed outside the box and from which we construct F A B A ce B ce here copy lines between B and C from the proof above which is What the conclusion requires Fl A Fl B TlAAB The premises of this rule tell us that we have proofs A l and B l r gtm these we easily get a proof 39Tl copy first proof A copy second proof B A B by ci which is What the bottom line asks for DPFC DQPC anQkC If we have proofs th n we have a proof F pvQ C P gt C ii Q c i C2 gt C iris C proof by ases with the boxes from the two given proofs as subproofs which meets the requirements of the bottom line ran FkaQ The top line may be interpreted as either F J I Q or T Q l P so we are given either a proof p Q l or a proof T g P and from either of these we get the conclusion P V Q from the premises F by the rule of disjunction intro 1uction I P I Q P l P gt C2 By the premise we have a proof F P Q given which we can immediately draw the conclusion P gt Q from the premises F by implication intro 1uction FI PC 1 ch I P gtQlC As always this is the most exciting of our rules The first premise needs to be read F P l C by our convention for handling multiple conclusions So we are given proofs from which we construct a proof 0 I F P V IP exc mid P gt Q P Q by mp here we copy one of the boxes from above P gt C ii IP here we copy one of the boxes from above J gt C ii C proof by cases which meets the requirements of the bottom line of the rule The techniques described in this proof can be used to convert a sequent proof of a tautology to a natural de 1uction proof of a tautology It will not be an especially short or natural natural de 1uction proof though Since we know that every tautology has a sequent proof we know that every tautology has a natural de 1uction proof I I think it would be a nasty exercise to actually convert a sequent proof of any size to a natural de 1uction proof in exactly this way but I may try it in my of ce not at the board and put the result in the notes or present it in class if it turns out not to be too bad l39otice the suspiciously prominent role of proof by cases in the proofs produced by this construction Of course proofs by truth table are the ultimate example of proof by every single case to the point of exhaustion 16 Wednesday February 4 I lectured in three areas 161 Deriving rules for new logical Operations I derived the left rule for GB exclusive or and both rules for the neither nor operator l The derivation DPFQA DQPRA DR QFA n thA DWA QPA DbPAQkA DWA QVfWAQFA DPQFA justi es the rule FPlQA FQlPA DPQFA The derivation of the other rule for GB is left as an exercise as is the derivation of rules for the biconditional The rules for l are more interesting in a way because they could in theory be used as the only rules of our system since all propositional logic operations can be de ned in terms of l Of course here our derivation uses the de nition P l Q E P v Q The derivation F l P Q A F l P v Q A I IP v Q l A F P l Q l A justi es the left rule F l P Q A F P l Q l A The derivation F P l A P Q l A DPVQFA F l P v Q A F l P l Q A justi es the right rule F P l A P Q l A 1 l P l Q A These rules combine characteristics of the rules of the connectives V and on the one hand and the rule for I on the other as one might expect 162 Translating natural deduction proofs into sequent proofs the need for the cut rule I talked about translation in the other direction certain natural deduction rules when expressed in sequent form seem to require the cut rule in addition to our official sequent rules The rules which I consi 1ered were modus ponens and negation intro 1uction the derivations are given above in the Monday notes not lectured on Tuesday but I will insert them here As we saw in the completeness proof for natural deduction certain rules of natural deduction correspond precisely to rules of sequent calculus This is true for implication intro 1uction and disjunction intro 1uction for example The formalizations of the simple disjunction elimination rules in sequent notation FPPAQ rep F l P Q P I Q are clearly valid inferences in sequent calculus They go against the grain from our sequent calculus standpoint because they prove simpler conclusions from more complex hypotheses l39otice that a sequent proof of F l P Q from our rules seems to require the existence of sequent proofs of F l P and F I Q already in existence as prerequisites The sequent formulations of the full disjunction elimination rules F l J F l P v Q P I Q and rt Q FkaQ rep have the same unsatisfactory property from our sequent calculus stand point of having more complex premises than conclusions 60 In the first case the existence of sequent proofs using our rules of the premises seems to require the existence of sequent proofs of F P l and so by weakening of F P I Q and of F l P Q The second case admits of a similar analysis The formalization of the rule of modus ponens FbP FkPaQ er has the same unsatisfactory characteristic But notice that a sequent proof using our rules of the two premises seems to require a proof of F l P and so by weakening of F l P Q and a proof of F P I Q A look at the negation intro 1uction rule will give the clearest indication of what we are lacking here DAFPA P Fk A A proof tree on the premise of this reasoning has the following structure r rpk DAPP TEQT DAFPA P Fk A All of the translations of natural de 1uction reasoning given above would become valid in our system if we adopted the following rule called the cut rule FPRA DPFA FPA It is easier to understand the cut rule if we note that F l P A is valid if and only if F IP I A is valid If we can deduce something in A from F and either P or P then it certainly follows that if everything in F is true something in A is true In the negation intro 1uction example we could use cut to deduce F A l and then F l IA from the sequents at the top of the proof tree just given This rule is clearly valid But it is certainly incompatible with the phi losophy of our sequent calculus any number of extra logical operations may 61 be intro 1uce 1 in the expression P whose structure is not motivated in any way by the structure of the sequent F l A The actual situation is that the rule is useful for interpreting natural deduction rules sound but not required anything that can be proved with the cut rule can be proved without it and in fact we already know this because we know that every valid sequent can be proved using our sequent rules It is possible to transform sequent proofs using cut mechanically into sequent proofs not using cut this is technically quite interesting but beyond the level of this course 163 Quanti ers reintroduced We now of cially finish our discussion of propositional logic and commence the discussion of what is called first order logic or predicate logic in which we add quantifiers Our language changes So far we have only allowed letters as logically atomic sentences We now allow sentences of more complex forms such as Pa the object has property P Rary or H y stands in the relation R to y or even or Tux relations among three or more objects A notation like Pa stands for an atomic sentence We use the notation to represent an arbitrary complex sentence with occurrences of For example if is defined as Ra gt Sat then means Ra gt Sa This admits baroque variations Ra gt 30 also can be written where is defined as Ra gt Sa With these definitions and are the same but Pb and Qb are different the first will be H gt S while the second will be H gt Sa The notation for complex sentences extends to more arguments a sentence Pr y stands for a complex sentence involving and Q The following discussion of the quantifier rules will differ from the discus sion earlier in using the notation instead of Pa The universal quantifier elimination rule ue is very simple If we have for all Pr then we certainly have for any particular The existential quantifier intro 1uction rule ei is similarly simple 62 If we have PM this witnesses Recall from our development in propositional logic that elimination rules tell us how to use premises of a given logical form while intro 1uction rules tell us how to prove conclusions of a given logical form The other two rules are more complicated and involve boxed subproofs To prove a statement of the form for all PW the standard strategy in a mathematical proof written in English is Let a be an arbitrary object prove PM This strategy is captured by the universal quanti er intro 1uction rule ui now presented Goal 1 a a hyp for ui must be new it cannot occur in any line which can be copied into the box Goal n n1 Vazl universal quanti er intro lines 1 11 The use of equality in the hypothesis line is purely arti cial it has the harmless side effect that is provable using just ui We will introduce of cial rules for equality later The restriction on use of the variable a can be enforced in two ways we can either require that a not appear in any line which is usable inside the box it might appear in some other closed box this is our of cial rule The alternative is to restrict copying no line mentioning some other 0 outside the box may be copied into the box We digress to consider the justi cation of a form of reasoning about uni versal statements which is actually more typical Most universal reasoning in mathematics is really not of completely unrestricted generality More often we want to prove something about all objects of a certain sort say natural numbers Our goal is to prove E N The usual strategy is Let a be an arbitrary natural number Prove PM The formal proof in our system would look like this Goal E 63 Goal rewritten using the de nition of restricted quanti ers E N gt 1 a a hyp for ui must be new it cannot occur in any line which can be copied into the box Goal 0 E N gt 2 a E N hyp for ii Goal n n1 a E N gt ii lines 2 n n2 E N gt universal quanti er intro lines 1 n1 n3 E N de nition of restricted quanti er line n2 We can see that our system captures the standard style of reasoning about restricted quanti ers We could but do not of cially introduce a separate rule for a restricted universal quanti er Goal E 1 a E A hyp for restricted universal quanti er intro must be new it cannot occur in any line which can be copied into the box Goal n n1 E restricted universal quanti er intro lines 1 n For the existential quanti er it is the elimination rule ee which is more complex m n hyp for ee on line In must be new as in the ui rule ni Q Q must not include any occurrence of ni1 Q existential quanti er elimination lines m n nii This rule captures the idea that if we have an existential hypothesis we can introduce a speci c object a such that Any state ment we can prove using the existential hypothesis which does not mention the named witness is uncon 1itionally proved 64 The use of a box here is optional we could adopt the convention that we can simply introduce a witness to any existential hypothesis and keep it around permanently However we believe that the named witness in this kind of proof is just as much a locally declared object as the arbitrary object in the universal intro 1uction rule s subproof A reason for the box which is connected to the actual practice in writing mathematical proofs is that we may want the use of a letter to represent a witness to be temporary we may not want to permanently reserve a name for the witness and keeping it in a box allows us to forget the name once we have proved the results we want using it and notice that the results we want to prove will naturally not mention the temporarily named witness 164 Sequent rules for quanti ers F l Pa A T l where 0 cannot appear in F A or F PU l A T l A There are no restrictions on t here l39otice that we don t eliminate the universally quanti ed sentence it might be necessary to use more examples F l Pt A T l There are no restrictions on t here l39otice that we don t eliminate the existentially quanti ed sentence it might be necessary to use more witnesses 13mg A T l A where 0 cannot appear in F or A 17 February 6 2004 This was our rst lab session See the Lab Handout I may add some remarks at this point later 18 February 9 2004 Today we looked at our rst examples of natural de 1uction proofs in rst order logic otherwise known as predicate logic the two terms are inter changeable We proved that a relation R is re exive if it is symmetric transitive and has the property that everything has the relation R to something That is from premises 1 VarVymRy gt 2 sz gt 3 R we can prove the conclusion We regard the premises listed above as lines 1 3 of our proof We then write Goal R The form of this goal suggests that we should open a box for universal quanti er intro 1uction 66 4 a 2 a 11yp 1 01 111 5 31yaRy 110 11110 3 x a 6 11R 11yp 101 00 11110 5 G0211 b R a 10 b0 p10v011 11s111g sy1n1n011y 211111 11110 6 7 VyuRy gt yRa 110 11110 1 xa 8 11R gt 11211110 11110 7 yb 9 MM 11111 111108 68 G0211 aRa 10 b0 p10v011 by t121111t1y1tyz 11R 211111 b R 0 01112111 0 R a 10 a R JR a 01 111108 69 11 VyV aRy sz gt 110 11110 2 xa 12 Rb JR 2 gt 0 Hz 110 1111011 yb 13 11R bRa gt 01211110 1111012 za 14 1130 1111 111108 10 13 15 01211 00 11110 5 6 14 16 111 111108 4 15 0111 110xt 0x211np10 18 111010 101np10x F101n p101n1s0 Ry 3mVyAy V Ry Ry gt 110111100 1110 0011011181011 I11f011n2111y 0110050 2111 211b1t1211y 13111101 A 01 Am 12150 1 Am F01 01110 y Ry by p101n1s0 1 1V1gtW b012111s0 Am 211111 Ry W0 1121V0 y Hat by p101n1s0 3 101np101111g 1110 p100f 01 1111s 12150 12150 2 Am L01 1 W11110s 1110 1111111 01 p101n1s0 2 10 1 01 2111 y Abe H y T111115 A V b Rfli 211111 W0 k110W 111211 1110 11181 21110111211110 1008 1101 110111 80 W0 1121V0 me T1118 101np10108 1110 p100f 01 1111s 12150 19 Tuesday February 10 We went to the lab today there are no additional notes at least not at this time We will spend some time in class tomorrow talking about the test but I do intend to lecture The homework is of cially due tomorrow but I m willing to take it after the test The test is on propositional logic only no quantifiers 20 Wednesday February 11 We completed a formal proof in natural de 1uction of the example informally intro 1uce 1 at the end of the Monday lecture The proof has the interesting feature that it makes use of all four quantifier rules We construct the proof following the structure of the proof sketch given at the end of the Monday notes 1 Ry 2 Early914g v By 3 Ry gt y Goal 68 4 a 2 a 11yp for 111 Goal Egg R Strat0gy as 111 t110 proof sk0tc11 prov0 by as0s E1t110r Act or not Au 5 Au V IAa 0xc 11111 for proof by as0s Goal Au gt Snya t110 goal IAa gt Egg R W111 app0ar aft0r t110 proof of t111s goal 6 Au 11yp for 11 7 SyuRy 110 11110 1 21 a 8 MRI 11yp for 00 11110 7 9 MRI Act 01 11110s 68 10 VyaRy AC1 gt yRa 110 11110 3 x a 11 aRbAAa gt bRa110 1111010 yb 12 130 1np 11110s 911 13 Snya 01 11110 12 14 3yyRa 00 11110 7 11110s 8 13 15 Au gt Snya 11 11110s 6 14 Goal s0o11d as0 IAa gt 3yyRa 16 IAa 11yp for 11 17 VyAy V bRy 11yp for 00 11110 2 xb 18 Act V bRy 110 11110 17 y b 19 bRy 10 11110s 16 18 20 Snya 01 11110 19 b y 21 31yyRa 00 11110s 2 17 20 22 IAa gt 3yyRa 11 16 21 23 Snya proof by as0s 11110s 5 15 22 24 111 11110s 1 23 21 Friday February 13 T111s p0r1od was d0vot0d to t110 first 0xa1n 69 22 Tuesday February 17 de Morgan laws for quanti ers Informally we can think of the universal quanti er as representing a kind of conjunction and the existential quanti er as representing a kind of dis junction if the objects of our universe are a1 a2 then we can think of Vamp as meaning something like and as meaning something like Pa1 V Pa2 V If our universe is nite these expansions are literally correct But if the universe is in nite as is usually the case these expansions are merely suggestive as our formalization usually does not admit the possibility of in nitely long sentences We consider the interaction of negations with quanti ers Using the ex pansion above and recalling the de Morgan laws for propositional logic we suggest the following chain of equivalences expands to quotPa1A A A i i which by de Morgan is equivalent to quotPa1 quotPa2 A V i i i which is the expansion of This is not a proof l In class we did the proofs of the biconditional theorem ltgt which turned out to present various points of dif culty These proofs are here reprdoced for the notes We suggested at the end of class that students work out their own proofs of the other de Morgan law for quanti ers ltgt 70 Here s the formal proof that occupied most of the period Extended com ments are inserted Goal ltgt Goal 1 gt 1 hyp for ii Goal 2 IElarIP2 hyp for proof by contradiction Goal contradiction Goal to take advantage of the nega tive premise 1 3 a a hyp for ui Goal 4 IPa hyp for contradiction 5 ei line 4 ax 6 IElariIP37 ci lines 25 proof by contra 1iction lines 4 6 8 VarPr ui lines 3 7 9 Var ci lines 19 10 contra 1iction lines 2 9 11 gt ii lines 1 10 The proof of Goal 1 is noteworthy because we seem to be stymied at every turn A motto to derive from this experience is that when one is desperate one should resort to proof by contra 1iction in this proof we are repeatedly presented with goals whose form gives us no direct hint how to proceed Another point is that when one has arrived at a contradiction as a goal one should look at negative premises to give new goals whose achievement will allow us to derive a contradiction as we did above when we adopte dthe goal Goal 2 gt 1 hyp fo1 11 Go211 2 hyp fo1 111 3 IPa hyp fo1 00 11110 1 4 110 11110 2 5 Q Q 110g21t1o11 01111111121t1o11 11110s 34 6 Q IQ 00 11110s 2 3 5 7 111 11110s 2 6 8 gt 11 11110s 1 7 This is th0 p1oof W0 did 111 121ss This 1121s th0 W011d f021t1110 th21t W0 1100d to 11s0 110g21tio11 01111111121tio11 21 11110 W0 11st0d 111 th0 i11t1o to 1121t111211 d0d11ctio11 but 112110 110101 h21d to 11s0 to g0t 21 o11t121dictio11 not involving th0 Wit110ss a so W0 c2111 g0t out of th0 0xist011ti211 01111111121tio11 box Th010 is 2111oth01 W21y to do this p1oof Which do0s 11ot 11111 into this p1ob 10m T110 st11d011t Who did th0 p1oof 21t th0 bo211d s11gg0st0d 21t th0 tim0 th21t W0 could go 01th01 With 110g21tio11 i11t1od11ctio11 1st o1 With 0xist011ti211 01111111121tio11 1st 11010 W0 shoW th21t th0 oth01 1o11t0 go0s 1no10 11i01y Go211 2 gt 1 hyp fo1 11 2 IPa hyp fo1 00 11110 1 Go211 W0 Wo111d 11o11n2111y W1it0 this 1ight 21ft01 th0 hyp fo1 11 but 11010 W0 i11t1od110 th0 Wit110ss a to p10mis0 1 1st 3 hyp fo1 111 4 110 11110 3 5 IPa 01 11110s 24 6 111 11110s 3 5 7 00 11110s 1 2 6 8 gt 11 11110s 1 7 This p1oof 1121s th0 s211n0 1011gth 2111d do0s11 t 101111110 th0 W011d 1112111011V01 With 110g21tio11 01111111121tio11 1V0g21t1o11 01111111121tio11 Which 1121s th0 fo11n P i Q 72 was originally listed as one of the basic rules of natural 1e 1uction but we have never actually used it As it turns out it can be derived from the other rules so I have now moved it to the derived rules section where you can see its rather strange proof l This proof justi es the rst two of the following four derived rules and the suggested exercise for tomorrow justi es the other two de Morgan rules for quanti ers 1 2 3 4 23 February 18 2004 Today we proved the exercise from yesterday ltgt and a new result 231 rst proof Goal ltgt Goal 1 gt 1 11ypf0111 Goal 2 a 2 a 11yp for 111 Goal IPa 3 11yp for 111 4 01 11110 3 ax 5 00 111108 14 6 IPa 111 111105 3 5 7 gt 11 111105 1 8 Goal 2 gt 9 11yp fgt111 Goal 10 11yp for 111 11 11yp for 00 11110 10 12 IPa 110 111109 xa 13 Q IQ 110 111108 1112 14 Q IQ 00 111108 10 11 13 15 111 111105 10 14 16 gt 11 111108 9 15 17 ltgt b1 111108 817 This proof 11001s 1110 110ga11011 0111111112111011 trick and 11 021111101 b0 av01d0d 11010 by changing 1110 01101 111 which b01108 2110 0p0110d 111 111108 2 6 00 232 second proof Goal V ltgt V Goal 1 V gt V 1 V 11yp for11 Goal V 2 11yp for 11 3 V 11yp for 00 11110 1 Xa 4 1111q 11110 2 5 IPa 110 11110 4 6 10 111108 35 7 01 11110 6 ax 8 00 111108 13 7 9 V 11 111108 2 8 10 V gt V 111108 1 10 Goal 2 V gt V 11 31771 V 11yp for11 Goal V Goal 1 proof by 021808 gt V 12 11yp for11 13 11yp for 00 11110 12 14 V 811 11110 13 16 V 01 11110 13 ax 16 V 00 111108 12 13 16 17 gt V 11 111108 12 16 Goal 2 proof by 021808 gt V 18 11yp for11 19 11yp for 00 11110 18 20 V 811 11110 19 21 V 01 11110 20 ax 22 V 00 111108 18 19 21 23 gt V 11 111108 18 22 24 February 20 2004 T1118 117218 a lab lay W0 111tro11101 1111prov01n011t8 to 1110 prov0r mo8t1y 111 r0adab1111y and 8tart0d working with q11a1111 0r8 25 February 23 2004 We did a natural de 1uction proof of SHAW gt B gt VarAar gt B We also did a sequent proof of gt 251 rst proof There is a hazard in this proof it is important to read the hypothesis cor rectly as gt B instead of gt B This is one of the reasons it is important to keep track of parentheses Goal gt B gt gt B 1 gt B hyp for ii Goal gt B 2 hyp for ii Gal B 3 gt B hyp for ee line 1 4 ue line 2 5 B mp lines 43 6 B ee lines 13 5 7 gt B ii lines 2 6 8 gt B gt gt B ii 1 7 It is important in this proof that B does not contain any occurrences of This means that it is unchanged in line 3 from line 1 and that it can be exported from the existential elimination box 252 second proof 26 February 24 2004 A second lab day on quanti cation 27 February 27 2004 The example started Tuesday and completed today by Mr Ricker follows gt premise VmVyV Qar y Qy gt Sar premise V premise IRy gt Sar premise E gt ElySy premise Goal ElaElbSa 1 Proof sketch Either there is an such that or not This de nes two cases Case 1 In this case there is a y such that S y y and we are done with y a and y b in the conclusion Case 2 Once again we consider two cases either or IElarIR2 Case 2a Choose an object 6 such that Rc Let d be chosen so that IRd By premise D we have S c d and we are done Case 2b I laIR27 By premise C this implies which by premise A implies c Vyrazmwm Let be any object By there is a y such that Qary by another application of there is 2 such that Qyz and by premise B we have S completing the proof It is important to observe that the structure of our natural de 1uction proof is basically the same as that of the proof sketch but much more explicit We now begin the main body of the formal proof 1 V exc mid Goal gt Sla3lbSa for proof by cases A B C D K K 2 11yp for11 3 3ySyy 1111 11110s 1532 4 S c c 11yp for 00 11110 3 5 31136 1 01 11110 4 6 31a31JSa 01 11110 3 7 31a 303a 00 11110 3 11110s 4 6 09 0 1 gt 3a311Sa 11 11110s 1 7 211 gt 31061130 for proof by as0s 9 11yp for11 Goal 31a3111Sa 10 V I31mIR27 0xc 11111 Goal gt 31a3111Sa for proof by as0s 11 11yp for11 Goal 31061130 12 Rc 11yp for 00 11110 9 13 IRd 11yp for 00 11110 11 14 wide A 0 gt 30 g 110 11110 D 15 RC IRd gt Scd 110 11110 14 16 Rc IRd 1 11110s 1213 17 Scd 1111 11110s 1516 18 3030 1 01 1111017 19 31a31JSa 01 1111018 20 31a31JSa 00 11110s 11 13 19 21 31a31JSa 00 11110s 9 12 20 22 gt 31a31JSa 11 11110s 11 21 T110 box do0s 11ot 10211131 1os0 11010 this is just a page b10a1lt1 Goal IElaIR27 gt Sla3lbSab for proof by cases 23 IElarIR27 l1yp for ii 24 VarIIR27 dmq line 23 Goal taken from the proof sketch 25 a 2 a l1yp for 11i Goal 26 V IRa 11e line C 27 IIRa 11e line 24 28 1e lines 2627 29 11i lines 26 28 30 mp A29 comment notice that the c intro 111ce 1 in the fol lowing line is not a Witness it is a completely arbitrary object 31 32Qc 11e line 30 32 Qc d l1yp for ee line 31 33 SzQM 11e line 30 QM e l1yp for ee line 33 35 QcdQd e ci lines 3234 36 myanew cm gt Sc 11e line B 37 VzQc d QM gt Sc 11e line 36 38 Qc d Qde gt Sc e 11e line 37 39 Sce mp lines 35 38 40 303c 1 ei line 39 41 Sla lbSa ei line 40 42 Sla lbSa ee 3334 41 43 3a lbSa ee 3132 42 44 IElaIR2 gt Sla lbSa ii lines 23 43 45 Sla3lbSa proof by cases lines 10 22 44 46 gt Sla lbSa ii lines 9 45 47 Sla3lbSa proof by cases lines 1846 79 28 March 1 2004 substitution and equality 281 Substitution It is necessary to be careful about the de nition of substitution in the pres ence of dummmy variables such as the in Actually you are already familiar with similar notational issues in calculus Consider the integral t2 dt 37247 132m This might be said to mean the same thing as 1 We would say that it does but that variables are being abused the in the bound means something quite different from the variable of integration This means the same thing as l39ow consider Consider the more complex integral 117 f t2 dt 1 which evaluates to t3 11 lg 39l39 477th If we replace t with here naively we get a genuine mathematical error at 2 f 1 evaluates to 3 which is de nitely different from the previous expression We indicate how we de ne substitution where P is any sentence of our logic and a is a term which is to replace the variable is the result of replacing with a in P The de nition is by recursion on the structure of sentences For an atomic sentence Pan mn we de ne as a when and otherwise then de ne Pan as For a negation IP we de ne as For a conjunction P Q we de ne P as The cases of the other binary propositional operations look just the same So far we have given a fancy de nition of the naive idea replace with a wherever it appears We can t do this with quanti ers and preserve meaning We give an example asserts that every object is equal to a is the only object 11 should be b and indeed this asserts that b is the only object might be thought to be from a naive standpoint but notice that the statement no longer says that is the only object it says that every object is equal to itself We can avoid this problem by renaming the bound variable Vyy is certainly equivalent to and Vyy may be taken to be Vyy which does have the meaning that is the only object Our de nition of substitution into quanti ed expressions errs on the side of caution and always renames the bound variable to a brand new variable whenever a substitution is made WWWy W Pl xllayl where 2 is a variable which does not appear in P or in a can t be 2 not can it be a complex name containing 2 as a component which can happen in applications The substitution of 2 for is carried out before the substitution of a for the variable y Examples l39otice that replacing with a in this expression actually doesn t change its meaning at all this should not be surprising since there isn t really any speci c object named that is talking about 81 l39otice that this does the right thing 1 It s nice to check that it works out sensibly in a nice case too Of course we will not usually change the dummy variable when we don t need to The computer program does because it is easier to do it all the time than to perform the checks required to see if the substitution is dangerous Our quanti er rules could be rewritten to take advantage of more pre cise substitution notation For example universal elimination allows us to deduce from Var here P may be any sentence and may actually include Existential intro 1uction allows us to deduce from P actually it s better to say that it allows us to deduce from y this allows us to talk about the deduction of from a a the expression a a is y while the expression Elf is l39otice that would just be and while we can validly infer from a a by existential intro 1uction it s not the only thing we can infer We will not usually be so precise we will normally stick with our conven tion that stands for an expression containing and replacing with a in this expression will give us 282 Equality In this lecture I intro 1uce 1 sequent rules for equality l a a and a bal lbmla Qlarl Rlbarla Slaml a baplaarlanb Rlamlaslbarl an equation to the left of the turnstile allows substitutions to be made freely in both directions everywhere in the sequent 82 are a suf cient set of rules but I don t like them very much The main reason I don t like them is that they introduce axioms l a a which don t have the uniform form which all axioms of sequent calculus have so far In the notes for Tuesday I will include the current computer proofs for basic properties of equality the prover de nes equality in terms of set theory in a way you can examine there I brie y discuss another way of handling equality which is actually closely related to the way the computer handles it which involves a powerful exten sion of our logic If we allow quanti ers over predicate letters P we can de ne a b as VPJ M ltgt Pb two objects are equal if they have the same properties l39otice that the new quanti ers quantify not only over atomic predicates but over complex predicates any sentence containing however complex The rules for secon 1 or 1er quanti ers are exactly analogous to those for rst order quanti ers I give the rst few steps of a couple of proofs l VPPa ltgt l a a We can see that the top line is a propositional tautology so we leave the rest of the proof for you The letter P1 stands for a new property intro 1uce 1 to handle a universal quantifier on the right a a ltgt b a l b a a b l b a l a b gt b a What I did at the last step working from the bottom up was to instan tiate the universally quanti ed P on the left with the property de ned by z a The top formula will be provable by propositional methods as long as a a is provable and we have indicated how to prove this We aren t really going to do secon 1 or 1er logic it s quite similar to set theory which is more familiar to you and is built into the computer prover 29 March 2 2004 This was another lab day 83 this is the computer proof for reflexivity of equality The prover defines equality as the property of belonging to the same sets E is the membership relation Line 1 Proved 1 Ax1x1 x1 by 2 Line 2 Proved 1 a1 a1 by 3 Line 3 Proved 1 AX2a1 E X2 a1 E X2 by 4 84 Line 4 Proved 1 a1 E a2 a1 E a2 by 5 Line 5 Proved 1 a1 E a2 gt a1 E a2 amp a1 E a2 gt a1 E a2 by 7 6 Line 7 Proved 1 a1 E a2 gt a1 E a2 by 9 Line 9 Proved 1 a1 E a2 1 a1 E a2 Line 6 Proved 1 a1 E a2 gt a1 E a2 by 8 Line 8 Proved 1 a1 E a2 1 a1 E a2 Here is the computer proof of symmetry of equality It gives more of an idea of how the set theory machinery in the prover works The prover does not allow just any set to be constructed Russell s paradox is avoided Line 1 Proved 86 1 Ax1Ax2x1 x2 gt x2 x1 by 2 Line 2 Proved 1 Ax3a1 x3 gt x3 a1 by 3 Line 3 Proved 1 a1 a2 gt a2 a1 by 4 Line 4 Proved 1 a1 a2 1 a2 a1 by 5 Line 5 Proved 1 Ax4a1 E x4 a2 E x4 by 6 Line 6 Proved 1 a1 E x1lx1 a1 a2 E x1lx1 a1 2 Ax4a1 E x4 a2 E x4 1 a2 a1 by 7 Line 7 Proved 1 a1 E x1lx1 a1 gt a2 E x1lx1 a1 amp a2 E x1lx1 a1 gt a1 E x1lx1 a1 2 Ax4a1 E x4 a2 E x4 88 by 8 Line 8 Proved 1 a1 E x1lx1 a1 gt a2 E x1lx1 a1 2 a2 E x1lx1 a1 gt a1 E x1lx1 a1 3 Ax4a1 E x4 a2 E x4 1 a2 a1 by 10 9 Line 10 Proved 1 a2 E X1lx1 a1 2 a2 E x1lx1 a1 gt a1 E x1lx1 a1 3 Ax4a1 E x4 a2 E x4 1 a2 a1 by 19 Line 19 Proved 1 a2 a1 2 a2 E X1lx1 a1 gt a1 E X1lx1 a1 3 AX4a1 E X4 a2 E X4 89 Line 9 1 a2 E 2 Ax4 1 a1 E 2 a2 by 11 Line 11 1 a2 E 2 Ax4 1 a1 2 a2 by 12 Line 12 1 a2 E a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 a1 E x4 a2 E x4 x1lx1 a1 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 E x4 a2 E x4 a1 a1 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 90 a1 E x4 a2 E x4 a1 E x5 a1 E x5 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 a1 E x4 a2 E x4 a3 a1 E a3 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 E x4 a2 E x4 a1 a1 E a3 gt a1 E a3 amp a1 E a3 2 Ax4 1 AXE 2 a2 by 13 Line 13 1 a2 E 2 Ax4 1 a1 E 2 a2 by 14 Line 14 1 a2 E 2 Ax4 1 gt 2 a2 a1 E a3 a1 91 by 16 15 Line 16 Proved 1 a2 E x1lx1 a1 gt a1 E x1lx1 a1 2 Ax4a1 E x4 a2 E x4 E a3 gt a1 E a3 a1 by 18 Line 18 Proved 1 a1 E a3 2 a2 E X1lx1 a1 gt a1 E X1lx1 a1 3 Ax4a1 E x4 a2 E x4 1 a1 E a3 2 a2 a1 Line 15 Proved 1 a2 E X1lx1 a1 gt a1 E X1lx1 a1 2 Ax4a1 E X4 a2 E X4 92 1 a1 E a3 gt a1 E a3 2 a2 a1 by 17 Line 17 Proved 1 a1 E a3 2 a2 E xllxl a1 gt a1 E xllxl a1 3 Ax4a1 E x4 a2 E x4 a3 a1 quot11 30 March 3 2004 301 Equality rules for natural deduction The new rules for equality are as usual an intro 1uction rule and an elimi nation rule Equality intro 1uction eq i is 020 This is actually provable but for arti cial reasons having to do with the use of a a as a dummy sentence about a in the rule of universal quanti er intro 1uction Goal 0 a Goal then use ue 1 a 2 a hyp for u i Goal 0 a 2 a a copy line 1 93 3 2 ii lines 1 2 4 a 2 a ue line 3 The rule of equality elimination can be written or more technically a 2 b The use of substitution notation makes it easier to express the idea that not all occurrences of a need to be replaced by b We prove the symmetry property of equality in natural deduction Goal 2 y gt y 2 1 a 2 a hyp for ui Goal Vyu 2 y gt y 2 2 b 2 b hyp for ui Gal a2b gtb2a 3 a 2 b hyp for ii 4 a 2 0 eq i 5 b 2 0 eq e lines 34 use line 3 to replace the rst occurrence of a in line 4 with b 6 a 2 b gt b 2 0 ii lines 3 5 7 Vyu 2 y gt y 2 ui lines 2 6 8 2 y gt y 2 ui lines 1 7 We suggest proving the transitive property of equality as an exercise A further adventure would be to try to prove the transitive property on the computer 302 Numerical quanti ers We show how to de ne 3Pm which means there is exactly one such that PW we can do this as soon as we have equality 3Par ltgt VyPy gt y 2 94 In words what this says is that there is an such that and moreover any y such that Py is actually equal to This can be done for any natural number For example we de ne meaning there are precisely two such that PW ltgt Py g y gt z V c De ning 3 for all natural numbers n in this way would lead to rather long expressions but there s a more ef cient way to do it De ne as If is de ned de ne Eln1mPar as ElmParElnyl y Ay The expressions de ned in this way will get larger linearly in the size of u If you were really ambitious you could try the following project prove the predicate logic version of 22 4 which is the following theorem 32Pm gt V 303 Completeness of sequent calculus The main result of this section is that every valid sequent of predicate logic is provable For the purposes of this section we extend our system with the cut rule but it is actually true if we don t use the cut rule as well it is harder to prove though This cut elimination result is beyond the scope of this course We use the language of our computer implementation which has an in nite supply of dummy variables and an in nite supply of names for objects The set of all expressions in our language is countably in nite we can place it in one to one correspon 1ence with the natural numbers by listing expressions in order of increasing length with expressions of the same length listed in alphabetical order determined by ASCII order on characters for example Fix such an order and let E be the expression correspon 1ing to the natural number 1 Our strategy is to show that any unprovable sequent is invalid Let F l A bean unprovable sequent we will construct an interpretation of the predicate and relation symbols appearing in the sequent under which all sentences in 95 F are true and all sentences in A are false establishing that the original sequent is invalid We construct a sequence of sequents ouch F l A de ned recursively I l A0 is de ned as F l A Note that this is by hypothesis an unprovable sequent Suppose that F l A has been de ned and is an unprovable sequent We de ne I l as the sequent F F l A unless this is provable in which case we de ne it as F l FA if both sequents wer provable we could prove F l A using the cut rule TH l A1 is de ned as I l A except in two special cases if F and I l FF l A then T l A1 is de ned as F F PM I A where a is the rst name that does not appear in I l If F and I l F I F A then we de ne F l A1 as F I F Paj A where a is once again the rst name that does not appear in I l T he sequent F l A1 will be unprovable even with the addition of the Paj s since if it were provable with them added it would also be provable without them since they can be intro 1uce 1 by applying the rule for the existential on the left or universal on the right to F So we succeed in constructing a sequence of unprovable sequents F l A De ne FCC as the union of all the sets F and ACC as the union of all the sets Since all sentences are included in the list of F s every sentence appears in either FCC or Ax If any sentence appeared in both lists the sequents F l A would be axioms for all large enough i We claim that the sentences in FCC can be understood to be the true sentences of a model and the sentences in ACC can be understood to be the false sentences of a model The elements of the model will be the names An atomic sentence Pa1 will be said to be true if Pa1 6 FCC We need to show that propositional operators and quanti ers behave correctly For any formula P 6 FCC IP cannot be in FCC because this would mean that any F l A with large enough index would be of the form I P J l A and so would be provable Similarly for any formula P g FCC and so in Am we must have IP in FCC to avoid having any F l A with large enough index being of the form F l P J A and so provable So negation behaves exactly as we expect the negation of a true statement is false and vice versa 96 For any formulas P and Q we claim that P Q is in FCC if and only if both P and Q are in FCC Suppose P and Q are in FCC if P Q were in Am then any I l A with large enough index would be of the form any I P Q l P Q A and so provable l39ow suppose that P Q is in FCC if either P or Q is in Am we get any I l A with large enough index being of the form I P Q l P A or I P Q I Q Ag and either of these would be provable The arguments for the other propositional connectives are similar more over we have de ned the other connectives in terms of and I and derived the rules for the other connectives from the rules for negation and conjunction in our of cial development of sequent calculus so we are actually safe l39ow we look at the quanti ers We need to show that is in FCC if and only if every is in FCC to show that has the correct meaning Suppose that VarP is in FCC and there is some in Ax then every T l A with large enough index will be of the form I l Pa1 A and this would be provable which is impossible If is not in FCC it must be in Am and when it was put into Ax some Paj was put there by the construction So the universal quanti er works correctly We need to show that is in FCC if and only if some is in FCC Suppose is in FCC the construction tells us that some Paj was put into FCC Suppose that is not in FCC and nonetheless some is in FCC every I l A with large enough index will be of the form I l A which is provable which is impossible It follows that the meaning of the existential quanti er is correct This completes the proof that any unprovable sequent is invalid so any valid sequent is provable predicate logic equivalently rst order logic is complete We summarize some further results machines can nd proofs A computer program can be written which will nd a proof of any sequent given to it which has a proof in theory because in general it will be extremely slow so slow as to be useless Programs can be written which are fairly good at nding proofs of some kinds of sequents machines cannot decide provability Acomputer program cannot be writ ten which decides whether a sequent is provable or not Any program of 97 this kind will say Yes to all sequents with proofs it can be programmed to find the proof eventually No to some sequents without proofs and end up looking for proofs forever for some unprovable sequents any rst order theory has a countably in nite model Notice that the model we constructed here is countably infinite it is made up of names This is odd because we can formalize a set theory in which we can prove that the set of real numbers is uncountable inside first order logic this means that this theory has a countable model The solution to the apparent paradox is that the reals in the countable model are not all the reals Outside the model we can see that the reals of the model can be indexed by natural numbers inside the model this indexing is not found among the functions of the model in nite theories are no problem If we have an infinite collection of premises with the property that no finite subcollection of the premises leads to contradiction we can adapt the proof given here to build a model in which all of the premises in the infinite collection are true The way to do this is to add a condition to the construction to put F on the right if it is a premise from the infinite collection This also leads to curious results The collection of premises consisting of the axioms of the natural numbers and the extra premises t gt 1 t gt 2 t gt 3 and so on through every natural number has these properties so we can build a model of the theory of the natural numbers which contains an object t which is larger than each of the real natural numbers equality can be added All the results we have stated also hold for predi cate logic with equality we have avoided the technical details of show ing that this is true 31 March 5 2004 Arithmetic Made Dif cult We move into the transition from logic to discrete math by considering the simplest discrete math structure the set of natural numbers with rigorous attention to the logical structure of our reasoning For the first time we allow terms names for objects more complicated than variables 98 We introduce a new term 0 For any term we allow ar as a term this is read the successor of a and means the same thing as 1 we will prove this once we have de ned For any terms and y we allow y and y as terms The in y can be omitted unless and y are both strings of digits We de ne 1 as 0 We de ne 2 as 1 We de ne 3 as 2 We de ne 4 as 3 We de ne 5 as 4 We de ne 6 as 5 We de ne 7 as 6 We de ne 8 as 7 We de ne 9 as 8 We de ne 10 as 9 The symbols 0123456789 are called digits For any string of digits D and digit d we de ne Dd as 10 D d This precisely de nes the usual decimal notation for natural numbers and also explains our convention for allowing omission of We de ne 2 y as 17 2 y Successor has the highest prece 1ence followed by multiplication followed by addition In the axioms I use everywhere though all the occurrences in the axioms can actually be omitted The axioms of Peano arithmetic are axiom 1 2 0 axiom 2 VarVyar 2 y gt 2 axiom 3 0 2 axiom 4 VmVyar y 2 a y axiom 5 Varm 0 2 0 axiom 6 y 2 y Peano arithmetic has a single additional rule used for proving universally quanti ed sentences It is the familiar rule of mathematical induction which can be presented without boxes in the form P0 VkPk gt Pk V71P7l or with boxes in the form Goal Warm Goal basis step P0 99 m P0 m1 Pk induction hypothesis 1 must be a new vari able not appearing in any line we are allowed to copy into this box n POW n1 induction lines m m1 n You may use either form of the rule in your proofs You also may use k 1 instead of k as is justified by the following theorem Theorem 1 2 1 a 2 a hyp for ui Goal 0 1 2 a 2 a0 2 a0 n1ue 4 mue means multiple universal elimination this would expand out into two applications of ue 3 a 1 2 0 de nition of 1 line 2 4 a 0 2 a ue 3 5 a 1 2 0 eq e or substitution lines 43 6 1 2 ui lines 1 5 The axioms may be regarded as lines accessible in every proof the style of reference shown here is adequate You will have the list of axioms and of cial definitions available at a test We now do our first induction proof which is a very strange one Theorem Every number other than 0 has a pre 1ecessor 2 0 gt 399 97 Goal basis step 0 2 0 gt Slyy 2 0 Comment This is vacuously true because the hypothesis is absurd The use of negation elimination in the proof is a standard way to deal with this 1 0 2 0 hyp for ui 2 20 2 0 de nition of 2 line 1 3 0 2 0 eq i 4 Elyy 2 0 neg elim lines 23 5 0 2 0 gt Slyy 2 0 ii lines 1 4 Goal induction step 2 0 gt Slyy 2 gt k 2 0 gt Slyy 2 k Comment this is also vacuously true because the conclusion Slyy 2 k 100 is true for reasons that have nothing to do with the hypotheses 6 a 2 a hyp for ui Goal 2 0 gt Elyy 2 gt a 2 0 gt Elyy 2 7 2 0 gt Elyy 2 hyp for 11 Goal a 2 0 gt Elyy 2 8 a 2 0 hyp for 11 Goal Elyy 2 a 9 a 2 0 eq 1 10 Elyy 2 a ei line 9 it isn t neces sary to replace every 0 with y 11 a 2 0 gt Slyy 2 11 lines 8 10 12 2 0 gt Elyy 2 gt a 2 0 gt Slyy 2 11 lines 7 11 13 2 0 gt Elyy 2 gt k 2 0 gt Slyy 2 ui lines 6 12 14 2 0 gt Elyy 2 induction lines 5 13 I suggest attempting two theorems 2 2 2 4 for un 1erstanding the axioms and Vm0m 2 0 an induction proof If you prove Vm0 2 ar 0 you are ready to try y 2 y the commutative property of addition It is important to note that our formulation of the axioms assumes that everything in the universe is a natural number If we were also talking about other kinds of objects we would need to restrict the quantifiers in our axioms to natural numbers 32 Monday March 8 2004 commutativity of addition Today we proved the theorem WWW y y 07 in class unfortunately the proof I gave was wrong I think I must have been asleep on my feet The main induction step needs something additional We adopted the derived rule symmetry of equality 101 a b b a This is justified by instantiating the theorem y gt y and modus ponens There are so many symmetry of equality lines in the proofs below that I think I will allow a line a b to be used either to substitute a for b or to substitute 1 for a in another line This is an example of the strategy to pursue in arithmetic basically we have one additional proof tool induction for proving universal sentences plus a few computational facts expressed in the axioms Using induction breaks the theorem down into two goals Basis 1 V90 y y 0 and Induction Step 1 VkVyk y y k gt V915 y y k We prove the basis first and prove the induction step below The reason for the number 1 will become evident shortly Goal Basis 1 Vy0 y y 0 This is also to be proved by induction We have no way to deal with addition of anything on the left in the axioms so there is no other possible approach Goal Basis 2 0 0 0 0 1 0 0 0 0 equality introduction Goal Induction Step 2 Vk k k 0 gt 0 k k 0 102 G 2 020 hyp for ui al 0aa0 gt0a a 0 3 0aa0 hyp for ii Goal 0 a a 0 Calculation Sketch 0 a ax 4 0 a ind hypa 0 ax 3 a 0 4 0 a 0 a mue 4 45 0 a 0 subst into 4 using 3 this corrects an error I found in the notes on the 9th I left out the use of ind hyp a 0 a ue ax 3 0 a 0 eq e or subst lines 545 0 0 a ue 3 a a 0 symmetry of equality line 7 0 a a 0 subst 86 00512239 9 10 0aa0 gt0a a 0ii lines4 9 11 Vk k k 0 gt 0 k k 0 ui lines 2 10 12 V90 y 2 y 0 induction 111 Goal Induction Step 1 VkVyk y y k gt Vyk y y k The proof I gave for Induction Step 1 in class was wrong I give the correct proof here and point out the needed extra ingredient 13 a 2 a hyp for ii Goal Vyu y y gt Vyu y y a 14 Vyu y y Goal Vyu y y a 15 b b hyp for ui Goal 0 b 2 1 0 Calculation Sketch b a ax 4 b a ind hyp a b 2 why not ax 4 exactly a b Comment to get a proof along these lines we need the result y 2 ar y Unfortunately this missing step requires a full induction proof We close up this proof for the moment and prove this theorem This is a separate proof so it has its own line numbers when we start up again with 103 the other proof we will resume its numbering scheme 104 I m setting this proof up using the box form of the induction rule Goal y 2 37 y 1 a2a hyp for ui Goal y 2 a y Goal basis 0 2 a 0 a0 2 a ue 3 a 0 2 a ue ax 3 a 2 a 0 symm 2 line 3 a 2 a 0 symm 2 line 2 a 0 2 a 0 subst lines 54 7 k 2 a k induction hypothesis Goal k 2 a k Calculation sketch 0 k 2 ax 4 a k 2 ind hyp k 2 ax 4 and substitution a k 8 a k 2 a k mue 4 9 a k 2 k symm 2 line 7 10 a k 2 k subst 98 11 a k 2 k mue ax 4 12 k 2 a k symm 2 line 11 13 a k 2 k subst 1210 14 k 2 a k symm 2 line 13 999 15 y 2 a y induction box form line 6 lines 8 14 16 y 2 37 y We refer to the theorem just proved as Lemma 1 We now resume the proof of the main theorem repeating from the be ginning of Induction Step 1 Goal Induction Step 1 VkVyk y 2 y k gt Vyk y 2 y k The proof I gave for Induction Step 1 in class was wrong I give the correct proof here and point out the needed extra ingredient 105 13 a 2 a 11yp 13901 11 G0a1 Vyu y 2 y gt Vyu y 2 y a 14 Vyu y y G0a1 Vyu y 2 y a 15 b 2 b 11yp 13901 111 G0a1 a b 2 1 0 Ca10111a11011 31101011 I a 2 ax 4 b a 2 11111 11yp b 2 L0mma 1 a b 16 1 0 2 b a m110 4 17 a b 2 b a 110 11110 14 18 10 2 11 symm011y 0f 01111a111y 11110 19 1 0 2 b subst 111108 1816 20 b 2 a b m110 L0mma 1 21 1 0 2 a b subst 20 19 22 a b 2 b a symm 2 11110 21 23 Vyu y 2 y a 111 111108 15 22 24 Vyu y 2 y gt Vyu y 2 y a 11 111108 14 23 25 VkVyk y 2 y k gt Vyk y 2 y k 111 111101 13 24 26 y 2 y 1111111011011 11110 12 25 S11gg01011 0x01018015 My 10 p10v0 y 2 y 1111111011011 011 y 01 2 m1g111 b0 b01101 111a11 1111111011011 011 111011g11 I 11111111 a11y W111 W01k Y011 m1g111 110011 L0mma 1 W0 0a11 110 1111111011011 011 y b00a11s0 y 2 y 1s 011111va10111 10 2 Y011 m1g111 11y p10v111g VarVyPar 1gt VyVarPar w111011 j11s11 0 1111s ma11011v01 T1y 2 33 March 9 2004 T011ay W0 10 11111 1110 p100f 0139 1110 ma111 1111111011011 8101 0139 1110 p100f 0f 00m m111a11v11y 0f a1111111011 11101111fy111g a1111 0011001111g my 01101 0139 y010111ay I a1111011110011 11111010111 s1y10 101111110m0111s 101 1180 0139 01111a111y 111108 than I 11111 y010111ayz 1110 11110 0139 equality elimination 01 substitution may b0 118011 106 in either of the forms I b a PM 1 b This minimizes the need for explicit applications of symmetry of equality But I do require that appeals to substitution be of the form substitution into line In using line n vhere line In is P and line 11 is a b or b a The new version of the proof will conform to these style requirements so it will have fewer explicit applications of symmetry of equality and it will also use the box version of the induction rule rather than the line version which will reduce the number of boxes created I prove Lemma 1 rst Goal y 2 37 y 1 a2a hyp for ui Goal y 2 a y Goal basis 0 2 a 0 2 a 0 2 a ue 3 3 a 0 2 a ue ax 3 4 a 0 2 0 subst into 3 using 2 5 0 2 a 0 symm 2 line 4 6 k 2 a k induction hypothesis Goal k 2 a k Calculation sketch 0 k 2 ax 4 a k 2 ind hyp k 2 ax 4 and substitution a k 7 a k 2 a k mue 4 8 a k 2 k subst into 7 using 6 9 a k 2 k mue ax 4 10 a k 2 k subst into 8 using 9 11 k 2 a k symm 2 line 10 12 y 2 a y induction box form line 5 lines 6 11 13 y 37 y ui lines 1 12 We will refer to this theorem as Lemma 1 and restart the numbering in the main proof which now follows Main Goal VarVyar y 2 y Goal Basis 1 Vy0 y 2 y 0 This is also to be proved by induction We have no way to deal with addition of anything on the left in the axioms so there is no other possible approach Goal Basis 2 0 0 2 0 0 1 0 0 2 0 0 equality intro 1uction 108 2 0 a a 0 inductive hypothesis Goal 0 a a 0 Calculation Sketch 0 a 4 0 a ind hypa 0 ax 3 twice a 0 0 a 0 a mue ax 4 0 a 0 subst into 3 using 2 a 0 a ue 3 0 a a subst into 4 using 5 a 0 a ue 3 0 a a 0 subst into 6 using 7 90513999 CO V90 y y 0 induction box form line 1 lines 2 8 10 Vyu y y induction hypothesis Goal Vyu y y a 11 b b hyp for ui Goal 0 b b 0 Calculation Sketch b a ax 4 b a ind hyp b 2 Lemma 1 a b b a b a mue ax 4 13 a b b a ue line 10 14 b a b subst into 12 using 13 15 b a b mue Lemma 1 16 b a a b subst into 14 using 15 17 a b b a symm 2 line 16 18 Vya y y a ui lines 11 17 5 19 y y induction box form line 9 lines 10 18 c that our new conventions make the proof signi cantly shorter and I think easier to read Tell me what you think Also I found an error in the proof of the basis step in the March 8 notes a step was left out this is corrected here and in the March 8 notes Please tell me if you notice any errors in the notes by the way extra credit points will be added to your homework average for proofreading contributions Just for fun I include the calculation justifying 2 2 4 that we did in class 22 definition of 2 109 21 axiom 6 2 1 2 2 de nition of 2 2 gt1 1 1 axiom 4 2 1 1 2 de nition of 1 2 gt1 1 0 axiom 4 2 1 0 axiom 3 2 1 2 de nition of 1 2 0 axiom 6 2 gt1 0 2 axiom 3 0 2 commutativity of addition this is a onsi 1erable shortcut 2 0 axiom 3 110 de nition of 3 3 de nition of 4 Isn t that nice For further work I suggest associativity of addition andor distributiv ity of addition over multiplication There s no need to change the order of quanti ers to do induction over different quanti ers just use the universal intro 1uction rule on the outer quanti ers and use induction on the vari able you want when you get to it I think that induction on any variable will work with associativity of addition but a is probably best I haven t thought about the other theorem yet 34 March 10 2004 The class produced a complete proof of the associative law of addition Goal VarVyV y y We will prove this by induction on 111 1 a 2 a hyp for ui Goal y y 3 4 5 6 7 2 b 2 b hyp for ui Goal b b Now we use induction Goal basis step a b 0 b 0 ab0 ab0 eq i 1 0 b ue ax 3 a b 0 a b subst into 3 using 4 ctHI 0 2 n1 ue ax 3 a b 0 b 0 subst into 5 using 6 8 a b k b k ind hyp Goal 0 b k b k Calculation sketch abk 4a b k ax 4 b k ind hypa b k ax 4a b k 9 a b k a b k eqi 10 1 k b k mue 6 11 a b k a b k subst into 9 using 10 12 a b k b k mue ax 6 13 wk 11k b k s11bst into line 12 using line 8 ind hyp 14 b k b k mue ax 6 15 a b k b k subst into 14 using 13 16 Van139 11 2 v b induction 7 8 15 17 y 2 v y ui lines 2 17 18 y y ui lines 1 18 35 Friday March 12 I proved in class today This is used in proving a b b a you also might want to prove Varl 112 Goal We will prove this by induction on This won t be identical to the proof I did in class but in general terms the strategy is the same 113 1 a a hyp for ui Goal 2 1 2 1 hyp for ui Goal 1 12 we prove this by induction Goal 10 a0 10 a 10 0 ue ax 5 0 0 0 ue ax 3 a 10 0 0 subst into 3 using 4 a0 0 ue ax 10 0 ue ax a 10 a0 0 subst into 5 using 6 a 10 a0 10 subst into 8 using 7 039 0 99905193955 9b 1k 0k 1k ind hyp Goal 1k ak 1k Calculation sketch a1k ax 6 wk 1ka1 ind hyp ak1ka1 2 many grouping steps 1k1 6 ak 1k l39otice below how many steps it takes to handle the grouping 10 a1k 2 wk 1k wk 1 mue ax 6 11 1k 11 1 subst into 10 using 9b 12 ak1ka1 ak1ka1 mue assoc 13 1k 11 1 subst into 11 using 12 14 ak 1k 11 a mue assoc 15 1k 1k 1 subst into line 13 using line 14 16 11 a a 1k mue comm 17 1k 1 subst into 15 using 16 This is just a page break the boxes are really still open 114 18 bk 2 bk mue assoc 19 bk bk b subst into 17 using 18 20 aka bkb akabkb mue assoc 21 bk bk b subst into line 19 using line 20 22 ak ak a mue ax 6 23 bk 2 bk b mue ax 6 24 bk ak bk b subst into line 21 using line 22 25 bk ak bk subst into line 24 using line 23 26 b be induction 9 9b 25 27 ui 2 26 28 ui 1 17 36 March 15 2004 set theory prerequisites for counting Today I lectured on set theory background which I will assume The notation E y means a is an element of y If E y then y is a set If and y are sets they are the same if they have the same members Axiom of Sethood If E y then y is a set Axiom of Extensionality If and y are sets then 2 y if and only if E ltgt z E These axioms leave open the possibility that there are many objects which are not sets and which will thus have no elements Of course there cannot be more than one set with no elements We introduce some notation b is the empty set the set with no elements If a b are objects there is a set with just a as an element a set b with just a and b as elements and so forth 115 The notation stands for the set of all such that Pr If g exists we have E a E g There are sentences for which there is provably no such set For example if there were a set R then it would follow that R E R ltgt R g R which is a contra 1iction We adopt a more restricted assumption about the existence of sets for any set A and sentence we assume the existence of E A g Axiom of Separation For each sentence and set A there is a set E A g such that E E A g ltgt a E A As well as restricted sets we also de ne restricted quanti ers E APr is de ned as E A gt and E is de ned as E A A consequence of the axiom of separation is that there is no universal set For any set A E A g is a set by the axiom of separation call it RA RA E RA ltgt RA E A RA RA the only way for this to be true is for RA E A to be false So for any set A we can construct a set which does not belong to it there is no universal set The rest of our axioms provide us with some sets to use in the role of A in Separation Axiom of Pairs b a V 1 exists for any objects a and De nition A Q B A is a subset of B i E A gt E B l39otice that A Q A and 0 Q A are always true Axiom of Power Set For any set A the set PA Q A exists PA is the set of all subsets of A Axiom of Union For any set A the set UA E y y E A exists UA called the union of A is the union of all sets which are elements of A Combining union and pairing we can see that AUB 6 AV E B exists because A U B UA The intersection A 1 B can be de ned as E A g E B so it is provided by Separation alone 116 The relative complement or set difference AB can be de ned as E A g g B so it is provided by Separation alone We do not have complements in general if we refer to the complement of a set A it is always actually a relative complement X A for some set X whose identity is to be understood from context For example if A is intro 1uce 1 as a set of natural numbers references to its complement will probably refer to N A The ordered pair b is de ned as Theorem b 2 ad gt a c b 2 it This theorem tells us everything we need to know about ordered pairs If a E A and b E B observe that E PA Q PA U B and 011 6 PAU B is obvious This means that b E P PA U In turn this means that Theorem For every set A and set B the set A X B the cartesian product of A and B de ned as E P PAUB g 3o 6 AElb 6 B42 2 exists and contains every ordered pair whose rst term is an element of A and whose second term is an element of B Once we have ordered pairs we can de ne the machinery of relations and functions A relation with domain A and range B is a subset of A X B Note that general relation symbols like 2 or Q do not as a rule de ne sets only relations whose domain and range are restricted to elements of speci c sets can be coded by sets A function with domain A and range B is a relation f with domain A and range B with the additional properties that E AEly E E and E AVy E B 2 E E f E f gt y For each element E A we de ne f as the uniquely determined y such that 77 y E f A function f A gt B is an injection or is one to one iff for all a7y 2 implies 2 y A function g A gt B is a surjection from A to B or is said to be onto B just in case Vy E BEL E Aga A function f A gt B is said to be a bijection iff it is an injection and is also a surjection from A to B A bijection is a one to one correspondence We say that A N B A and B are the same size just in case there is a bijection from A to B 117 Now we de ne the natural numbers The basic idea is that we want to de ne each natural number n as a set with n elements This makes 0 the empty set Notice that for any n gt 0 the set 0 n 1 has n elements We de ne it as 0 n 1 This means that 0 0 1 0 2 0 1 0 Notice that for any natural number n nUn 0 n1Un 0 n1 n n 1 We want to de ne the set of all natural numbers For this we need a new axiom Axiom of In nity There is a set S such that 0 E S and E S gt U E S Fix a set S which witnesses the truth of the axiom We can de ne N the set of natural numbers as n g VA 6 PS 0 E A E A gt arU E A gt n E This set will clearly contain our natural numbers 0 1 2 3 and is the intersection of all sets which contain all of them We need the Axiom of In nity to say that there is at least one set which contains 0 and is closed under the successor operation notice that AU exists for any set A not just for natural numbers Now we de ne notions of counting We say that a set A is nite just in case there is a natural number n such that A N u If A is nite we let A represent the unique natural number n such that A N n it is of course necessary to prove a theorem that A N n for no more than one u or this de nition won t make sense If m and n are natural numbers we de ne m n as the unique p such that for any A N m and B N n with A 1 B 0 ie A and B are disjoint we have A U B p We can more explicitly de ne m n as m gtlt U n x If m and n are natural numbers we de ne mu 2 m X n Theorems need to be proved to show that the disjoint union of two nite sets is nite and that the cartesian product of two nite sets is nite It takes some work to prove that the axioms of formal arithmetic we provided above are true of our natural numbers it is necessary to restrict all quanti ers to the set of natural numbers in these axioms though 118 Theorem on Classi cation of Cyclic Groups Dr Holmes April 19 2004 The main theorem of section 209 characterization of cyclic groups is proved using a different strategy than is used in the book I made an error in preparing this proof and so had to wing it sorry Further the proof I did in class wasn t quite right either but the one given here is easier and I think now correct I also have a nice quick argument for Euler s formula Theorem Let G be a group of order 72 The following statements are equiv alent 1 G is isomorphic to Gquot G is a cyclic group N There are exactly elements of G of order d for each divisor d of 72 There are exactly d elements of G such that aid 1 9 First we show that 1 implies 2 and Assume that G is a cyclic group of order n Let g be an element of G of order 71 Every element of G can be written in the form 9 for some k with 0 g k lt n and the value of k is uniquely determined by the element of G Suppose aid 1 Then we have a g for a uniquely determined k with 0 g k lt 71 and we have 9 1 This can only be true if kd 171 for some 1 kd must be a multiple of 71 so In 93 This means that k must be a multiple of 3 and there are exactly d multiples of 3 which are greater than or equal to 0 and less than n Notice that if k is a multiple of 3 then kd will be a multiple of 71 so these values of k are exactly the ones which work and there are exactly d elements a of G such that 1quot An element a g ofG will have order 7quot such that CT is the least common multiple of k and 71 this implies 7quot W From this we see that a g has order 71 i 39 k is relatively prime to 71 and so there are 01 elements of Gquot of order 71 The set of elements y of G such that yd 1 is a copy of Cd and will include all elements of G of order d we have just shown that G contains elements of order d so G contains elements of order d 2 implies 1 is easy if a group of order 71 contains elements for each element d of n then it contains 02 2 1 elements of order 72 a group of order 71 with an element of order 71 is cyclic Now we show that 3 implies 2 which allows us to see that 1 2 and 3 are all equivalent This is where our proof is different from the proof in the book and it s also where we got confused We do not need strong induction 1 wrong about this in class Let G be a group of order n such that for each divisor d of 72 there are exactly d elements such that 1quot For each divisor d of 72 there is either an element of order d in the group or there is not If there is an element of order d the powers of this element make up a cyclic subgroup of order d which will contain all the elements y such that yd 1 and this group will contain elements of order d which will be all the order d elements in the group All elements of G will have a divisor of 71 their order so 71 the size of G can be expressed the sum of all the such that there is an element of order d in G But Edno d 71 so this sum must contain the for all dgn in order to add up to n and there are elements of each order d dividing 71 So 3 implies Of course this immediately implies that there is an order 7 element so we have 1 well To see that Edn d 7 consider the following For any 71 n is the number of positive proper fractions fractions less than one in simplest form with denominator 71 71 is the number of positive proper fractions with denominator 71 But every positive proper fraction with denominator 7 sim pli es to a uniquely determined positive proper fraction in simplest form with denominator some divisor d of 71 the number of these is Edno d and so this must be equal to 71 Math 387 Lecture Notes M Randall Holmes March 17 2004 Contents 1 Introduction 4 2 Monday January 12 4 21 Basic operations of propositional logic 4 22 The method of truth tables 6 23 Tautology entailment and equivalence 7 24 Informal introduction to natural deduction 8 3 Natural deduction formally introduced 9 31 Rules for conjunction 10 32 Rules for implication 10 33 An example 11 34 Rules for negation 12 35 Rules for disjunction 12 36 Rules for the biconditional 13 37 Derived rules 14 4 Wednesday January 14 20 5 Friday January 16 23 6 Tuesday Jan 20 25 61 Derived rules 25 62 Soundness and completeness 26 63 Expressive completeness 26 64 A digression one point basis 27 65 Development of algebraic rules 28 7 Wednesday January 21 31 71 Alternative interpretations and duality 32 8 Friday January 23 32 9 Monday January 26 sequent calculus introduced 36 10 Tuesday January 26 39 101 Sequent calculus continued 39 102 Natural deduction rules for quanti ers 42 11 Wednesday January 28 44 12 Friday January 30 44 13 Monday February 2 46 131 Sequent examples 46 132 Understanding a rule of sequent calculus as a distributive law in boolean algebra 48 14 Notes on the cut rule written Monday but not lectured Tues day 49 141 The relationship between the sequent calculus and natural de duction 49 15 Tuesday February 3 completeness of natural deduction 52 16 Wednesday February 4 58 161 Deriving rules for new logical operations 58 162 Translating natural deduction proofs into sequent proofs the need for the cut rule 60 163 Quanti ers reintroduced 62 164 Sequent rules for quanti ers 65 17 February 6 2004 65 18 February 9 2004 66 19 Tuesday February 10 20 Wednesday February 11 21 Friday February 13 22 Tuesday February 17 de Morgan laws for quanti ers 23 February 18 2004 231 first proof 232 second proof 24 February 20 2004 25 February 23 2004 251 first proof 252 second proof 26 February 24 2004 27 February 27 2004 28 March 1 2004 substitution and equality 281 Substitution 282 Equality 29 March 2 2004 30 March 3 2004 301 Equality rules for natural deduction 302 Numerical quanti ers 303 Completeness of sequent calculus 31 March 5 2004 Arithmetic Made Dif cult 32 Monday March 8 2004 commutativity of addition 33 March 9 2004 34 March 10 2004 68 68 69 77 80 80 82 83 98 101 106 111 35 Friday March 12 112 36 March 15 2004 set theory prerequisites for counting 115 1 Introduction This document contains the lecture notes for the foundational part of Math 387 section 1 spring 2004 The notes are organized by day I will provide the notes for each day either just before or just after lecturing If I provide them early I may of course not complete the planned lecture in which case I will insert the new date heading at the appropriate point 2 Monday January 12 21 Basic operations of propositional logic For the moment we use capital letters such as P Q R to represent state ments The only thing that interests us about the statements represented by capital letters is their truth value whether they are true or false We de ne operations on statements correspon 1ing though sometimes not precisely to certain conjunctions in English IP means not P or it is not the case that P The operation rp resented by I is called negation The English is unambiguous we can be certain that if P is true IP will be false and if P is false IP will be true We can summarize this in the following truth table P IP T F F T P Q means P and Q The operation represented by is called conjunction Again this is unambiguously determined by the English PVQ means P or Q The operation represented by V is called disjunc tion Here English is ambiguous If P is true and Q is false or vice versa it is clear that P V Q should be true and if P and Q are both false it is clear that P V Q should be false but it is not clear What truth value to assign if P and Q are both true The usual convention in mathematics is to use the inclusive or with the following truth table The operation exclusive or or xor will be represented by the notation EB and has the following truth table The notation P gt C2 is said to denote if P then Q It is a matter of philosophical debate Whether the meaning of if P then Q really depends only on the truth values of P and Q In mathematics the convention is to suppose that it does An expression of the form P gt C2 is called an implication The truth table for implication is The notation P ltgt Q is defined as denoting P if and only if Q which is often abbreviated as P iff Q This is true exactly when P and Q have the same truth value An expression of the form P ltgt Q is called a biconditional The truth table for the biconditional is 0 Order of operations I binds most tightly followed by A then V then gt then ltgt and EB the latter will seldom be used We can also use associa tivity of V and to drop some parentheses H and EB are also associative for what it is worth It never hurts to use redundant parentheses to make your meaning clear 22 The method of truth tables We have already seen truth tables used to de ne propositional operations They can also be used to analyze the behavior of complex propositions built using these operations For example we can use truth tables to show that P gt Q has the same meaning as IP V Q our convention on order of operations lets us write this instead of IP V Q Compare this with the truth table for P gt Q We give an example of a logical truth PAQ gt P which can be written P C2 gt P by order of operations veri ed by truth tables A different table style avoids the necessity of copying out many subex pressions in a truth table here we write the values of each subexpression below the symbol for its top level operation 6 23 Tautology entailment and equivalence In this section we introduce a new kind of variable script variables A B C a script variable stands for any expression of propositional logic not just a single propositional letter Strictly speaking we could have used script variables in our de nitions of propositional connectives IA is a formula of propositional logic for any expression A not just for propositional letters P as our less careful usage above might suggest For any formula A we say that A is a tautology symbolically l A if A is true no matter what values are assigned to the propositional letters appearing in A For example we showed l P C2 gt P above We have special terminology for tautologies which are implications or bicon 1itionals l A gt B may be written A l B and read A entails B The example just shown can be written in the form P Q l P l A ltgt B may be written A E B and read A is logically equivalent to B For example our argument that P gt Q has the same meaning as IP VQ could also be used to show that P gt C2 ltgt IP V Q is a tautology and so tlxatPaQE IPVQ It is important to notice that l A A l B and A E B are not formulas of propositional logic lIoreover A l 8 means something different from A gt B and similarly A E 8 means something different from A ltgt B For example P gt C2 is a sentence of propositional logic which may be true or false depending on what values are assigned to P and Q while P I Q is a statement about propositional logic which is false because P gt C2 is not a tautology 24 Informal introduction to natural deduction The method of truth tables is a complete technique for finding logical truths tautologies and determining entailments and equivalences in propositional logic However it is not very practical because the truth table for a formula containing 7 propositional variables will contain 2quot rows The truth table description of the behaviour of a logic circuit with 100 different inputs not 100 different logic gates as I mistakenly said in class would have 2100 N 1030 rows which can t be implemented in practice A peculiar feature of a proof by truth table is that all proofs of formulas with the same number of variables are essentially the same size since every possible assignment of values to the variables must be consi 1ered in 1ivi 1ually There are techniques of proof in propositional logic that can be more efficient it is unknown whether there is a technique of proof for propositional logic that is always more efficient for all known methods of proof in propositional logic the worst case bound for the proof of a tautology is the same 2quot as it is for the method of truth tables it is suspected but is not known that this will be true for any technique of proof it would be very exciting if a truly efficient proof technique could be found The method which we briefly and quite informally introduce here is called natural 1e 1uction there are various systems of natural 1e 1uction someone else s formalization could differ in detail from mine For each operation of propositional logic natural de 1uction provides a strategy for proving propositions with that operation as their top level op eration and a method for using propositions with that operation as their top level operation to deduce new conclusions For example to prove A B we prove A then prove B If we have a premise A B we can deduce A and B as conclusions To prove A gt B assume A add it as a new premise and prove B If we have A and A gt B as premises we can draw the conclusion 8 this is called the rule of modus ponens We present a natural de 1uction proof of P gt QQ gt R gt P gt R Goal top P gt Q Q gt R gt P gt R Assume 1 P gt Q Q gt R for Goal 1 P gt R Assume P 2 for Goal 2 R from 1 get 3 P gt Q from 2 and 3 get 4 Q by modus ponens from 1 get 5 Q gt R from 4 and 5 get R by modus ponens which is goal 2 and completes the proof of goal 1 which in turn completes the proof of the top goal This is not in our nal formalism but has the right structure Compare this with the truth table proof of the same tautology NQH w wwwwssss wwsswwss wewswsws wwwwssss sssswmssi wwsswwssg sswswwwsgt MMHHMMSSE sswssswsl wewswswsa ssssssssl wwwwssssg sssswswsl wewswswsa The natural de 1uction proof is smaller and implements a more intelligent and in some sense natural approach to proving the result 3 ZNaturaldeductknl nwna y39hmroduced In this section we present the formal details of our system of natural deduc tion Later on I plan to prove that every tautology and only the tautologies of propositional logic can be proved using natural 1e 1uction Each logical operation conjunction implication negation disjunction has two kinds of rules associated with it introduction rules which allow con clusions built with that operation to be proved and elimination rules which allow information to be extracted from premises built with that operation In this section I will usually not make the distinction between proposi tional variables P and script variables A standing for complex expressions which I intro 1uce 1 above the rules of natural deduction are valid if complex expressions are substituted for the letters appearing in them 31 Rules for conjunction Conjunction introduction P Q P Q Conjunction elimination P Q P or P Q Q In each rule the items above the line are premises which can be taken from earlier lines of proofs The item below the line is the conclusion a new line for the proof The rules can be abbreviated ci and ce the two different forms of ce could be called ce 1 and ce 2 but this seems too pedantic 32 Rules for implication Implication elimination modus ponens P H Q This rule may be abbreviated either ie or mp according to taste 10 Implication introduction This rule has a rather different structure 1 P hypothesis for implication introduction Goal Q representing an unknown number of proof lines n Q we don t know what rule we use to get the conclusion n1 P gt C2 implication intro 1uction lines 1 11 The box indicates a subproof with the additional hypothesis P No line of the subproof can be used outside the subproof Lines outside the subproof may be used in the subproof unless they belong to some other subproof which does not contain the given subproof This rule embodies the natural strategy for proving an implication P gt C2 assume P and prove Q this proof allows you to conclude that P gt C2 is true whether P is true or not if P is true we use the auxiliary proof to show that Q is also true so P gt C2 is true if P is false P gt C2 is vacuously true The line labelled Goal is a comment it tells us what conclusion we need to close the subproof 33 An example We use the rules for implication and conjunction to prove P gt C2 C2 gt R gt P gt R this is the formalization of the last example in the previous section Goal P gt C2 C2 gt R gt P gt R Since this is an implication we attempt to apply implication intro 1uction 11 1 P gt gt R hypothes1s for 11 Goal P gt R Once aga1n we attempt 11 2 P hypothesis for 11 Goal R 3 P gt Q e l1ne 1 4 Q mp l1nes 23 5 6 Q gt R e l1ne 1 R mp l1nes 45 7 P gt R 1mpl1cat1on 1ntro 1ut1on l1nes 2 6 8 P gt gt R gt P gt R 11 l1nes 1 7 34 Rules for negation We resume the development of rules for the other log1al operat1ons negation introduction Th1s 1s another rule of the same form as 1mpl1ca t1on 1ntro 1ut1on 1 P hypothes1s for negat1on 1ntro 1ut1on Goal ontrad1ct1on represent1ng an unknown number of proof l1nes n Q IQ we don t know what rule we use to get the onclus1on n1 IP negat1on 1ntro 1ut1on l1nes 1 n We prove that P 1s false by assum1ng P and deduc1ng a ontra 11t1on There 1s a negat1on el1m1nat1on rule but 1t 1s l1sted among the der1ved rules below 35 Rules for disjunction Each of the rules for 11sjunct1on 1s l1ke the rule of onjunct1on el1m1nat1on 1n hav1ng two symmetr1c forms We w1ll not requ1re use of separate names for the two forms of each rule 12 Disjunction elimination Either pvo ng I pvo Q Disjunction introduction Either 1 IP hypothesis for disjunction intro 1uction Goal Q representing an unknown number of proof lines n Q we don t know what rule we use to get the conclusion n1 P V Q disjunction intro 1uction lines 1 11 I 1 Q hypothesis for disjunction intro 1uction Goal P representing an unknown number of proof lines n P we don t know what rule we use to get the conclusion n1 P V Q disjunction intro 1uction lines 1 11 36 Rules for the biconditional For now our of cial rules for the biconditional amount to a de nition of PHQasP gtQQ gtP Biconditional introduction wakoam PHQ 13 Biconditional elimination P ltgt Q 1 gt Q A Q gt P The following set of rules might be found more natural These are the elimination rules P w t t w t O39UQ 39UQQ O39UQ l l Tl is is the inrrm lncrirm rule 1 P hyp for biconditional intro 1uction ii Q n1 Q hyp for biconditional intro 1uction ni P ni1 P ltgt Q bicon 1itional intro 1uction lines 1 n n1 ni These rules can be derived from the of cial de nition this is left as an exercise for the reader 37 Derived rules The rules already given are the basic rules of our system but of course there are many simple rules of inference that are equally basic to reasoning in practice In this subsection we derive some of them 14 Excluded middle Goal P V IP 1 IP hypothesis for disjunction intro luction 2 IP copy line 2 3 P V P disjunction intro luction lines 1 2 We can use this to prove any statement of the form P IP and rather than reproduce this proof Whenever we do this we use the new rule PVIP which we call excluded middle or exc mid Note that this rule does not require any premises Double negation Under this heading we prove the rules for intro luction and elimination of double negations and introduce the method of proof by contra liction Double negation introduction 1 P Goal IIP 2 IP hypothesis for negation intro 3 P IP ci lines 12 4 IIP negation intro lines 2 3 This justi es the rule of double negation intro luction dni P p Double negation elimination 1 P Goal P 2 P V IP exc mid 3 P Lil lines 12 This justi es the rule of double negation elimination dne p P Proof by contradiction Goal P 1 IP hypothesis for n i n Q Q n1 IIP negation intro lines 1 n n2 P 1ne line n1 justi es the rule of proof by ontra 1ition which is just one line shorter Goal P 1 IP hypothesis for proof by contradiction i112 Q n1 P proof by ontra 1ition lines 1 n Modus tollens The rule of modus tollens mt is the additional implica tion elimination rule P gt C2 rQ IP It is justi ed by the following proof 1 P gt C2 2 Q Goal IP 3 P hypothesis for n i 4 Q mp lines 13 5 Q Q i lines 24 16 6 IP ni lines 3 5 Simple disjunction introduction The rules of simple disjunction intro duction are 71 P Q and Q P Q The formal proofs follow 1 P Goal P V Q 2 Q hypothesis for disjunction intro Goal P 3 P copy line 1 4 P V Q di lines 2 3 The other proof is very similar 1 Q Goal P V Q 2 IP hypothesis for disjunction intro Goal Q 3 Q copy line 1 4 P V Q di lines 2 3 The simple disjunction rules sdi are often presented as the basic disjunction intro 1uction rules In this case one will also need reasoning by cases the next derived rule as an elimination rule and excluded middle Our choice of basic disjunction rules is more economical Reasoning by cases The rule of reasoning by cases cases for short is PVQ P gtR Q gtR The formal proof follows 1 P v Q 2 P gt R 3 C2 gt R Goal R IR hypothesis for proof by contra 1iction IP mt lines 24 Q de lines 15 R mp lines 36 R IR ci lines 4 905130er 9 R proof by contradiction lines 4 8 negation elimination P P Q This expresses the idea that anything can be deduced from a contra diction any proposition is implied by a false proposition as is clear from the truth table for implication 1 P premise 2 IP premise Goal Q 3 Q hyp for proof by contra 1iction 4 P IP ci lines 12 5 Q proof by contradiction lines 3 4 This proof might make one vaguely ill since the contra 1iction derived in the box has nothing to do with the hypothesis intro 1uce 1 in the box but it is formally correct 18 16 Morgan rules T110 10 Morgan 111108 2110 as follows M pA Q 1 IP V Q pr0mis0 Goal IP IQ Goal IP 2 P 11yp for 111 3 P V Q sd1 11110 2 4 P V P V 01 14 5 IP 111 111108 2 4 Goal IQ 6 Q 11yp for 111 7 P V Q sd1 11110 6 8 P V IP V 01 17 9 Q 111 111105 6 8 10 IP IQ 01 59 pA Q pVQ 1 IP IQ pr0mis0 Goal IP V Q 2 P V Q hyp for 111 3 IP 00 11110 1 4 Q 00 11110 1 5 P 10 111108 24 6 P IP 01 111108 53 7 P V 111 111108 2 6 M pv Q 19 1 IP Q premise Goal IP V IQ 5 3 IIP hyp for 11 Goal IQ Q hyp for 111 P d11e line 3 P Q 1 lines 54 4 5 6 7 P IP 1 lines 16 8 Q 111 lir1es 4 7 9 IP V IQ 11 lir1es 3 8 p v Q quot1 Q 1 IP V IQ premise Goal IP Q P Q hyp for 111 P e line 2 IIP 1111 line 3 Q 1e li11es 41 Q e line 2 Q Q 1 lines 56 rlgvsleswso 8 P 111 lir1es 2 7 4 Wednesday January 14 Today we 111 proofs in class and we will continue on Friday The theorems proved today were IAB IAVIB with the following proof Goal IA B gt A V IB 20 1 A B 11ypfor11 G 2311 A B 2 IIA 11yp for 11 G 211 B 3 B 11yp for 111 Goal contradiction 4 A 1110 11110 2 5 A B 01 111108 34 6 A B IA B 01 16 7 B 111 111108 4 6 8 IA V B 111 111108 2 7 9 A B gt IAV B 11 111108 1 8 and PVQ gtRlt gtP gtRAQ gtR Goal PVQ gtRlt gt P gtRQ gtR A conjunctive goal can b0 b1ok0n into two subgoals Goal PVQ gt R gt P gt R Q gt R 1 P V gt R 11yp for 11 Goal P gt R C2 gt R G 211 P gt R 2 P 11yp for 11 3 P V Q sd1 11110 2 4 R mp 111108 13 5 P gt R 11 111108 2 4 Goal C2 gt R 6 Q 11yp for 11 7 P V Q sd1 11110 6 8 R mp 111108 17 9 C2 gt R 11 111108 6 8 7 P gt R C2 gt R 01 111108 59 8 PVQ gtR gtP gtRQ gtR Goal P gtRQ gtR gtPVQ gtR 21 1b P gt R gt R l1yp for 11 Goal P V C2 gt R 2b P V l1yp for 11 Gal R 3b IR l1yp for proof by contradiction Goal contradiction 4b P gt R 00 11110 1b 5b IP modus toll0ns lin0s 3b4b 6b Q 10 lin0s 2b6b 7b C2 gt R 00 11110 1b 8b R modus pon0ns lin0s 6bb 9b R IR 01 lin0s 3b8b 10b R proof by contradiction lin0s 3 9 11b P V gt R 11 lin0s 1 9 12b P gt R gt R gt P V gt R 11 lin0s 1 11 13111 gt RWQ gt R gt two gt RPVQ gt R gt P gt R Q gt 01 lin0s 8 12b 14P gt R C2 gt R ltgt P V C2 gt R biconditional introduction 11110 13 0110 issu0 which cam0 up 111 class which is worth r00ording is how to l1andl0 tl10 situation of a conjunction as a goal Goal A B I us0d tl10 script l0tt0rs to 0mpl1asiz0 tl10 fact that tl10s0 ar0 unknown but compl0x 0xpr0ssions tl10y ar0 c0rtainly not propositional l0tt0rsl Wl1il0 w0 ar0 doing natural d0 1uction I won t usually draw this distinction Th0 structur0 of tl10 proof will b0 Goal A 8 Goal A 111 A Goal 8 11 B n1 A B 01 lin0s 11111 Th0 proof of a biconditional will l1av0 this form if w0 us0 tl10 rul0 for boconditionals giv0n 111 tl10 l1om0work 22 Goal A ltgt 8 Goal A gt B m A gt 8 Goal 8 gt A n B gt A n1 A gt B B gt A i lines mn n2 A ltgt l3 biconditional intro from homework The rule you develop in homework problem 3 should involve subproofs something resembling the reasoning I give here could be used to justify the rule you develop 5 Friday January 16 We did more proofs at the board The tautologies which we proved were PAQ gtRltgtP gtQ gtR Goal PAQ gtRlt gtP gt Q gtR Goal P Q gt R gt P gt C2 gt R 1 P gt R hyp for ii Goal P gt C2 gt R 2 P hyp for ii Gwl C2 gt R 3 Q hyp for ii Goal R 4 P Q i lines 23 5 R mp lines 15 6 C2 gt R ii lines 3 5 7 P gt gt E ii lines 2 6 8 P gt R gt P gt gt R ii lines 1 Goal P gt C2 gt R gt P Q gt R 23 9 P gt gt R 11yp for 11 Goal P C2 gt R 10 P Q 11yp for 11 Goal R 11 P 00 11110 10 12 C2 gt R 1np 11n0s 9 11 13 Q 00 11110 10 14 R modus pon0ns 11n0s 12 13 15 P gt R 11 11n0s 10 14 16 P gt gt R gt P gt R 11 11110s 9 15 17 P gt C2 gt R ltgt P C2 gt R biconditiona1 introduction 11n0s 816 and AABVAAIB gtA Ga1 A B A IB gtA 1 A B V A IB 11yp for 11 G a1 A 2 IA 11yp for proof by contradiction Goal contra 1iction Goal IA B to 11s0 With 10 With 11110 1 3 A B 11yp for 111 4 A 00 11110 3 5 A IA 01 11n0s 24 6 A B 111 11110s 3 5 7 A B 10 11n0s 16 8 A 00 11110 7 9 A IA 01 11110s 28 10 A proof by contradiction 11n0s 2 9 11 A B V A B 11 11n0s 1 10 This is t110 proof W0 did 111 class At that tim0 W0 had not y0t intro 1uc0 1 t110 r1110 of proof by cas0s Wit11 proof by cas0s you g0t a 11111011 0asi0r proof W11ic11 W0 10av0 as an 0x0rcis0 24 6 ThesdayJan 20 6 1 Derived rules Here is a brief discussion of how to introduce and use a new rule At this point we do not discuss rules that involve subproofs boxes A rule such as P P gtQ is used in the following situation a P b P gt C2 c Q mp lines ab or more typically in a situation like this a A B b AAB gtCD c C V D mp lines ab Here the letters P and Q in the rule are replaced by the expressions AAB and C VD respectively All of our rules have the property that the letters in them can be replaced by arbitrary expressions as long as every occurrence of the same letter in the rule is replaced by the same expression The same is actually true of any proof in our system To prove a new rule such as vWAQ IP V IQ we can give a proof which has the expressions above the bar as premises and the expression below the bar as conclusion 1 P Q premise Goal P V IQ 2 IIP hyp for 11 Go 1 Q 3 Q hyp for 111 4 P dne line 2 5 P Q 1 lines 34 6 P IP 1 lines 16 7 Q 8 J V IQ 11 2 7 This completes the proof of the derived rule We give it the name deM 1 it is one of the de Morgan rules It can be used just like the basic rules a IIR U V V b IR V U V V deM 1 line a l39otice that the letters in the original rule have been replaced with com plex expressions The derived rule could be eliminated from the proof by in serting the complete proof from above with the appropriate substitutions using derived rules can make proofs much shorter We will give a formal treatment of how to develop rules with subproofs later you can see examples of such derivations above 62 Soundness and completeness A proof system for an area of mathematics is sound if all the statements it proves are correct It is complete if it can prove as a theorem every statement expressible in its language which is actually true We will prove later that our system of natural deduction is sound and complete We point out that we already have a sound and complete proof technique for propositional logic the method of truth tables What we will do today is develop an algebraic system of logic which we can prove to be sound and complete because it can be seen to implement the method of truth tables 63 Expressive completeness We use truth tables to demonstrate how any function of propositions which has a truth table can be expressed in terms of the operators A V and I For example 26 39 39 39 i i i i39 39 i i39 39 i i wswswswsm 39 39 i i39 ig The function fPQR this is a purely temporary notation can be represented by the expression PAQARPAIQARPAIQAIRVIPQIR This expression is a disjunction of conjunctions of propositional letters and negations of propositional letters Each conjunction represents one of the rows of the truth table There is one special case if all rows of the truth table are F we can use the contra 1ictory expression PIP to represent its value We also introduce the notations T and F for the truth values into our language We say that an expression in which negation is applied only to single letters and no disjunction appears as part of a conjunction is in disjunctive normal form DNF The expressions we derive from truth tables have the additional features that each conjunction contains the same letters in the same order sometimes negated and no conjunction or disjunction contains duplicated terms 64 A digression onepoint basis De ne a new propositional operation P l Q as IPQ I used a downward arrow for this in class but I don t know how to typeset it P l Q can be read Neither P nor Q in English We point out the following equivalences pspip PVQE W39U VQE PlQEU lQHU lQ 27 PAQE l J V Q E J l IQEU lmHQlQ The l operation can be used to express I and V so it can be used to de ne all propositional operations de ned by truth tables This is more amusing than practicall An exe ise is to show that the operation PgQ de ned as P Q can also be used to de ne all other propositional operations 65 Development of algebraic rules We will develop a set of rules for calculation with propositional operations which will enable us to transform any expression written with the proposi tional operations and or and not into DNF then transform it into the form representing its truth table We begin with rules needed to put conjunctions and disjunctions in de sired order and remove duplicate items commutative laws PAQEQAP PVQEQVP associative laws PAQREPQR PVQVREPVQVR idempotent laws PAPEP PVPEP contradiction P J E F Note that this rule also allows elimination of duplicated letters in con junctions 28 identity law PVFEP This law allows contradictions appearing as terms of disjunctions to be ignored zero law PAFEF This law allows conjunctions containing contradictions to be reduced to F l39ow we introduce rules to enable reduction of any expression to DNF de Morgan laws IPQ E IPV IQ PvQE pA Q double negation J E P Repeated use of these rules will cause all negations to be applied to single propositional letters distributivity of conjunction over disjunction PAQVREPQVPR Use of this rule will eliminate all conjunctions with disjunctions as com ponents combined with commutativity of conjunction in order to deal with disjunctions appearing on the left of A It should be clear that enough applications of the last four rules will reduce any expression to DNF The rules above allow us to convert any term in DNF to one in which each conjunction contains at most one occurrence of each letter Occurrences of P or IP twice are eliminated by idempotent laws and occurrences of P and IP together allow the entire conjunction to be reduced to F and then eliminated completely using an identity law unless the whole expression converts to F 29 Further we can put letters in each conjunction in the same order using associative and commutative laws Suppose that we have an expression in letters P Q and R which contains a conjunction which is too short for example P Q We can replace this with the following disjunction of conjunctions containing all the letters PAIQARVPIQIR The same process can be iterated to add more missing letters as needed The equivalence needed to justify this is P E P Q V P Q We can justify this by making the following calculation PEPTEPAQVIQEPQVPIQ Each of the steps in this calculation is justified if we add the following two equivalences another identity law PATEP excluded middle P V IP E T So we have shown that any expression can be converted to an expression in Dl39F coding its truth table Finally we show that any tautology can be reduced to T A tautology has a truth table containing all possible conjunc tions If the three letters P Q and R are used we will for example have P Q R and P Q IR as two disjuncts of the DNF term they can be moved next to each other using associativity and commutati ity of V then we can apply the same result we used to add extra letters to conjuncts above to reduce the disjunction PAQARVPQIR to P Q Similarly every occurrence of R can be eliminated Similarly one letter after the other can be eliminated until just one is left P V IP E T 30 7 Wednesday January 21 I list the axioms of boolean algebra pqqp pqqp pq 7 p QH m pq7 ppp ppp 27 27 1 pH 0 p0p 2712 p11 p00 PQ739P 1P7 pqr p9p7 pqpq pqpq pp If we interpret 0 as F 1 as T p as Ip pq as p q and p q as p V q all the axioms are interpreted as logical equivalences All of the equivalences used in the previous section are found here plus some extras We reviewed the argument of the previous section that boolean algebra allows any expression to be converted into a form which represents its truth table and further allows the truth table of a tautology to be converted to T or 1 We carried out the proof of the tautology P C2 gt R gt P gt C2 gt I m going to give the short proof here p gt q is equivalent to Ip V q or p q Using this we translate PAQ gt R gt P gt C2 gt R to PQ R P Q R l39ow observe that PQ R PQR PQR so the whole expression can be written PQR P Q R l39ow observe that PQR Q R so we can write the whole expression as PQR PQR 1 The proof of the tautology is complete l39otice that our style of reasoning here is that of algebra as we learned it in high school the rules are not quite the same but the way the rules are used is the same Each rule is a universal statement in a rule like p q q p we can replace p and q with any desired expressions and we are allowed to substitute equal subexpressions for one another By way of contrast in natural de 1uction we are not allowed as yet to use logical equivalences to make substitutions for deeply embedded subexpressions though we could v 31 add a rule which allows this all of our rules work on the top levels of expressions 71 Alternative interpretations and duality There are other possible interpretations of boolean algebra of which we give two If we were to allow 1 to mean F and 0 to mean T instead of the reverse it is straightforward to check that pq would now mean qu and pq would mean p q It is interesting to observe that the axioms of boolean algebra remain axioms if addition is interchanged with multiplication and 1 is interchanged with 0 This duality can also be explained using truth tables If T is replaced with F everywhere in the truth table for A we obtain the truth table of V with the lines in a different order similarly the table for transforms to a table for V and the table for I to a different table for I Further if we take two logically L e pie ion and tran f orm them both in this way we still get logically equivalent expressions which suggests that the procedure of interchanging I and V and xing I in ex pressions with no other operators should convert logic equivalences to other logical equivalences as we see in the case of the axioms of boolean algebra in the standard interpretation Another interpretation is in terms of sets addition could be union of sets multiplication could be intersection of sets and negation could be comple ment relative to some xed universe while 0 would be the empty set and 1 would be the universe 8 Friday January 23 Our topic today is another algebraic approach to propositional logic The idea is to use the operations of arithmetic mod 2 to implement the operations 32 of propositional logic The following tables express well known properties of even and odd integers if we let representative elements 0 and 1 stand in for the classes 0 0 0 1 1 0 0 0 1 0 The only unexpected result is 1 1 0 and what this means is an odd number plus an odd number is an even number which is unexceptional The following algebraic rules are inherited from the algebra of the integers HOquot OI AI A myym mywmyz my my ar0ar 3713 myarz There are two additional special rules which clearly hold 2 0 2 In the lecture in class I included m0 as an axiom but in fact m0 y 0 proves this from the axioms given If we interpret 1 as true and 0 as false then multiplication will be inter preted as and addition will be interpreted as EB the exclusive or We now show how to define other logical connectives in terms of this algebraic interpretation 17 1 is easily checked mVy21IarIy 11ar1y 11arymyaryary establishes the definition of V y y my mvy myb y1my1my 1aryyyar1armg 33 establishes the definition gt y 1 3769 atwhyW 1mmy1yym 2 1yyarararyarymaryaryymyyar 2 1ary in the last step the terms cancel in pairs As an example we prove that P C2 gt R is logically equivalent to P gt C2 gt R PAQ gtRPQ gtR1PQPQR P gtQ gtR1PPQ gtR 1PP1QQR1PPPQPQR1PQPQR and this establishes the desired equivalence Just as in the case of boolean algebra there is a dual interpretation of this algebraic system as logic In the dual interpretation 0 represents true 1 represents false addition represents ltgt and multiplication represents V The representation of GB or ltgt by addition mod 2 gives a quick argument that these operations are commutative and associative It also allows us to quickly determine the rather surprising meaning of expressions rather like P1 EB P2 EB 65 P7 which does not mean that exactly one of the Pn s is true or P1 ltgt P2 ltgt Pn vhich does not mean that all the H s are equivalent A sum an 777 of mod 2 integers will be equal to 1 precisely if an odd number of the are odd In the original interpretation this means that P1 EB P2 EB 65 P7 is true just in case an odd number of the H s are true In the dual interpretation we find that P1 ltgt P2 ltgt P is false just in case an odd number of the H s are false so true just in case an even number of the H s are false l39ow we present a proof of the completeness of our algebraic presentation it is obvious that the rules we have given are sound but it remains to be shown that every tautology can be reduced to 1 using our rules 1 llultiplication distributes over both multiplication and addition My z 37W my m 34 2 Case analysis myvmymy1mymyymym justifying the rule C We define where A and a are any expressions and is a variable as the result of substituting a for in A are For any expression A mA 2 aA1 The procedure for showing this is to distribute the factor over every product and sum in the term A so that every variable or occurrence of 0 or 1 is multiplied by Then replace each occurrence of with the logically equivalent m1 then undo the distribution giving arA1 For any expression A A IarA0 This is proved in the same way as the previous equation but one uses the identity m1ar mar0m0 instead of 2 m1 It follows that any expression A satisfies A 2 mA u A 2 We give example calculations ymygt my may m1 myltm1gtltmygt m y 1y illustrates the way that substitutions are proved mymyar1y1yIat0y0y area111ltwgtlt1010meta100gtlt ygtlto000gtgt x91 y Wyl WM WW and the last expression codes the truth table of the original expression in an obvious way If all of the final factors of 0 or 1 in the expression coding the truth table then repeated use of the identity murar1ar1 35 will reduce this expression to 1 which establishes completeness of this system This kind of completeness proof will actually work using boolean algebra as well boolean multiplication distributes over both addition and multipli cation y V is an identity and the proof that 7714 mAll and 0314 works the same way too so this method of simulating truth table reasoning will also work in boolean algebra 9 h40ndayJanuary 265equentcahn usin troduced Today I am introducing yet another and the last system of proof for propo sitional logic that we will consider It is called sequent calculus A sequent is a notation F l A where F and A are finite sets of propo sitions in our usual notation We adopt the convention that a proposition P can stand for the finite set with P as its only element and that a notation like F P will stand for the set F U P sets are just represented as comma separated lists The fact that our lists represent sets allows us to ignore order of items in lists and allows items to be duplicated in lists harmlessly We say that a sequent F l A is valid if any assignment of truth values to propositional letters in the sequent which makes all propositions in the set F true makes some proposition in the set A true A simple example of a valid sequent is P l P More generally any sequent F P l P A in which there is a proposition which appears in both sets is valid if all propositions on the left are true then P is true and P is one of the propositions on the right as well We introduce basic rules for negation and conjunction and use them to derive rules for disjunction and implication FFAA D AFA DAPA Fk AA The negation rules simply cause the negated expression to be moved across the turnstile 36 To see for example that the rst rule is valid suppose that the sequent above the bar is valid so that any assignment of truth values to propositional letters which makes all sentences in F true either makes A true or makes some sentence in A true This implies that any assignment of truth values to propositional letters which makes all sentences in F true and also makes IA true must make some sentence in A true which is the condition of validity of the sequent below the bar DAABFA DABPA FPAA FPBA rkAAaA We present the derivation of an obviously valid sequent PlP R Pk PAIPl W A sequent l P asserts that P is a tautology if every proposition in the empty set is true vacuously true then P is true Similarly a sequent P l asserts that P is contra 1ictory The sequent with which we start is valid because it has P on both sides The sequent is built from the bottom an advantage of the sequent calculus is that the construction of proofs is driven by the form of the statement to be proved this is partially true in natural deduction proofs We now present the derivation of rules for disjunction and implication The derivation F P l A P Q l A F l IP A F I Q A F l IP Q A F I IP Q l A DPVQFA justi es the rule F P l A P Q l A DPVQFA 37 The derivation F l P Q A F P I Q A F IP Q l A F P Q l A 1 l P Q P l P v Q A justi es the rule F l P Q A F l P v Q A it is not acci 1ental l39otice the symmetry between the rules for the dual operations and V The derivation F P I Q A 1 l IP Q A F l P v Q A F l P gt Q A justi es the rule TPlQA r l P gt Q A Set A 0 in this rule and get F P I Q 1 l P gt Q If you read this carefully you will see that this is basically the implication intro 1uction rule of our natural deduction system The derivation F l P A F P l A F Q l A F P v Q l A 1 P gt Q l A 38 justifies the rule rtnA thA DPanA This rule will look quite peculiar understan 1ably We do not usually use P gt Q as a premise all by itself we use it in the context of a rule like modus ponens with an additional hypothesis We demonstrate that modus 90718716 is provable using this rule APAB ABtB AAaBkB The two premises of this deduction are both valid because they have an identical letter on both sides of the turnstile The conclusion is the rule of modus 90716713 The whole deduction is an example of the second rule for implication with T 2 A A 2 B P 2 A and Q 2 B 10 39TuesdayJanuary 26 101 Sequent calculus continued Another way to view sequents is to consider the circumstances under which a sequent is invalid F l A will be invalid if there is an assignment of truth values which will make all sentences in F true and all sentences in A false The strategy of proof in sequent calculus can then be viewed as an attempt to invalidate the sequent we start with We outline this approach First we consider the basic rules We only need to consider the rules for I and A because we know that all other operations can be de ned in terms of these two and also because we know that the rules for the other propositional operations have been derived from these F l A A F IA l A If we aim to make all sentences in F true 2A true and A false this is exactly the same thing as to make all sentences in F true and to make A and all sentences in A false 39 DAPA FFAAA If we aim to make all sentences in F true and to make IA and all sentences in A false this is exactly the same thing as to make all sentences in F and A true and to make all sentences in A false DAABFA DABPA To make all sentences in F and the sentence A B true and make all sentences in A false is exactly the same thing as to make all sentences in F true along with A and B and to make all sentences in A false FPAA FPEA FFAAB To make all sentences in F true and to make A B and all sentences in A false is the same thing as to be able to do one or both of the following either make all sentences in F true and make A and all sentences in A false or make all sentences in A true and make B and all sentences in A false It follows from this consi 1eration of the individual basic rules and similar arguments can be made for each of the rules derived above that if we have a partial proof tree of a sequent we can invalidate that sequent if and only if we can invalidate some sequent at the top of the proof tree This means that if the top of the proof tree contains only axioms sequents of the form F P l P A then the sequent at the base of the proof cannot be invalidated and of course this is what we mean by having a complete proof Further notice that every application of a rule makes the sentences in the sequents simpler if we continued applying the rules long enough all top sequents would consist only of single letters we don t always do this because the sequents may become axioms before they are completely atomized in this way If every top sequent is an axiom we of course have a proof If we have a top sequent which is not an axiom then we can invalidate the sequent at the base by assigning all propositional letters to the left of the turnstile the value true and all propositional letters to the right the value false To be more precise on any branch of the tree going up the structure of the rules guarantees that a logical operation will be eliminated at each step Thus in a number of steps no greater than the number of logical operations 40 in the base sequent of the tree we will arrive at a sequent containing no logical operations just letters Every branch of the tree will be of uniform height bounded by the number of logical operations involved The potential size of the tree grows exponentially with the number of logical operations in the base sequent due to the possibility of branching at each step This is a completeness proof for this system for every tautology P there is a proof of l P in sequent calculus and for every non tautology there is a partial proof tree from which we can extract a counterexample showing that it is not a tautology Examples done in class we did two proofs of P C2 gt R gt P gt C2 gt R and used a proof tree to find a truth assignment showing that the bogus sentence P Q V R gt P R V Q R from the original version of assignment 2 is not a tautology RQPRR RQPQR Pan PAQLR FAQR2P2QlR PAQ gtRPI Q gtR PAQ gtRlP gtQ gtR I PQ gtR gtP gtQ gtR PQRlR Typesetting this so that it doesn t over ow takes some ingenuity I apol ogize if the result is not beautiful The main strategic choice I want to call attention to is the use of the rule for implication on the right instead of the left at the second step counting from the bottom of the tree The second example will show what happens if we use the left rule instead causing the tree to branch at the second level PQlPR PQIQR QlPAQLR PalPAQ7QgtR l PAQMPMQWD PAQgtRl PgtQgtR I PQ gtR gtP gtQ gtR RPQlR RPl Q gtR RI P gtQ gtR I m amazed that this one typeset inside the page l39otice that we still succeed in proving it if we choose to use the branching rule at the second 41 stage but the proof is a little larger Sequent calculus proofs like proofs in any known system of propositional logic can but don t always expand ex ponentially in size with the size of the formula being proved when explosion occurs it occurs because one is forced to use many branching rules rules like the rule for conjunction on the right which have more than one premise Finally we contruct a proof tree for the non tautology P Q V R gt P R V Q R and extract a truth assignment from it which makes this sentence false nor mag PQlRR P Ql P QAR PQI RQR PRlPRQR RQFPAEQAR PQVRlPRVQR PAQVRlPRVQR PAQVR gtPRVQR All the top level sequents in this proof tree are valid except P Q l R R from which we extract the information that if P and Q are true and R is false we can conclude that P Q V R gt P R V Q R is false as it is easy to check 102 Natural deduction rules for quanti ers The quanti ers for all Pat and for some Par or there exists such that Par are assumed to be familiar We will extend our natural deduction system and our sequent calculus with rules for reasoning with quantifiers algebraic reasoning with quantifiers is less common but I will try to put something in the notes about it eventually In this subsection I introduce the natural deduction rules for the universal quantifier V and the existential quantifier El I avoid technicalities about substitution which will enter into a final technically accurate statement of these rules To prove a statement of the form for all Par the standard strategy in a mathematical proof written in English is Let a be an arbitrary object prove Pa This strategy is captured by the universal quantifier intro 1uction rule ui now presented 42 Goal 1 a a hyp for ui must be new it cannot occur in any line which can be copied into the box n Pa n1 universal quanti er intro lines 1 11 The use of equality in the hypothesis line is purely arti cial it has the harmless side effect that is provable using just ui The restric tion on use of the variable a can be enforced in two ways we can either require that a not appear in any line which is usable inside the box it might appear in some other closed box this is our of cial rule The alternative is to restrict copying no line mentioning some other 0 outside the box may be copied into the box The universal quanti er elimination rule ue is very simple Pa If we have for all Par then we certainly have Pa for any particular The existential quanti er intro 1uction rule ei is similarly simple Pa If we have Pa this witnesses For the existential quanti er it is the elimination rule ee which is more complex m n Pa hyp for ee on line m must be new as in the ui rule ni Q Q must not include any occurrence of ni1 Q existential quanti er elimination lines m n nii This rule captures the idea that if we have an existential hypothesis Sarf we can introduce a speci c object a such that Pa Any state ment we can prove using the existential hypothesis which does not mention the named witness is uncon 1itionally proved 43 The use of a box here is optional we could adopt the convention that we can simply introduce a witness to any existential hypothesis and keep it around permanently However we believe that the named witness in this kind of proof is just as much a locally declared object as the arbitrary object in the universal intro 1uction rule s subproof 11 Wednesday January 28 On Wednesday I presented examples of the use of my computer software for sequent calculus I will create a section of notes on this session at some point in any event a manual will be available when we go to the computer lab with this next week 12 Friday January 30 Today we did sequent calculus proofs at the board I noted in class that it would be a good idea to attempt proofs of these tautologies using the other techniques that we have learned An easy one P Q l P P I Q gt P I P gt Q gt P Another easy one A l A I A 1A l IA w l Sticking with easy Pl P 1 151 l Pv IP Verging on trivial 44 A B l A B W A B l A v B l A B gt A v B It s tempting to do the left conjunction and right disjunction rules at the same time This is one direction of the de 1uction of one of dellorgan s laws AFAB BPAB FABmA FABmB PAVBwA kAvB B kAva A B Avmk AA 3 P Avaa AA B Here s the last example we did in class QPQP RQPP 39quot QIP PV Q gtPQp Pvmtm vagQ M g MQ M In this example I use the style of circling the sentences to which rules are applied actually I use boxes since that s What my typesetting program supports but it s not too pretty because I can t gure out how to keep the boxes from sticking to the line above I m sure there is a solution which I will nd eventually I made a remark during class about the application of certain rules which might be helpful In the branching rules FPAA FPBA rkAAaA DPFA DQPA DPVQPA 45 I PIQA FI P gtQA we may think of the procedure as follows In the conjunction rule on the left make two copies of the sequent and replace the conjunction with the first conjunct in one of them and with the second conjunct in the other In the disjunction rule on the left similarly make two copies of the sequent but replace the disjunction with the first disjunct in one of them and with the second disjunct in the other The left implication rule is a little trickier make two copies of the sequent omitting the implication on the left then in one of them add the hypothesis on the right and in the other add the conclusion on the left We discussed writing these up I suggested that a good way to document what rule is being used is to circle the sentence to which the rule is being applied at each step and indicate axioms by linking the identical sentences appearing on both sides of the turnstile I illustrated the circling in one of the examples above 13 Monday February 2 131 Sequent examples We did the following examples in class Proofs will be inserted into the notes Another deMorgan example IPQ gtIPIQ lP Pl V gt V Extract a counterexample from the proof tree of this classic non tautology waoawam 46 Q Pa P Q Q l P P QLQhP W hm FWQMQM From either of the invalid sequents at the top of the proof tree we read off the only counterexample the case when Q is true and P is false I said originally Prove the following tautology a natural deduction proof of this would also be of interest PVQIQVR gtP gtR RIMQR QJ lQJE PvQPI QR PvQRPI R PVQ239Q2P l R PVQLEQVRLPFR PVQIQVRPlR PVQIQVR l P gtR PVQIQVR gt P gtR But in fact this was not a tautology and we extract a counterexample The one invalid sequent at the top of the tree tells us that the only coun terexample is the case where P is true and Q and R are false The intended tautology was pvQMvam m vm and we did prove this together QFQRR neevmrn QWQPRR QRFRR eccvmrna wv mevmrn3 vaLvamkaR PVQA IQVRIPVR I PVQ IQVR gtPVR 132 Understanding a rule of sequent calculus as a dis tributive law in boolean algebra This example is provided as a way to understand what branching rules really are and also as motivation for possible future exercises The sequent P V Q R l S T is valid i quot P V Q R gt S V T is a tautology In boolean algebra notation this is P QR S T Apply de Morgan to get PQRST Further apply deborgan to get PQ R S T l39ow apply distributivity of addition over multiplication to get PRSTQRST and de Morgan again to get PR S TQR S T which in propositional logic is PAR gtSVTQR gtSVT This is a tautology precisely if the conjuncts P R gt S V T and Q R gt S V T are tautologies and this is true precisely if the sequents P R l ST and Q R l S T are valid This presentation is better than what I did in class because it shows that the division of the sequent into two simpler sequents really is the result of a single application of a distributive law There was another irrelevant application of distributivity in my class presentation 48 14 Notes on the cut rule written Monday ln n0tlectured39Tuesday 141 The relationship between the sequent calculus and natural deduction We started this topic at the end of the day lV Ionday These notes are not in final form but you are welcome to look them over We first discuss conversion of natural de 1uction proofs into a notation which looks more like that of sequent calculus A rule like P 7xe with no use of subproofs and more than one premise can be written in a style more like that of natural 1e 1uction 1 Q P Q This is clearly just a notational variation More useful is the conversion of rules involving subproofs For example the rule of implication intro 1uction becomes P I Q P gt C2 The line P I Q says that Q can be proved if P is added as an additional assumption The next step is to convert all lines to sequents This can be done by putting in front of every line of the natural de 1uction proof a turnstile and to the left of the turnstile putting all the assumptions needed for that line to follow these will be any premises of the whole argument plus the hypotheses of any subproofs The rules given above can then be written in a fully sequent form rep FPQ FPPAQ 49 F P I Q P l P gt Q It is easy to see that these rules are valid in the sequent calculus and provable using our rules Additional consi 1eration is required to justify the use of previous lines of a proof in natural 1e 1uction We can copy lines from parts of the proof with fewer assumptions from outside current boxes Fl P FUAlP It s actually easy to see that the following more general rule of weaken ing is valid in sequent calculus F l A F U F2 l A U A2 If it follows from all sentences in F being true that some sentence in A is true it certainly follows from all sentences in F U F2 being true that some sentence in A which will also be in A U A2 will be true We can add stuff to sequents freely on both sides and they stay valid l39otice that this is automatically enforced by our rules because axioms stay axioms and applications of rules stay valid applications of rules if the contexts F and A are enlarged The disjunction intro 1uction rules take the following form in sequent style notation FkaP FkaQ FpPkQ FkaQ These forms are not precisely what we would want both sequent and conclusion cry out for proof using the sequent F l PQ but the natural deduction context does not so far suggest a use for multiple conclusions A convention to the effect that additional conclusions on the right stand in for the negations of these conclusions on the left could be useful but 50 it does mean that a sequent with multiple conclusions has several different meanings depending on which conclusion is to be proved FPPAQ FkP FFPAQ F I Q are clearly valid inferences in sequent calculus They go against the grain from our sequent calculus standpoint because they prove simpler conclusions from more complex hypotheses l39otice that a sequent proof of F l P Q from our rules seems to require the existence of sequent proofs of F l P and F I Q already in existence as prerequisites rk p FkaQ er and Tk Q FkaQ FkP have the same unsatisfactory property from our sequent calculus stand point of having more complex premises than conclusions In the first case the existence of sequent proofs using our rules of the premises seems to require the existence of sequent proofs of F P l and so by weakening of F P I Q and of F l P Q The second case admits of a similar analysis F l P F l P gt Q P I Q has the same unsatisfactory characteristic But notice that a sequent proof using our rules of the two premises seems to require a proof of F l P and so by weakening of F l P Q and a proof of F P I Q A look at the negation intro 1uction rule will give the clearest indication of what we are lacking here DAFPA P Fk A 51 A proof tree on the premise of this reasoning has the following structure r rpk DAPP TEQT DAFPA P Fk A All of the translations of natural deduction reasoning given above would become valid in our system if we adopted the following rule called the cut rule FPRA DPFA FPA In the negation intro 1uction example we could use cut to deduce F A l and then F l IA from the sequents at the top of the proof tree just given This rule is clearly valid But it is certainly incompatible with the phi losophy of our sequent calculus any number of extra logical operations may be intro 1uce 1 in the expression P whose structure is not motivated in any way by the structure of the sequent F l A The actual situation is that the rule is useful for interpreting natural deduction rules sound but not required anything that can be proved with the cut rule can be proved without it and in fact we already know this because we know that every valid sequent can be proved using our sequent rules 15 Tuesday February 3 completeness of nat uraldeduc on In this section I present the proof of completeness of natural deduction The strategy is to interpret sequents as making assertions about the ex istence of natural deduction proofs then show that the new definition of sequent has the same axioms and satisfies the same rules of inference as the original de nition If P is a tautology the meaning of l P under the new interpretation will be there is a natural deduction proof of P We already know that the sequent calculus is complete so if this program works every tautology has a natural deduction proof The new interpretation is this we interpret F l A A as meaning there is a proof of A with premises all the sentences in F and the negations of all the sentences in A This is quite suspect because there is no special way to pick out one element of the right set in a sequent as the conclusion before we can use this definition we need to show that all the different interpretations of F l A A are equivalent We first show the following if F IA l B is valid under the new inter pretation then F B l A is valid under the new interpretation The same is true for the old interpretation and it is also possible though it takes a little more work than you might think to show that if one sequent has a proof using our sequent rules so does the other We can be sure of this though because we actually know that the valid sequents in the old sense are exactly the ones that have proofs since one sequent is valid in the old sense iff the other is valid it is also the case that one has a proof iff the other does F IA l B says There is a natural de 1uction proof of B from the premises in F and A Pictorially we have a proof of the form IA B F B l A says There is a natural deduction proof of A from the premises in F and B We can construct such a proof from the proof above IA hyp for contradiction here we copy the box from the proof above B B IB ci A contradiction by preceding box This result allows us to work only with sequents of the form F l C with exactly one conclusion In case there is more than one conclusion in a sequent we handle the additional ones by negating them and moving them across the turnstile If we want to apply a right rule to one of these negated conclusions we use the rule above to swap it with the of cial conclusion apply the rule then swap it back If there is no conclusion we convert F A l 53 to F A IIA I clearly equivalent by using the double negation elimination rule then to FA l IA So in any case we can restrict ourselves to the case with a unique conclusion which makes life easier for use when thinking about natural deduction Axioms are clearly valid F A l A is valid under our new interpretation since there is certainly a proof of A from premises which include A It might be necessary to convert a sequent of the form I AIA l C to the form F A C l A using the previous result in order to recognize an axiom l39ow we need to check the validity of the rules for the various operations All rules are presented with their conclusions having single conclusions F l A C F IA l C These sequents are equivalent by the convention indicated above so the left negation rule is already taken care of by our treatment of multiple con clusions DAI Fk A The premise F A l is equivalent to F A l IA by the discussion above This sserts the existence of a proof like this A IA This can be converted to a proof of IA from F as follows A V IA exc mid A here we copy the box from the proof above IA A gt A ii IA IA copy previous line IA gt A ii IA proof by cases DABFC DAABPC The premise asserts the existence of a proof A B C in which we suppose that there are no lines between the hypothesis A of the outer box and the box with hypothesis B any such lines could be moved inside the box with hypothesis B and repro 1uced after that box if needed outside the box and from which we construct F A B A ce B ce here copy lines between B and C from the proof above which is What the conclusion requires Fl A Fl B TlAAB The premises of this rule tell us that we have proofs A l and B l r gtm these we easily get a proof 39Tl copy first proof A copy second proof B A B by ci which is What the bottom line asks for DPFC DQPC anQkC If we have proofs th n we have a proof F pvQ C P gt C ii Q c i C2 gt C iris C proof by ases with the boxes from the two given proofs as subproofs which meets the requirements of the bottom line ran FkaQ The top line may be interpreted as either F J I Q or T Q l P so we are given either a proof p Q l or a proof T g P and from either of these we get the conclusion P V Q from the premises F by the rule of disjunction intro 1uction I P I Q P l P gt C2 By the premise we have a proof F P Q given which we can immediately draw the conclusion P gt Q from the premises F by implication intro 1uction FI PC 1 ch I P gtQlC As always this is the most exciting of our rules The first premise needs to be read F P l C by our convention for handling multiple conclusions So we are given proofs from which we construct a proof 0 I F P V IP exc mid P gt Q P Q by mp here we copy one of the boxes from above P gt C ii IP here we copy one of the boxes from above J gt C ii C proof by cases which meets the requirements of the bottom line of the rule The techniques described in this proof can be used to convert a sequent proof of a tautology to a natural de 1uction proof of a tautology It will not be an especially short or natural natural de 1uction proof though Since we know that every tautology has a sequent proof we know that every tautology has a natural de 1uction proof I I think it would be a nasty exercise to actually convert a sequent proof of any size to a natural de 1uction proof in exactly this way but I may try it in my of ce not at the board and put the result in the notes or present it in class if it turns out not to be too bad l39otice the suspiciously prominent role of proof by cases in the proofs produced by this construction Of course proofs by truth table are the ultimate example of proof by every single case to the point of exhaustion 16 Wednesday February 4 I lectured in three areas 161 Deriving rules for new logical Operations I derived the left rule for GB exclusive or and both rules for the neither nor operator l The derivation DPFQA DQPRA DR QFA n thA DWA QPA DbPAQkA DWA QVfWAQFA DPQFA justi es the rule FPlQA FQlPA DPQFA The derivation of the other rule for GB is left as an exercise as is the derivation of rules for the biconditional The rules for l are more interesting in a way because they could in theory be used as the only rules of our system since all propositional logic operations can be de ned in terms of l Of course here our derivation uses the de nition P l Q E P v Q The derivation F l P Q A F l P v Q A I IP v Q l A F P l Q l A justi es the left rule F l P Q A F P l Q l A The derivation F P l A P Q l A DPVQFA F l P v Q A F l P l Q A justi es the right rule F P l A P Q l A 1 l P l Q A These rules combine characteristics of the rules of the connectives V and on the one hand and the rule for I on the other as one might expect 162 Translating natural deduction proofs into sequent proofs the need for the cut rule I talked about translation in the other direction certain natural deduction rules when expressed in sequent form seem to require the cut rule in addition to our official sequent rules The rules which I consi 1ered were modus ponens and negation intro 1uction the derivations are given above in the Monday notes not lectured on Tuesday but I will insert them here As we saw in the completeness proof for natural deduction certain rules of natural deduction correspond precisely to rules of sequent calculus This is true for implication intro 1uction and disjunction intro 1uction for example The formalizations of the simple disjunction elimination rules in sequent notation FPPAQ rep F l P Q P I Q are clearly valid inferences in sequent calculus They go against the grain from our sequent calculus standpoint because they prove simpler conclusions from more complex hypotheses l39otice that a sequent proof of F l P Q from our rules seems to require the existence of sequent proofs of F l P and F I Q already in existence as prerequisites The sequent formulations of the full disjunction elimination rules F l J F l P v Q P I Q and rt Q FkaQ rep have the same unsatisfactory property from our sequent calculus stand point of having more complex premises than conclusions 60 In the first case the existence of sequent proofs using our rules of the premises seems to require the existence of sequent proofs of F P l and so by weakening of F P I Q and of F l P Q The second case admits of a similar analysis The formalization of the rule of modus ponens FbP FkPaQ er has the same unsatisfactory characteristic But notice that a sequent proof using our rules of the two premises seems to require a proof of F l P and so by weakening of F l P Q and a proof of F P I Q A look at the negation intro 1uction rule will give the clearest indication of what we are lacking here DAFPA P Fk A A proof tree on the premise of this reasoning has the following structure r rpk DAPP TEQT DAFPA P Fk A All of the translations of natural de 1uction reasoning given above would become valid in our system if we adopted the following rule called the cut rule FPRA DPFA FPA It is easier to understand the cut rule if we note that F l P A is valid if and only if F IP I A is valid If we can deduce something in A from F and either P or P then it certainly follows that if everything in F is true something in A is true In the negation intro 1uction example we could use cut to deduce F A l and then F l IA from the sequents at the top of the proof tree just given This rule is clearly valid But it is certainly incompatible with the phi losophy of our sequent calculus any number of extra logical operations may 61 be intro 1uce 1 in the expression P whose structure is not motivated in any way by the structure of the sequent F l A The actual situation is that the rule is useful for interpreting natural deduction rules sound but not required anything that can be proved with the cut rule can be proved without it and in fact we already know this because we know that every valid sequent can be proved using our sequent rules It is possible to transform sequent proofs using cut mechanically into sequent proofs not using cut this is technically quite interesting but beyond the level of this course 163 Quanti ers reintroduced We now of cially finish our discussion of propositional logic and commence the discussion of what is called first order logic or predicate logic in which we add quantifiers Our language changes So far we have only allowed letters as logically atomic sentences We now allow sentences of more complex forms such as Pa the object has property P Rary or H y stands in the relation R to y or even or Tux relations among three or more objects A notation like Pa stands for an atomic sentence We use the notation to represent an arbitrary complex sentence with occurrences of For example if is defined as Ra gt Sat then means Ra gt Sa This admits baroque variations Ra gt 30 also can be written where is defined as Ra gt Sa With these definitions and are the same but Pb and Qb are different the first will be H gt S while the second will be H gt Sa The notation for complex sentences extends to more arguments a sentence Pr y stands for a complex sentence involving and Q The following discussion of the quantifier rules will differ from the discus sion earlier in using the notation instead of Pa The universal quantifier elimination rule ue is very simple If we have for all Pr then we certainly have for any particular The existential quantifier intro 1uction rule ei is similarly simple 62 If we have PM this witnesses Recall from our development in propositional logic that elimination rules tell us how to use premises of a given logical form while intro 1uction rules tell us how to prove conclusions of a given logical form The other two rules are more complicated and involve boxed subproofs To prove a statement of the form for all PW the standard strategy in a mathematical proof written in English is Let a be an arbitrary object prove PM This strategy is captured by the universal quanti er intro 1uction rule ui now presented Goal 1 a a hyp for ui must be new it cannot occur in any line which can be copied into the box Goal n n1 Vazl universal quanti er intro lines 1 11 The use of equality in the hypothesis line is purely arti cial it has the harmless side effect that is provable using just ui We will introduce of cial rules for equality later The restriction on use of the variable a can be enforced in two ways we can either require that a not appear in any line which is usable inside the box it might appear in some other closed box this is our of cial rule The alternative is to restrict copying no line mentioning some other 0 outside the box may be copied into the box We digress to consider the justi cation of a form of reasoning about uni versal statements which is actually more typical Most universal reasoning in mathematics is really not of completely unrestricted generality More often we want to prove something about all objects of a certain sort say natural numbers Our goal is to prove E N The usual strategy is Let a be an arbitrary natural number Prove PM The formal proof in our system would look like this Goal E 63 Goal rewritten using the de nition of restricted quanti ers E N gt 1 a a hyp for ui must be new it cannot occur in any line which can be copied into the box Goal 0 E N gt 2 a E N hyp for ii Goal n n1 a E N gt ii lines 2 n n2 E N gt universal quanti er intro lines 1 n1 n3 E N de nition of restricted quanti er line n2 We can see that our system captures the standard style of reasoning about restricted quanti ers We could but do not of cially introduce a separate rule for a restricted universal quanti er Goal E 1 a E A hyp for restricted universal quanti er intro must be new it cannot occur in any line which can be copied into the box Goal n n1 E restricted universal quanti er intro lines 1 n For the existential quanti er it is the elimination rule ee which is more complex m n hyp for ee on line In must be new as in the ui rule ni Q Q must not include any occurrence of ni1 Q existential quanti er elimination lines m n nii This rule captures the idea that if we have an existential hypothesis we can introduce a speci c object a such that Any state ment we can prove using the existential hypothesis which does not mention the named witness is uncon 1itionally proved 64 The use of a box here is optional we could adopt the convention that we can simply introduce a witness to any existential hypothesis and keep it around permanently However we believe that the named witness in this kind of proof is just as much a locally declared object as the arbitrary object in the universal intro 1uction rule s subproof A reason for the box which is connected to the actual practice in writing mathematical proofs is that we may want the use of a letter to represent a witness to be temporary we may not want to permanently reserve a name for the witness and keeping it in a box allows us to forget the name once we have proved the results we want using it and notice that the results we want to prove will naturally not mention the temporarily named witness 164 Sequent rules for quanti ers F l Pa A T l where 0 cannot appear in F A or F PU l A T l A There are no restrictions on t here l39otice that we don t eliminate the universally quanti ed sentence it might be necessary to use more examples F l Pt A T l There are no restrictions on t here l39otice that we don t eliminate the existentially quanti ed sentence it might be necessary to use more witnesses 13mg A T l A where 0 cannot appear in F or A 17 February 6 2004 This was our rst lab session See the Lab Handout I may add some remarks at this point later 18 February 9 2004 Today we looked at our rst examples of natural de 1uction proofs in rst order logic otherwise known as predicate logic the two terms are inter changeable We proved that a relation R is re exive if it is symmetric transitive and has the property that everything has the relation R to something That is from premises 1 VarVymRy gt 2 sz gt 3 R we can prove the conclusion We regard the premises listed above as lines 1 3 of our proof We then write Goal R The form of this goal suggests that we should open a box for universal quanti er intro 1uction 66 4 a 2 a 11yp 1 01 111 5 31yaRy 110 11110 3 x a 6 11R 11yp 101 00 11110 5 G0211 b R a 10 b0 p10v011 11s111g sy1n1n011y 211111 11110 6 7 VyuRy gt yRa 110 11110 1 xa 8 11R gt 11211110 11110 7 yb 9 MM 11111 111108 68 G0211 aRa 10 b0 p10v011 by t121111t1y1tyz 11R 211111 b R 0 01112111 0 R a 10 a R JR a 01 111108 69 11 VyV aRy sz gt 110 11110 2 xa 12 Rb JR 2 gt 0 Hz 110 1111011 yb 13 11R bRa gt 01211110 1111012 za 14 1130 1111 111108 10 13 15 01211 00 11110 5 6 14 16 111 111108 4 15 0111 110xt 0x211np10 18 111010 101np10x F101n p101n1s0 Ry 3mVyAy V Ry Ry gt 110111100 1110 0011011181011 I11f011n2111y 0110050 2111 211b1t1211y 13111101 A 01 Am 12150 1 Am F01 01110 y Ry by p101n1s0 1 1V1gtW b012111s0 Am 211111 Ry W0 1121V0 y Hat by p101n1s0 3 101np101111g 1110 p100f 01 1111s 12150 12150 2 Am L01 1 W11110s 1110 1111111 01 p101n1s0 2 10 1 01 2111 y Abe H y T111115 A V b Rfli 211111 W0 k110W 111211 1110 11181 21110111211110 1008 1101 110111 80 W0 1121V0 me T1118 101np10108 1110 p100f 01 1111s 12150 19 Tuesday February 10 We went to the lab today there are no additional notes at least not at this time We will spend some time in class tomorrow talking about the test but I do intend to lecture The homework is of cially due tomorrow but I m willing to take it after the test The test is on propositional logic only no quantifiers 20 Wednesday February 11 We completed a formal proof in natural de 1uction of the example informally intro 1uce 1 at the end of the Monday lecture The proof has the interesting feature that it makes use of all four quantifier rules We construct the proof following the structure of the proof sketch given at the end of the Monday notes 1 Ry 2 Early914g v By 3 Ry gt y Goal 68 4 a 2 a 11yp for 111 Goal Egg R Strat0gy as 111 t110 proof sk0tc11 prov0 by as0s E1t110r Act or not Au 5 Au V IAa 0xc 11111 for proof by as0s Goal Au gt Snya t110 goal IAa gt Egg R W111 app0ar aft0r t110 proof of t111s goal 6 Au 11yp for 11 7 SyuRy 110 11110 1 21 a 8 MRI 11yp for 00 11110 7 9 MRI Act 01 11110s 68 10 VyaRy AC1 gt yRa 110 11110 3 x a 11 aRbAAa gt bRa110 1111010 yb 12 130 1np 11110s 911 13 Snya 01 11110 12 14 3yyRa 00 11110 7 11110s 8 13 15 Au gt Snya 11 11110s 6 14 Goal s0o11d as0 IAa gt 3yyRa 16 IAa 11yp for 11 17 VyAy V bRy 11yp for 00 11110 2 xb 18 Act V bRy 110 11110 17 y b 19 bRy 10 11110s 16 18 20 Snya 01 11110 19 b y 21 31yyRa 00 11110s 2 17 20 22 IAa gt 3yyRa 11 16 21 23 Snya proof by as0s 11110s 5 15 22 24 111 11110s 1 23 21 Friday February 13 T111s p0r1od was d0vot0d to t110 first 0xa1n 69 22 Tuesday February 17 de Morgan laws for quanti ers Informally we can think of the universal quanti er as representing a kind of conjunction and the existential quanti er as representing a kind of dis junction if the objects of our universe are a1 a2 then we can think of Vamp as meaning something like and as meaning something like Pa1 V Pa2 V If our universe is nite these expansions are literally correct But if the universe is in nite as is usually the case these expansions are merely suggestive as our formalization usually does not admit the possibility of in nitely long sentences We consider the interaction of negations with quanti ers Using the ex pansion above and recalling the de Morgan laws for propositional logic we suggest the following chain of equivalences expands to quotPa1A A A i i which by de Morgan is equivalent to quotPa1 quotPa2 A V i i i which is the expansion of This is not a proof l In class we did the proofs of the biconditional theorem ltgt which turned out to present various points of dif culty These proofs are here reprdoced for the notes We suggested at the end of class that students work out their own proofs of the other de Morgan law for quanti ers ltgt 70 Here s the formal proof that occupied most of the period Extended com ments are inserted Goal ltgt Goal 1 gt 1 hyp for ii Goal 2 IElarIP2 hyp for proof by contradiction Goal contradiction Goal to take advantage of the nega tive premise 1 3 a a hyp for ui Goal 4 IPa hyp for contradiction 5 ei line 4 ax 6 IElariIP37 ci lines 25 proof by contra 1iction lines 4 6 8 VarPr ui lines 3 7 9 Var ci lines 19 10 contra 1iction lines 2 9 11 gt ii lines 1 10 The proof of Goal 1 is noteworthy because we seem to be stymied at every turn A motto to derive from this experience is that when one is desperate one should resort to proof by contra 1iction in this proof we are repeatedly presented with goals whose form gives us no direct hint how to proceed Another point is that when one has arrived at a contradiction as a goal one should look at negative premises to give new goals whose achievement will allow us to derive a contradiction as we did above when we adopte dthe goal Goal 2 gt 1 hyp fo1 11 Go211 2 hyp fo1 111 3 IPa hyp fo1 00 11110 1 4 110 11110 2 5 Q Q 110g21t1o11 01111111121t1o11 11110s 34 6 Q IQ 00 11110s 2 3 5 7 111 11110s 2 6 8 gt 11 11110s 1 7 This is th0 p1oof W0 did 111 121ss This 1121s th0 W011d f021t1110 th21t W0 1100d to 11s0 110g21tio11 01111111121tio11 21 11110 W0 11st0d 111 th0 i11t1o to 1121t111211 d0d11ctio11 but 112110 110101 h21d to 11s0 to g0t 21 o11t121dictio11 not involving th0 Wit110ss a so W0 c2111 g0t out of th0 0xist011ti211 01111111121tio11 box Th010 is 2111oth01 W21y to do this p1oof Which do0s 11ot 11111 into this p1ob 10m T110 st11d011t Who did th0 p1oof 21t th0 bo211d s11gg0st0d 21t th0 tim0 th21t W0 could go 01th01 With 110g21tio11 i11t1od11ctio11 1st o1 With 0xist011ti211 01111111121tio11 1st 11010 W0 shoW th21t th0 oth01 1o11t0 go0s 1no10 11i01y Go211 2 gt 1 hyp fo1 11 2 IPa hyp fo1 00 11110 1 Go211 W0 Wo111d 11o11n2111y W1it0 this 1ight 21ft01 th0 hyp fo1 11 but 11010 W0 i11t1od110 th0 Wit110ss a to p10mis0 1 1st 3 hyp fo1 111 4 110 11110 3 5 IPa 01 11110s 24 6 111 11110s 3 5 7 00 11110s 1 2 6 8 gt 11 11110s 1 7 This p1oof 1121s th0 s211n0 1011gth 2111d do0s11 t 101111110 th0 W011d 1112111011V01 With 110g21tio11 01111111121tio11 1V0g21t1o11 01111111121tio11 Which 1121s th0 fo11n P i Q 72 was originally listed as one of the basic rules of natural 1e 1uction but we have never actually used it As it turns out it can be derived from the other rules so I have now moved it to the derived rules section where you can see its rather strange proof l This proof justi es the rst two of the following four derived rules and the suggested exercise for tomorrow justi es the other two de Morgan rules for quanti ers 1 2 3 4 23 February 18 2004 Today we proved the exercise from yesterday ltgt and a new result 231 rst proof Goal ltgt Goal 1 gt 1 11ypf0111 Goal 2 a 2 a 11yp for 111 Goal IPa 3 11yp for 111 4 01 11110 3 ax 5 00 111108 14 6 IPa 111 111105 3 5 7 gt 11 111105 1 8 Goal 2 gt 9 11yp fgt111 Goal 10 11yp for 111 11 11yp for 00 11110 10 12 IPa 110 111109 xa 13 Q IQ 110 111108 1112 14 Q IQ 00 111108 10 11 13 15 111 111105 10 14 16 gt 11 111108 9 15 17 ltgt b1 111108 817 This proof 11001s 1110 110ga11011 0111111112111011 trick and 11 021111101 b0 av01d0d 11010 by changing 1110 01101 111 which b01108 2110 0p0110d 111 111108 2 6 00 232 second proof Goal V ltgt V Goal 1 V gt V 1 V 11yp for11 Goal V 2 11yp for 11 3 V 11yp for 00 11110 1 Xa 4 1111q 11110 2 5 IPa 110 11110 4 6 10 111108 35 7 01 11110 6 ax 8 00 111108 13 7 9 V 11 111108 2 8 10 V gt V 111108 1 10 Goal 2 V gt V 11 31771 V 11yp for11 Goal V Goal 1 proof by 021808 gt V 12 11yp for11 13 11yp for 00 11110 12 14 V 811 11110 13 16 V 01 11110 13 ax 16 V 00 111108 12 13 16 17 gt V 11 111108 12 16 Goal 2 proof by 021808 gt V 18 11yp for11 19 11yp for 00 11110 18 20 V 811 11110 19 21 V 01 11110 20 ax 22 V 00 111108 18 19 21 23 gt V 11 111108 18 22 24 February 20 2004 T1118 117218 a lab lay W0 111tro11101 1111prov01n011t8 to 1110 prov0r mo8t1y 111 r0adab1111y and 8tart0d working with q11a1111 0r8 25 February 23 2004 We did a natural de 1uction proof of SHAW gt B gt VarAar gt B We also did a sequent proof of gt 251 rst proof There is a hazard in this proof it is important to read the hypothesis cor rectly as gt B instead of gt B This is one of the reasons it is important to keep track of parentheses Goal gt B gt gt B 1 gt B hyp for ii Goal gt B 2 hyp for ii Gal B 3 gt B hyp for ee line 1 4 ue line 2 5 B mp lines 43 6 B ee lines 13 5 7 gt B ii lines 2 6 8 gt B gt gt B ii 1 7 It is important in this proof that B does not contain any occurrences of This means that it is unchanged in line 3 from line 1 and that it can be exported from the existential elimination box 252 second proof 26 February 24 2004 A second lab day on quanti cation 27 February 27 2004 The example started Tuesday and completed today by Mr Ricker follows gt premise VmVyV Qar y Qy gt Sar premise V premise IRy gt Sar premise E gt ElySy premise Goal ElaElbSa 1 Proof sketch Either there is an such that or not This de nes two cases Case 1 In this case there is a y such that S y y and we are done with y a and y b in the conclusion Case 2 Once again we consider two cases either or IElarIR2 Case 2a Choose an object 6 such that Rc Let d be chosen so that IRd By premise D we have S c d and we are done Case 2b I laIR27 By premise C this implies which by premise A implies c Vyrazmwm Let be any object By there is a y such that Qary by another application of there is 2 such that Qyz and by premise B we have S completing the proof It is important to observe that the structure of our natural de 1uction proof is basically the same as that of the proof sketch but much more explicit We now begin the main body of the formal proof 1 V exc mid Goal gt Sla3lbSa for proof by cases A B C D K K 2 11yp for11 3 3ySyy 1111 11110s 1532 4 S c c 11yp for 00 11110 3 5 31136 1 01 11110 4 6 31a31JSa 01 11110 3 7 31a 303a 00 11110 3 11110s 4 6 09 0 1 gt 3a311Sa 11 11110s 1 7 211 gt 31061130 for proof by as0s 9 11yp for11 Goal 31a3111Sa 10 V I31mIR27 0xc 11111 Goal gt 31a3111Sa for proof by as0s 11 11yp for11 Goal 31061130 12 Rc 11yp for 00 11110 9 13 IRd 11yp for 00 11110 11 14 wide A 0 gt 30 g 110 11110 D 15 RC IRd gt Scd 110 11110 14 16 Rc IRd 1 11110s 1213 17 Scd 1111 11110s 1516 18 3030 1 01 1111017 19 31a31JSa 01 1111018 20 31a31JSa 00 11110s 11 13 19 21 31a31JSa 00 11110s 9 12 20 22 gt 31a31JSa 11 11110s 11 21 T110 box do0s 11ot 10211131 1os0 11010 this is just a page b10a1lt1 Goal IElaIR27 gt Sla3lbSab for proof by cases 23 IElarIR27 l1yp for ii 24 VarIIR27 dmq line 23 Goal taken from the proof sketch 25 a 2 a l1yp for 11i Goal 26 V IRa 11e line C 27 IIRa 11e line 24 28 1e lines 2627 29 11i lines 26 28 30 mp A29 comment notice that the c intro 111ce 1 in the fol lowing line is not a Witness it is a completely arbitrary object 31 32Qc 11e line 30 32 Qc d l1yp for ee line 31 33 SzQM 11e line 30 QM e l1yp for ee line 33 35 QcdQd e ci lines 3234 36 myanew cm gt Sc 11e line B 37 VzQc d QM gt Sc 11e line 36 38 Qc d Qde gt Sc e 11e line 37 39 Sce mp lines 35 38 40 303c 1 ei line 39 41 Sla lbSa ei line 40 42 Sla lbSa ee 3334 41 43 3a lbSa ee 3132 42 44 IElaIR2 gt Sla lbSa ii lines 23 43 45 Sla3lbSa proof by cases lines 10 22 44 46 gt Sla lbSa ii lines 9 45 47 Sla3lbSa proof by cases lines 1846 79 28 March 1 2004 substitution and equality 281 Substitution It is necessary to be careful about the de nition of substitution in the pres ence of dummmy variables such as the in Actually you are already familiar with similar notational issues in calculus Consider the integral t2 dt 37247 132m This might be said to mean the same thing as 1 We would say that it does but that variables are being abused the in the bound means something quite different from the variable of integration This means the same thing as l39ow consider Consider the more complex integral 117 f t2 dt 1 which evaluates to t3 11 lg 39l39 477th If we replace t with here naively we get a genuine mathematical error at 2 f 1 evaluates to 3 which is de nitely different from the previous expression We indicate how we de ne substitution where P is any sentence of our logic and a is a term which is to replace the variable is the result of replacing with a in P The de nition is by recursion on the structure of sentences For an atomic sentence Pan mn we de ne as a when and otherwise then de ne Pan as For a negation IP we de ne as For a conjunction P Q we de ne P as The cases of the other binary propositional operations look just the same So far we have given a fancy de nition of the naive idea replace with a wherever it appears We can t do this with quanti ers and preserve meaning We give an example asserts that every object is equal to a is the only object 11 should be b and indeed this asserts that b is the only object might be thought to be from a naive standpoint but notice that the statement no longer says that is the only object it says that every object is equal to itself We can avoid this problem by renaming the bound variable Vyy is certainly equivalent to and Vyy may be taken to be Vyy which does have the meaning that is the only object Our de nition of substitution into quanti ed expressions errs on the side of caution and always renames the bound variable to a brand new variable whenever a substitution is made WWWy W Pl xllayl where 2 is a variable which does not appear in P or in a can t be 2 not can it be a complex name containing 2 as a component which can happen in applications The substitution of 2 for is carried out before the substitution of a for the variable y Examples l39otice that replacing with a in this expression actually doesn t change its meaning at all this should not be surprising since there isn t really any speci c object named that is talking about 81 l39otice that this does the right thing 1 It s nice to check that it works out sensibly in a nice case too Of course we will not usually change the dummy variable when we don t need to The computer program does because it is easier to do it all the time than to perform the checks required to see if the substitution is dangerous Our quanti er rules could be rewritten to take advantage of more pre cise substitution notation For example universal elimination allows us to deduce from Var here P may be any sentence and may actually include Existential intro 1uction allows us to deduce from P actually it s better to say that it allows us to deduce from y this allows us to talk about the deduction of from a a the expression a a is y while the expression Elf is l39otice that would just be and while we can validly infer from a a by existential intro 1uction it s not the only thing we can infer We will not usually be so precise we will normally stick with our conven tion that stands for an expression containing and replacing with a in this expression will give us 282 Equality In this lecture I intro 1uce 1 sequent rules for equality l a a and a bal lbmla Qlarl Rlbarla Slaml a baplaarlanb Rlamlaslbarl an equation to the left of the turnstile allows substitutions to be made freely in both directions everywhere in the sequent 82 are a suf cient set of rules but I don t like them very much The main reason I don t like them is that they introduce axioms l a a which don t have the uniform form which all axioms of sequent calculus have so far In the notes for Tuesday I will include the current computer proofs for basic properties of equality the prover de nes equality in terms of set theory in a way you can examine there I brie y discuss another way of handling equality which is actually closely related to the way the computer handles it which involves a powerful exten sion of our logic If we allow quanti ers over predicate letters P we can de ne a b as VPJ M ltgt Pb two objects are equal if they have the same properties l39otice that the new quanti ers quantify not only over atomic predicates but over complex predicates any sentence containing however complex The rules for secon 1 or 1er quanti ers are exactly analogous to those for rst order quanti ers I give the rst few steps of a couple of proofs l VPPa ltgt l a a We can see that the top line is a propositional tautology so we leave the rest of the proof for you The letter P1 stands for a new property intro 1uce 1 to handle a universal quantifier on the right a a ltgt b a l b a a b l b a l a b gt b a What I did at the last step working from the bottom up was to instan tiate the universally quanti ed P on the left with the property de ned by z a The top formula will be provable by propositional methods as long as a a is provable and we have indicated how to prove this We aren t really going to do secon 1 or 1er logic it s quite similar to set theory which is more familiar to you and is built into the computer prover 29 March 2 2004 This was another lab day 83 this is the computer proof for reflexivity of equality The prover defines equality as the property of belonging to the same sets E is the membership relation Line 1 Proved 1 Ax1x1 x1 by 2 Line 2 Proved 1 a1 a1 by 3 Line 3 Proved 1 AX2a1 E X2 a1 E X2 by 4 84 Line 4 Proved 1 a1 E a2 a1 E a2 by 5 Line 5 Proved 1 a1 E a2 gt a1 E a2 amp a1 E a2 gt a1 E a2 by 7 6 Line 7 Proved 1 a1 E a2 gt a1 E a2 by 9 Line 9 Proved 1 a1 E a2 1 a1 E a2 Line 6 Proved 1 a1 E a2 gt a1 E a2 by 8 Line 8 Proved 1 a1 E a2 1 a1 E a2 Here is the computer proof of symmetry of equality It gives more of an idea of how the set theory machinery in the prover works The prover does not allow just any set to be constructed Russell s paradox is avoided Line 1 Proved 86 1 Ax1Ax2x1 x2 gt x2 x1 by 2 Line 2 Proved 1 Ax3a1 x3 gt x3 a1 by 3 Line 3 Proved 1 a1 a2 gt a2 a1 by 4 Line 4 Proved 1 a1 a2 1 a2 a1 by 5 Line 5 Proved 1 Ax4a1 E x4 a2 E x4 by 6 Line 6 Proved 1 a1 E x1lx1 a1 a2 E x1lx1 a1 2 Ax4a1 E x4 a2 E x4 1 a2 a1 by 7 Line 7 Proved 1 a1 E x1lx1 a1 gt a2 E x1lx1 a1 amp a2 E x1lx1 a1 gt a1 E x1lx1 a1 2 Ax4a1 E x4 a2 E x4 88 by 8 Line 8 Proved 1 a1 E x1lx1 a1 gt a2 E x1lx1 a1 2 a2 E x1lx1 a1 gt a1 E x1lx1 a1 3 Ax4a1 E x4 a2 E x4 1 a2 a1 by 10 9 Line 10 Proved 1 a2 E X1lx1 a1 2 a2 E x1lx1 a1 gt a1 E x1lx1 a1 3 Ax4a1 E x4 a2 E x4 1 a2 a1 by 19 Line 19 Proved 1 a2 a1 2 a2 E X1lx1 a1 gt a1 E X1lx1 a1 3 AX4a1 E X4 a2 E X4 89 Line 9 1 a2 E 2 Ax4 1 a1 E 2 a2 by 11 Line 11 1 a2 E 2 Ax4 1 a1 2 a2 by 12 Line 12 1 a2 E a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 a1 E x4 a2 E x4 x1lx1 a1 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 E x4 a2 E x4 a1 a1 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 90 a1 E x4 a2 E x4 a1 E x5 a1 E x5 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 a1 E x4 a2 E x4 a3 a1 E a3 a1 Proved x1lx1 a1 gt a1 E x1lx1 a1 E x4 a2 E x4 a1 a1 E a3 gt a1 E a3 amp a1 E a3 2 Ax4 1 AXE 2 a2 by 13 Line 13 1 a2 E 2 Ax4 1 a1 E 2 a2 by 14 Line 14 1 a2 E 2 Ax4 1 gt 2 a2 a1 E a3 a1 91 by 16 15 Line 16 Proved 1 a2 E x1lx1 a1 gt a1 E x1lx1 a1 2 Ax4a1 E x4 a2 E x4 E a3 gt a1 E a3 a1 by 18 Line 18 Proved 1 a1 E a3 2 a2 E X1lx1 a1 gt a1 E X1lx1 a1 3 Ax4a1 E x4 a2 E x4 1 a1 E a3 2 a2 a1 Line 15 Proved 1 a2 E X1lx1 a1 gt a1 E X1lx1 a1 2 Ax4a1 E X4 a2 E X4 92 1 a1 E a3 gt a1 E a3 2 a2 a1 by 17 Line 17 Proved 1 a1 E a3 2 a2 E xllxl a1 gt a1 E xllxl a1 3 Ax4a1 E x4 a2 E x4 a3 a1 quot11 30 March 3 2004 301 Equality rules for natural deduction The new rules for equality are as usual an intro 1uction rule and an elimi nation rule Equality intro 1uction eq i is 020 This is actually provable but for arti cial reasons having to do with the use of a a as a dummy sentence about a in the rule of universal quanti er intro 1uction Goal 0 a Goal then use ue 1 a 2 a hyp for u i Goal 0 a 2 a a copy line 1 93 3 2 ii lines 1 2 4 a 2 a ue line 3 The rule of equality elimination can be written or more technically a 2 b The use of substitution notation makes it easier to express the idea that not all occurrences of a need to be replaced by b We prove the symmetry property of equality in natural deduction Goal 2 y gt y 2 1 a 2 a hyp for ui Goal Vyu 2 y gt y 2 2 b 2 b hyp for ui Gal a2b gtb2a 3 a 2 b hyp for ii 4 a 2 0 eq i 5 b 2 0 eq e lines 34 use line 3 to replace the rst occurrence of a in line 4 with b 6 a 2 b gt b 2 0 ii lines 3 5 7 Vyu 2 y gt y 2 ui lines 2 6 8 2 y gt y 2 ui lines 1 7 We suggest proving the transitive property of equality as an exercise A further adventure would be to try to prove the transitive property on the computer 302 Numerical quanti ers We show how to de ne 3Pm which means there is exactly one such that PW we can do this as soon as we have equality 3Par ltgt VyPy gt y 2 94 In words what this says is that there is an such that and moreover any y such that Py is actually equal to This can be done for any natural number For example we de ne meaning there are precisely two such that PW ltgt Py g y gt z V c De ning 3 for all natural numbers n in this way would lead to rather long expressions but there s a more ef cient way to do it De ne as If is de ned de ne Eln1mPar as ElmParElnyl y Ay The expressions de ned in this way will get larger linearly in the size of u If you were really ambitious you could try the following project prove the predicate logic version of 22 4 which is the following theorem 32Pm gt V 303 Completeness of sequent calculus The main result of this section is that every valid sequent of predicate logic is provable For the purposes of this section we extend our system with the cut rule but it is actually true if we don t use the cut rule as well it is harder to prove though This cut elimination result is beyond the scope of this course We use the language of our computer implementation which has an in nite supply of dummy variables and an in nite supply of names for objects The set of all expressions in our language is countably in nite we can place it in one to one correspon 1ence with the natural numbers by listing expressions in order of increasing length with expressions of the same length listed in alphabetical order determined by ASCII order on characters for example Fix such an order and let E be the expression correspon 1ing to the natural number 1 Our strategy is to show that any unprovable sequent is invalid Let F l A bean unprovable sequent we will construct an interpretation of the predicate and relation symbols appearing in the sequent under which all sentences in 95 F are true and all sentences in A are false establishing that the original sequent is invalid We construct a sequence of sequents ouch F l A de ned recursively I l A0 is de ned as F l A Note that this is by hypothesis an unprovable sequent Suppose that F l A has been de ned and is an unprovable sequent We de ne I l as the sequent F F l A unless this is provable in which case we de ne it as F l FA if both sequents wer provable we could prove F l A using the cut rule TH l A1 is de ned as I l A except in two special cases if F and I l FF l A then T l A1 is de ned as F F PM I A where a is the rst name that does not appear in I l If F and I l F I F A then we de ne F l A1 as F I F Paj A where a is once again the rst name that does not appear in I l T he sequent F l A1 will be unprovable even with the addition of the Paj s since if it were provable with them added it would also be provable without them since they can be intro 1uce 1 by applying the rule for the existential on the left or universal on the right to F So we succeed in constructing a sequence of unprovable sequents F l A De ne FCC as the union of all the sets F and ACC as the union of all the sets Since all sentences are included in the list of F s every sentence appears in either FCC or Ax If any sentence appeared in both lists the sequents F l A would be axioms for all large enough i We claim that the sentences in FCC can be understood to be the true sentences of a model and the sentences in ACC can be understood to be the false sentences of a model The elements of the model will be the names An atomic sentence Pa1 will be said to be true if Pa1 6 FCC We need to show that propositional operators and quanti ers behave correctly For any formula P 6 FCC IP cannot be in FCC because this would mean that any F l A with large enough index would be of the form I P J l A and so would be provable Similarly for any formula P g FCC and so in Am we must have IP in FCC to avoid having any F l A with large enough index being of the form F l P J A and so provable So negation behaves exactly as we expect the negation of a true statement is false and vice versa 96 For any formulas P and Q we claim that P Q is in FCC if and only if both P and Q are in FCC Suppose P and Q are in FCC if P Q were in Am then any I l A with large enough index would be of the form any I P Q l P Q A and so provable l39ow suppose that P Q is in FCC if either P or Q is in Am we get any I l A with large enough index being of the form I P Q l P A or I P Q I Q Ag and either of these would be provable The arguments for the other propositional connectives are similar more over we have de ned the other connectives in terms of and I and derived the rules for the other connectives from the rules for negation and conjunction in our of cial development of sequent calculus so we are actually safe l39ow we look at the quanti ers We need to show that is in FCC if and only if every is in FCC to show that has the correct meaning Suppose that VarP is in FCC and there is some in Ax then every T l A with large enough index will be of the form I l Pa1 A and this would be provable which is impossible If is not in FCC it must be in Am and when it was put into Ax some Paj was put there by the construction So the universal quanti er works correctly We need to show that is in FCC if and only if some is in FCC Suppose is in FCC the construction tells us that some Paj was put into FCC Suppose that is not in FCC and nonetheless some is in FCC every I l A with large enough index will be of the form I l A which is provable which is impossible It follows that the meaning of the existential quanti er is correct This completes the proof that any unprovable sequent is invalid so any valid sequent is provable predicate logic equivalently rst order logic is complete We summarize some further results machines can nd proofs A computer program can be written which will nd a proof of any sequent given to it which has a proof in theory because in general it will be extremely slow so slow as to be useless Programs can be written which are fairly good at nding proofs of some kinds of sequents machines cannot decide provability Acomputer program cannot be writ ten which decides whether a sequent is provable or not Any program of 97 this kind will say Yes to all sequents with proofs it can be programmed to find the proof eventually No to some sequents without proofs and end up looking for proofs forever for some unprovable sequents any rst order theory has a countably in nite model Notice that the model we constructed here is countably infinite it is made up of names This is odd because we can formalize a set theory in which we can prove that the set of real numbers is uncountable inside first order logic this means that this theory has a countable model The solution to the apparent paradox is that the reals in the countable model are not all the reals Outside the model we can see that the reals of the model can be indexed by natural numbers inside the model this indexing is not found among the functions of the model in nite theories are no problem If we have an infinite collection of premises with the property that no finite subcollection of the premises leads to contradiction we can adapt the proof given here to build a model in which all of the premises in the infinite collection are true The way to do this is to add a condition to the construction to put F on the right if it is a premise from the infinite collection This also leads to curious results The collection of premises consisting of the axioms of the natural numbers and the extra premises t gt 1 t gt 2 t gt 3 and so on through every natural number has these properties so we can build a model of the theory of the natural numbers which contains an object t which is larger than each of the real natural numbers equality can be added All the results we have stated also hold for predi cate logic with equality we have avoided the technical details of show ing that this is true 31 March 5 2004 Arithmetic Made Dif cult We move into the transition from logic to discrete math by considering the simplest discrete math structure the set of natural numbers with rigorous attention to the logical structure of our reasoning For the first time we allow terms names for objects more complicated than variables 98 We introduce a new term 0 For any term we allow ar as a term this is read the successor of a and means the same thing as 1 we will prove this once we have de ned For any terms and y we allow y and y as terms The in y can be omitted unless and y are both strings of digits We de ne 1 as 0 We de ne 2 as 1 We de ne 3 as 2 We de ne 4 as 3 We de ne 5 as 4 We de ne 6 as 5 We de ne 7 as 6 We de ne 8 as 7 We de ne 9 as 8 We de ne 10 as 9 The symbols 0123456789 are called digits For any string of digits D and digit d we de ne Dd as 10 D d This precisely de nes the usual decimal notation for natural numbers and also explains our convention for allowing omission of We de ne 2 y as 17 2 y Successor has the highest prece 1ence followed by multiplication followed by addition In the axioms I use everywhere though all the occurrences in the axioms can actually be omitted The axioms of Peano arithmetic are axiom 1 2 0 axiom 2 VarVyar 2 y gt 2 axiom 3 0 2 axiom 4 VmVyar y 2 a y axiom 5 Varm 0 2 0 axiom 6 y 2 y Peano arithmetic has a single additional rule used for proving universally quanti ed sentences It is the familiar rule of mathematical induction which can be presented without boxes in the form P0 VkPk gt Pk V71P7l or with boxes in the form Goal Warm Goal basis step P0 99 m P0 m1 Pk induction hypothesis 1 must be a new vari able not appearing in any line we are allowed to copy into this box n POW n1 induction lines m m1 n You may use either form of the rule in your proofs You also may use k 1 instead of k as is justified by the following theorem Theorem 1 2 1 a 2 a hyp for ui Goal 0 1 2 a 2 a0 2 a0 n1ue 4 mue means multiple universal elimination this would expand out into two applications of ue 3 a 1 2 0 de nition of 1 line 2 4 a 0 2 a ue 3 5 a 1 2 0 eq e or substitution lines 43 6 1 2 ui lines 1 5 The axioms may be regarded as lines accessible in every proof the style of reference shown here is adequate You will have the list of axioms and of cial definitions available at a test We now do our first induction proof which is a very strange one Theorem Every number other than 0 has a pre 1ecessor 2 0 gt 399 97 Goal basis step 0 2 0 gt Slyy 2 0 Comment This is vacuously true because the hypothesis is absurd The use of negation elimination in the proof is a standard way to deal with this 1 0 2 0 hyp for ui 2 20 2 0 de nition of 2 line 1 3 0 2 0 eq i 4 Elyy 2 0 neg elim lines 23 5 0 2 0 gt Slyy 2 0 ii lines 1 4 Goal induction step 2 0 gt Slyy 2 gt k 2 0 gt Slyy 2 k Comment this is also vacuously true because the conclusion Slyy 2 k 100 is true for reasons that have nothing to do with the hypotheses 6 a 2 a hyp for ui Goal 2 0 gt Elyy 2 gt a 2 0 gt Elyy 2 7 2 0 gt Elyy 2 hyp for 11 Goal a 2 0 gt Elyy 2 8 a 2 0 hyp for 11 Goal Elyy 2 a 9 a 2 0 eq 1 10 Elyy 2 a ei line 9 it isn t neces sary to replace every 0 with y 11 a 2 0 gt Slyy 2 11 lines 8 10 12 2 0 gt Elyy 2 gt a 2 0 gt Slyy 2 11 lines 7 11 13 2 0 gt Elyy 2 gt k 2 0 gt Slyy 2 ui lines 6 12 14 2 0 gt Elyy 2 induction lines 5 13 I suggest attempting two theorems 2 2 2 4 for un 1erstanding the axioms and Vm0m 2 0 an induction proof If you prove Vm0 2 ar 0 you are ready to try y 2 y the commutative property of addition It is important to note that our formulation of the axioms assumes that everything in the universe is a natural number If we were also talking about other kinds of objects we would need to restrict the quantifiers in our axioms to natural numbers 32 Monday March 8 2004 commutativity of addition Today we proved the theorem WWW y y 07 in class unfortunately the proof I gave was wrong I think I must have been asleep on my feet The main induction step needs something additional We adopted the derived rule symmetry of equality 101 a b b a This is justified by instantiating the theorem y gt y and modus ponens There are so many symmetry of equality lines in the proofs below that I think I will allow a line a b to be used either to substitute a for b or to substitute 1 for a in another line This is an example of the strategy to pursue in arithmetic basically we have one additional proof tool induction for proving universal sentences plus a few computational facts expressed in the axioms Using induction breaks the theorem down into two goals Basis 1 V90 y y 0 and Induction Step 1 VkVyk y y k gt V915 y y k We prove the basis first and prove the induction step below The reason for the number 1 will become evident shortly Goal Basis 1 Vy0 y y 0 This is also to be proved by induction We have no way to deal with addition of anything on the left in the axioms so there is no other possible approach Goal Basis 2 0 0 0 0 1 0 0 0 0 equality introduction Goal Induction Step 2 Vk k k 0 gt 0 k k 0 102 G 2 020 hyp for ui al 0aa0 gt0a a 0 3 0aa0 hyp for ii Goal 0 a a 0 Calculation Sketch 0 a ax 4 0 a ind hypa 0 ax 3 a 0 4 0 a 0 a mue 4 45 0 a 0 subst into 4 using 3 this corrects an error I found in the notes on the 9th I left out the use of ind hyp a 0 a ue ax 3 0 a 0 eq e or subst lines 545 0 0 a ue 3 a a 0 symmetry of equality line 7 0 a a 0 subst 86 00512239 9 10 0aa0 gt0a a 0ii lines4 9 11 Vk k k 0 gt 0 k k 0 ui lines 2 10 12 V90 y 2 y 0 induction 111 Goal Induction Step 1 VkVyk y y k gt Vyk y y k The proof I gave for Induction Step 1 in class was wrong I give the correct proof here and point out the needed extra ingredient 13 a 2 a hyp for ii Goal Vyu y y gt Vyu y y a 14 Vyu y y Goal Vyu y y a 15 b b hyp for ui Goal 0 b 2 1 0 Calculation Sketch b a ax 4 b a ind hyp a b 2 why not ax 4 exactly a b Comment to get a proof along these lines we need the result y 2 ar y Unfortunately this missing step requires a full induction proof We close up this proof for the moment and prove this theorem This is a separate proof so it has its own line numbers when we start up again with 103 the other proof we will resume its numbering scheme 104 I m setting this proof up using the box form of the induction rule Goal y 2 37 y 1 a2a hyp for ui Goal y 2 a y Goal basis 0 2 a 0 a0 2 a ue 3 a 0 2 a ue ax 3 a 2 a 0 symm 2 line 3 a 2 a 0 symm 2 line 2 a 0 2 a 0 subst lines 54 7 k 2 a k induction hypothesis Goal k 2 a k Calculation sketch 0 k 2 ax 4 a k 2 ind hyp k 2 ax 4 and substitution a k 8 a k 2 a k mue 4 9 a k 2 k symm 2 line 7 10 a k 2 k subst 98 11 a k 2 k mue ax 4 12 k 2 a k symm 2 line 11 13 a k 2 k subst 1210 14 k 2 a k symm 2 line 13 999 15 y 2 a y induction box form line 6 lines 8 14 16 y 2 37 y We refer to the theorem just proved as Lemma 1 We now resume the proof of the main theorem repeating from the be ginning of Induction Step 1 Goal Induction Step 1 VkVyk y 2 y k gt Vyk y 2 y k The proof I gave for Induction Step 1 in class was wrong I give the correct proof here and point out the needed extra ingredient 105 13 a 2 a 11yp 13901 11 G0a1 Vyu y 2 y gt Vyu y 2 y a 14 Vyu y y G0a1 Vyu y 2 y a 15 b 2 b 11yp 13901 111 G0a1 a b 2 1 0 Ca10111a11011 31101011 I a 2 ax 4 b a 2 11111 11yp b 2 L0mma 1 a b 16 1 0 2 b a m110 4 17 a b 2 b a 110 11110 14 18 10 2 11 symm011y 0f 01111a111y 11110 19 1 0 2 b subst 111108 1816 20 b 2 a b m110 L0mma 1 21 1 0 2 a b subst 20 19 22 a b 2 b a symm 2 11110 21 23 Vyu y 2 y a 111 111108 15 22 24 Vyu y 2 y gt Vyu y 2 y a 11 111108 14 23 25 VkVyk y 2 y k gt Vyk y 2 y k 111 111101 13 24 26 y 2 y 1111111011011 11110 12 25 S11gg01011 0x01018015 My 10 p10v0 y 2 y 1111111011011 011 y 01 2 m1g111 b0 b01101 111a11 1111111011011 011 111011g11 I 11111111 a11y W111 W01k Y011 m1g111 110011 L0mma 1 W0 0a11 110 1111111011011 011 y b00a11s0 y 2 y 1s 011111va10111 10 2 Y011 m1g111 11y p10v111g VarVyPar 1gt VyVarPar w111011 j11s11 0 1111s ma11011v01 T1y 2 33 March 9 2004 T011ay W0 10 11111 1110 p100f 0139 1110 ma111 1111111011011 8101 0139 1110 p100f 0f 00m m111a11v11y 0f a1111111011 11101111fy111g a1111 0011001111g my 01101 0139 y010111ay I a1111011110011 11111010111 s1y10 101111110m0111s 101 1180 0139 01111a111y 111108 than I 11111 y010111ayz 1110 11110 0139 equality elimination 01 substitution may b0 118011 106 in either of the forms I b a PM 1 b This minimizes the need for explicit applications of symmetry of equality But I do require that appeals to substitution be of the form substitution into line In using line n vhere line In is P and line 11 is a b or b a The new version of the proof will conform to these style requirements so it will have fewer explicit applications of symmetry of equality and it will also use the box version of the induction rule rather than the line version which will reduce the number of boxes created I prove Lemma 1 rst Goal y 2 37 y 1 a2a hyp for ui Goal y 2 a y Goal basis 0 2 a 0 2 a 0 2 a ue 3 3 a 0 2 a ue ax 3 4 a 0 2 0 subst into 3 using 2 5 0 2 a 0 symm 2 line 4 6 k 2 a k induction hypothesis Goal k 2 a k Calculation sketch 0 k 2 ax 4 a k 2 ind hyp k 2 ax 4 and substitution a k 7 a k 2 a k mue 4 8 a k 2 k subst into 7 using 6 9 a k 2 k mue ax 4 10 a k 2 k subst into 8 using 9 11 k 2 a k symm 2 line 10 12 y 2 a y induction box form line 5 lines 6 11 13 y 37 y ui lines 1 12 We will refer to this theorem as Lemma 1 and restart the numbering in the main proof which now follows Main Goal VarVyar y 2 y Goal Basis 1 Vy0 y 2 y 0 This is also to be proved by induction We have no way to deal with addition of anything on the left in the axioms so there is no other possible approach Goal Basis 2 0 0 2 0 0 1 0 0 2 0 0 equality intro 1uction 108 2 0 a a 0 inductive hypothesis Goal 0 a a 0 Calculation Sketch 0 a 4 0 a ind hypa 0 ax 3 twice a 0 0 a 0 a mue ax 4 0 a 0 subst into 3 using 2 a 0 a ue 3 0 a a subst into 4 using 5 a 0 a ue 3 0 a a 0 subst into 6 using 7 90513999 CO V90 y y 0 induction box form line 1 lines 2 8 10 Vyu y y induction hypothesis Goal Vyu y y a 11 b b hyp for ui Goal 0 b b 0 Calculation Sketch b a ax 4 b a ind hyp b 2 Lemma 1 a b b a b a mue ax 4 13 a b b a ue line 10 14 b a b subst into 12 using 13 15 b a b mue Lemma 1 16 b a a b subst into 14 using 15 17 a b b a symm 2 line 16 18 Vya y y a ui lines 11 17 5 19 y y induction box form line 9 lines 10 18 c that our new conventions make the proof signi cantly shorter and I think easier to read Tell me what you think Also I found an error in the proof of the basis step in the March 8 notes a step was left out this is corrected here and in the March 8 notes Please tell me if you notice any errors in the notes by the way extra credit points will be added to your homework average for proofreading contributions Just for fun I include the calculation justifying 2 2 4 that we did in class 22 definition of 2 109 21 axiom 6 2 1 2 2 de nition of 2 2 gt1 1 1 axiom 4 2 1 1 2 de nition of 1 2 gt1 1 0 axiom 4 2 1 0 axiom 3 2 1 2 de nition of 1 2 0 axiom 6 2 gt1 0 2 axiom 3 0 2 commutativity of addition this is a onsi 1erable shortcut 2 0 axiom 3 110 de nition of 3 3 de nition of 4 Isn t that nice For further work I suggest associativity of addition andor distributiv ity of addition over multiplication There s no need to change the order of quanti ers to do induction over different quanti ers just use the universal intro 1uction rule on the outer quanti ers and use induction on the vari able you want when you get to it I think that induction on any variable will work with associativity of addition but a is probably best I haven t thought about the other theorem yet 34 March 10 2004 The class produced a complete proof of the associative law of addition Goal VarVyV y y We will prove this by induction on 111 1 a 2 a hyp for ui Goal y y 3 4 5 6 7 2 b 2 b hyp for ui Goal b b Now we use induction Goal basis step a b 0 b 0 ab0 ab0 eq i 1 0 b ue ax 3 a b 0 a b subst into 3 using 4 ctHI 0 2 n1 ue ax 3 a b 0 b 0 subst into 5 using 6 8 a b k b k ind hyp Goal 0 b k b k Calculation sketch abk 4a b k ax 4 b k ind hypa b k ax 4a b k 9 a b k a b k eqi 10 1 k b k mue 6 11 a b k a b k subst into 9 using 10 12 a b k b k mue ax 6 13 wk 11k b k s11bst into line 12 using line 8 ind hyp 14 b k b k mue ax 6 15 a b k b k subst into 14 using 13 16 Van139 11 2 v b induction 7 8 15 17 y 2 v y ui lines 2 17 18 y y ui lines 1 18 35 Friday March 12 I proved in class today This is used in proving a b b a you also might want to prove Varl 112 Goal We will prove this by induction on This won t be identical to the proof I did in class but in general terms the strategy is the same 113 1 a a hyp for ui Goal 2 1 2 1 hyp for ui Goal 1 12 we prove this by induction Goal 10 a0 10 a 10 0 ue ax 5 0 0 0 ue ax 3 a 10 0 0 subst into 3 using 4 a0 0 ue ax 10 0 ue ax a 10 a0 0 subst into 5 using 6 a 10 a0 10 subst into 8 using 7 039 0 99905193955 9b 1k 0k 1k ind hyp Goal 1k ak 1k Calculation sketch a1k ax 6 wk 1ka1 ind hyp ak1ka1 2 many grouping steps 1k1 6 ak 1k l39otice below how many steps it takes to handle the grouping 10 a1k 2 wk 1k wk 1 mue ax 6 11 1k 11 1 subst into 10 using 9b 12 ak1ka1 ak1ka1 mue assoc 13 1k 11 1 subst into 11 using 12 14 ak 1k 11 a mue assoc 15 1k 1k 1 subst into line 13 using line 14 16 11 a a 1k mue comm 17 1k 1 subst into 15 using 16 This is just a page break the boxes are really still open 114 18 bk 2 bk mue assoc 19 bk bk b subst into 17 using 18 20 aka bkb akabkb mue assoc 21 bk bk b subst into line 19 using line 20 22 ak ak a mue ax 6 23 bk 2 bk b mue ax 6 24 bk ak bk b subst into line 21 using line 22 25 bk ak bk subst into line 24 using line 23 26 b be induction 9 9b 25 27 ui 2 26 28 ui 1 17 36 March 15 2004 set theory prerequisites for counting Today I lectured on set theory background which I will assume The notation E y means a is an element of y If E y then y is a set If and y are sets they are the same if they have the same members Axiom of Sethood If E y then y is a set Axiom of Extensionality If and y are sets then 2 y if and only if E ltgt z E These axioms leave open the possibility that there are many objects which are not sets and which will thus have no elements Of course there cannot be more than one set with no elements We introduce some notation b is the empty set the set with no elements If a b are objects there is a set with just a as an element a set b with just a and b as elements and so forth 115 The notation stands for the set of all such that Pr If g exists we have E a E g There are sentences for which there is provably no such set For example if there were a set R then it would follow that R E R ltgt R g R which is a contra 1iction We adopt a more restricted assumption about the existence of sets for any set A and sentence we assume the existence of E A g Axiom of Separation For each sentence and set A there is a set E A g such that E E A g ltgt a E A As well as restricted sets we also de ne restricted quanti ers E APr is de ned as E A gt and E is de ned as E A A consequence of the axiom of separation is that there is no universal set For any set A E A g is a set by the axiom of separation call it RA RA E RA ltgt RA E A RA RA the only way for this to be true is for RA E A to be false So for any set A we can construct a set which does not belong to it there is no universal set The rest of our axioms provide us with some sets to use in the role of A in Separation Axiom of Pairs b a V 1 exists for any objects a and De nition A Q B A is a subset of B i E A gt E B l39otice that A Q A and 0 Q A are always true Axiom of Power Set For any set A the set PA Q A exists PA is the set of all subsets of A Axiom of Union For any set A the set UA E y y E A exists UA called the union of A is the union of all sets which are elements of A Combining union and pairing we can see that AUB 6 AV E B exists because A U B UA The intersection A 1 B can be de ned as E A g E B so it is provided by Separation alone 116 The relative complement or set difference AB can be de ned as E A g g B so it is provided by Separation alone We do not have complements in general if we refer to the complement of a set A it is always actually a relative complement X A for some set X whose identity is to be understood from context For example if A is intro 1uce 1 as a set of natural numbers references to its complement will probably refer to N A The ordered pair b is de ned as Theorem b 2 ad gt a c b 2 it This theorem tells us everything we need to know about ordered pairs If a E A and b E B observe that E PA Q PA U B and 011 6 PAU B is obvious This means that b E P PA U In turn this means that Theorem For every set A and set B the set A X B the cartesian product of A and B de ned as E P PAUB g 3o 6 AElb 6 B42 2 exists and contains every ordered pair whose rst term is an element of A and whose second term is an element of B Once we have ordered pairs we can de ne the machinery of relations and functions A relation with domain A and range B is a subset of A X B Note that general relation symbols like 2 or Q do not as a rule de ne sets only relations whose domain and range are restricted to elements of speci c sets can be coded by sets A function with domain A and range B is a relation f with domain A and range B with the additional properties that E AEly E E and E AVy E B 2 E E f E f gt y For each element E A we de ne f as the uniquely determined y such that 77 y E f A function f A gt B is an injection or is one to one iff for all a7y 2 implies 2 y A function g A gt B is a surjection from A to B or is said to be onto B just in case Vy E BEL E Aga A function f A gt B is said to be a bijection iff it is an injection and is also a surjection from A to B A bijection is a one to one correspondence We say that A N B A and B are the same size just in case there is a bijection from A to B 117 Now we de ne the natural numbers The basic idea is that we want to de ne each natural number n as a set with n elements This makes 0 the empty set Notice that for any n gt 0 the set 0 n 1 has n elements We de ne it as 0 n 1 This means that 0 0 1 0 2 0 1 0 Notice that for any natural number n nUn 0 n1Un 0 n1 n n 1 We want to de ne the set of all natural numbers For this we need a new axiom Axiom of In nity There is a set S such that 0 E S and E S gt U E S Fix a set S which witnesses the truth of the axiom We can de ne N the set of natural numbers as n g VA 6 PS 0 E A E A gt arU E A gt n E This set will clearly contain our natural numbers 0 1 2 3 and is the intersection of all sets which contain all of them We need the Axiom of In nity to say that there is at least one set which contains 0 and is closed under the successor operation notice that AU exists for any set A not just for natural numbers Now we de ne notions of counting We say that a set A is nite just in case there is a natural number n such that A N u If A is nite we let A represent the unique natural number n such that A N n it is of course necessary to prove a theorem that A N n for no more than one u or this de nition won t make sense If m and n are natural numbers we de ne m n as the unique p such that for any A N m and B N n with A 1 B 0 ie A and B are disjoint we have A U B p We can more explicitly de ne m n as m gtlt U n x If m and n are natural numbers we de ne mu 2 m X n Theorems need to be proved to show that the disjoint union of two nite sets is nite and that the cartesian product of two nite sets is nite It takes some work to prove that the axioms of formal arithmetic we provided above are true of our natural numbers it is necessary to restrict all quanti ers to the set of natural numbers in these axioms though 118 Math 387 Spring 2009 Lecture Notes Contents M Randall Holmes May 7 2009 1 Introduction 2 Propositional Logic 21 January 207 2009 levels of language7 basic operations7 truth January 217 2009 adequacy of our basic operations reducing them too far tables 22 23 231 232 233 234 235 236 237 24 25 26 27 28 29 Homework Set 1 January 267 2009 Examples of natural deduction proofs January 277 2009 Lab 1 January 287 2009 sequents and rules Homework 2 Jan 307 2009 Proofs of correctness of sequent rules January 237 2009 proof strategy for natural deduction proofs Conjunctions in proofs Implications in proofs Biconditionals in proofs An example with conjunction and implication and bi conditional Negation in proofs Disjunction in proofs Discussion and more examples 210 February 27 2009 sample proof trees 211 Tuesday7 February 37 2009 Lab ll7 worked on Homework ll 03 n 212 Wednesday February 4 2009 multiple conclusion sequents and rules derivations of rules for disjunction and implication from those for negation and conjunction 51 Predicate or FirstOrder Logic 56 31 Friday February 6 2009 introduction to predicate sentences and quanti ers 56 32 February 9 2009 sample proof trees and natural deduction proofs with quanti ers 61 33 February 10 2009 7 Lab 111 rst stand alone lab assignment 63 34 Wednesday February 11 2009 some proof tree examples 63 Formalized Arithmetic 65 41 Tuesday February 17 2009 discussion of test introduction to formal arithmetic formal rules for equality 65 42 February 18 2009 multiple and restricted quanti ers addi tion of natural numbers is commutative 68 43 Homework 3 70 44 February 20th and 23d 2009 De nition and properties of order in formal arithmetic 71 45 February 24th 2009 Lab lV 76 Completeness of rst order logic 99 51 Soundness of our logic 99 52 The cut rule and Marcer Tthut command 100 53 Completeness of our logic 102 Constructions in set theory 106 61 March 2 2009 introduction to set theory 106 62 March 3 2009 lab V continuation of Lab 1V 111 63 March 4th and 6th 2009 implementation of mathematical concepts Zermelo natural numbers proof strategy for set theory the ordered pair basics of functions and relations 111 631 Zermelo7s implementation of the natural numbers 111 632 Proof strategy for set theory 115 633 De nition and basic properties of the ordered pair 116 634 Basics of the theory of relations and functions sizes of sets 119 K 00 1 64 Homework 4 121 65 March 97 2009 Counting and the von Neumann natural numbers122 66 March 107 2009 Lab Vl 125 67 March 117 2009 veri cation of Axiom lV 126 68 March 187 2009 counting 128 69 March 207 2009 addition and multiplication 129 610 Homework 5 133 Finite Combinatorics 133 71 Group Axioms7 basic results 133 72 An example the groups of orders 1 4 isomorphism 136 73 Subgroups orders of elements 141 74 Symmetries of a Square an extended example 144 75 Cosets and Lagrange7s theorem 147 76 The characterization of cyclic groups results about Euler7s function 147 77 Permutations 149 78 Example the subgroups of A4 149 79 The groups of order 6 150 710 Possibly helpful note about the groups of order 8 150 711 Groups of permutations 151 Extra Stuff for Test 111 154 81 Permutations which commute 154 82 Extra stuff about generating functions 156 Introduction More stuff might appear here later For the moment I shall just say that the rst part of this course is on logic and the foundations of mathematics7 and we shall begin with logic7 of which the rst branch is propositional logic 2 Propositional Logic Propositional logic is the study of mathematical concepts corresponding to the little English words not and or if I might say more about this heading later7 but for the moment7 onwardl 21 January 20 2009 levels of language basic opera tions truth tables I started by saying something about three layers of language formalized language Formalized languages have precise de nitions for all symbols employed and a precisely expressed grammar of allowed ex pressions The language of propositional logic that we introduce in this section is a formalized language A computer language is a formalized language mathematical English In mathematical English7 we speak more or less naturally7 though we are more careful about our grammar and our use of particular words may be governed by the technical meanings we assign them in mathematics We hope that the formal rules of inference that we learn to apply to formalized languages will transfer to techniques of reasoning that we can use in writing proofs in mathematical English and in fact I will talk about the relationships between these activities ordinary speech Our ordinary language is lled with ambiguities and vague nesses of meaning We know this7 yet we manage to get along somehow It might be that learning how to reason very precisely in formalized lan guages or in mathematical proofs may help us argue more convincingly in other areas of life7 but other things are also at work there We begin de ning the formalized language of propositional logic atomic sentences For the moment7 sentences with no internal structure are represented by capital letters A7 B7 0 sentence variables Script letters such as A7 8 C are sentence variables7 which may stand for any sentence at all whether it has internal struc ture or not We will see the use of this shortly complex sentences If A and B are any sentences7 A A B A V 13 7 A a 13 7 and A lt gt B are sentences These sentence forms A A B A V B A a 13 7 and A lt gt B are read not A 7 A and B A or B if A7 then B and A if and only if B The precise intended meanings are explained below 4 Note the use of sentence variables in the de nition of complex sentences The general sentence form A B a conjunction includes examples like AVB C7 because the script letters A and B may themselves represent complex sentences The use of parentheses above may appear excessive We will adopt con ventions of order of operations77 which allow many parentheses to be left out However7 since we are in the realm of formalized language7 we need to spell out precisely what omissions we will allow as we would when enabling order of operations in a computer language We will do this below until then we may drop parentheses in cases where confusion is unlikely We introduce the semantics fancy Greek term for meaning of our constructions Each sentence of our formal language is intended to be either true or false More formally7 we assign a value t or f to each sentence Each atomic sentence may have the value t or f nothing in propositional logic allows us to decide which The value of a sentence variable is determined by the structure of the sentence it represents The value of a sentence A is t if the value of A is f7 and f if the value of A is t This is more readily seen in a truth table A A t f f t The operation denoted by n is called negation and the sentence A means It is not the case that A We will give truth tables for each of the complex sentence constructions we have given We do add that we rmly maintain that truth tables7 while they are a useful technical tool7 have nothing at all to do with how we ac tually reason in formalized or unformalized language They are very precise7 however7 which is an advantage ABAB The operation denoted by is called conjunction and A 8 means A and 8 There are uses of the English word and77 which are not in line with the use of A but we will not review them now ABAVB The operation denoted by V is called disjunction and AVB means A or 8 Here we are making a decision about the meaning of or77 which ordinary language does not make for us Some uses for or77 really t the following table ABAEBB for an operation which we might call exclusive or If a mother says You may have chocolate cake or cherry pie she is quite likely to be excluding the case where the child has both Lawyers also make this distinction and they call the operation which we represent by V andor ln mathematical English or77 is always to be read as inclusive unless it is speci cally stated that it is to be exclusive ABA B t The operation represented by a is called implication and the sentence A a B is read if A then B or B if A or A implies 8 There are other readings The problem with the truth table for A a B is not anything about its entries but a question as to whether a truth table is appropriate at all That the entries are correct we can deduce from the following little story By promising her child that if he cleans up his room she will order pizza the mother seems to be saying A a B where A means the child cleans up his room77 and 8 means the mother orders pizza If the child cleans up his room and the pizza is ordered the promise has been kept If the child cleans up his room and the mother does not order pizza the promise has been broken we feel that the mother was lying If the child does not clean up his room and the mother orders pizza the mother may be foolishly generous but she was not lying If the child does not clean up his room and the mother does not order pizza that is only to be expected In each case our feelings agree with the truth table given above To see the discomfort one might feel with this consider the statement if 225 then Napoleon conquered China Our table above assures us that this is true Our instinctive reaction is not so much that it is false but that the hypothesis has nothing to do with the conclusion if 22 5 then I like ice cream77 I do leads to similar discomfort it is judged true and If 22 4 then the rst European settlement in Australia was at Botany Bay77 it was which our table tells us is true again leaves us unsatis ed because of the lack of a connection between the hypothesis and the conclusion We nd in practice that this is the most convenient de nition of impli cation Experience should make us more comfortable with it We note that this is not a modern folly of logicians one of the schools of logic in classical antiquity early in the Common Era artived at the same conclusion as to what the de nition of implication must be I do not remember which one ABAHB The operation represented by lt gt is called the biconditional and we read A lt gt B as A if and only if B for which we use A iff B as an abbreviation A lt gt B says that A and B have the same value We have some additional remarks to make about the rhetoric of negation Of course A has the same value as A Also we do not say It is not the case that it is not the case that A when what we want to say is just A This is the famous issue of double negation When we negate an atomic sentence how about A de ned as Snow is white we do not say anything like It is not the case that snow is white we say Snow isn7t white Now consider A B This could be read as It is not the case that A and B but it seems safer to read it as It is not the case both that A and B to avoid ambiguity Notice that this is not anything we would really say If A is Snow is white and B is Violets are blue A B should be read literally It is not the case both that snow is white and violets are blue but one would be much more likely to say Snow isn7t white or violets aren7t blue which re ects the following equivalence ABA AAB Av B The fact recorded above is written A B E A V B This is one of what are called de Morgan7s laws This says something more than A B lt gt A V off though it does say this it says that this is true no matter what sentences replace A and 8 Similar facts which you might be asked to verify in homework are 1 AM v B E AA AB This is the other de Morgan law 2 A BElt AVB 3 Alt gt83AgtBBgtA Notice that A B is equivalent to A B which is in turn equiva lent to A V off so we can de ne conjunction in terms of negation and disjunction The facts above show that implication can be de ned in terms of negation and disjunction and the biconditional can be de ned in terms of conjunction and implication both of which can be de ned in terms of negation and disjunction It is also possible to de ne disjunction in terms of negation and conjunc tion in basically the same way and then de ne implication and the bicondi tional in terms of negation and conjunction as well 8 So either n V or n could be taken as basic operations in terms of which the others can be de ned 22 January 21 2009 adequacy of our basic opera tions reducing them too far In this day7s lecture I addressed two questions Question 1 Do we have enough operations of propositional logic Question 2 Do we have too many operations of propositional logic These are rather vague questions We will be able to make them more precise and answer both of them The operations we have introduced so far take a xed number of sentences 1 in the case of negation and 2 in the case ofeach ofthe others and produce a sentence Moreover7 the behavior of the operation can be completely de ned in terms of the truth values It or f of each of the inputs and the truth value of the output in each case Brie y7 all these operations have truth tables Let B be the set t7 f of truth values we leave aside the historical reasons for the choice of the letter B here Let B be the set of all lists of n truth values for a xed We de ne an n ary truth function77 as a function from B to B This may seem quite bizarre and needlessly abstract It may make more sense when you realize that an n ary truth function precisely codes a truth table for an operation on n sentences7 entirely in terms of ideas you would nd in your discrete math book For example7 ABAHB the truth table for lt gt contains the same information as a function lt gt from B2 to B such that lt gt ht tlt gt t7f flt gt t flt gt f7f It Like the truth table7 the truth function is a nite object We comment on the niteness of truth tables and truth functions I didn7t say this in the lecture but I will come back to it Notice that B has 9 2 elements this corresponds to the fact that a truth table for an expression containing 71 propositional letters has 2 lines In constructing an element of B we make 71 independent choices from 2 alternatives this is why B has 2 arguments We have just counted the rows in a truth table with 71 letters or the elements of the domain of an n ary truth function We can do more than this we can count how many n ary truth functions there are To de ne an n ary truth function we assign a value either It or f independently to the 2 elements of the domain so there are 22 n ary truth functions This indicates why the niteness of the method of truth tables can be overplayed A real life logic circuit may have 100 binary inputs and may reasonably be supposed to have binary output depending in a truth functional way on those inputs This means that to analyze the behavior of the circuit with 100 inputs we need to consider 2100 possible combinations of the input values or about 1030 This is an impracticably large number the method of truth tables will not really work to analyze the behavior of logic circuits Even worse there are 22100 possible different behaviors for a logic circuit with 100 inputs To write this number down would take on the order of 1030 digits in decimal notation Spend some time contemplating just how ridiculously large this is We take a moment to talk about order of operations Our of cial notation has a lot of parentheses We adopt conventions just as we do in arithmetic to avoid having to write so many We apply operations in the following order when not forced to do so in a different order by parentheses rst n then A then V then a then lt gt So We can now answer Question 1 in the af rmative and say precisely what we mean by our af rmative answer Theorem Every n ary truth function fp1 pn is associated with an expression involving propositional variables A1 An and the opera tions V with the property that if each A has the truth value p then the truth value of the expression is fp1 pn Proof We do not give a formal proof but illustrate a procedure which will give an expression with any desired truth table which shows why this is true If we have a truth table with columns for each A and a nal col umn giving the truth value of an unknown expression we can write 10 an expression with this truth table as a disjunction of conjunctions of propositional letters and negations of propositional letters except in one special case There will be a term in the disjunction for each row in the truth table for which the value of the unknown expression is t This term will be a conjunction containing terms A if A is assigned the value t in that row and Aj if A is assigned the value f in that row The exceptional case is that in which there is no row in which the unknown expression has the truth value t In this case the expression A1 A Al will work if one prefers to have every letter in the expression one can throw all the other letters into the conjunction along with the contradiction Here is an example of the procedure ABC is realized if is taken to be AABACvA B cv ABCv A BC Now for Question 2 Our answer to this is also af rmative in a sense we have too many logical operators of propositional logic but it is really a tongue in cheek77 answer in reality we really do not want to work with fewer basic operations even though we can replace the set ofthree operations we have just shown to be adequate with a single operation We showed above that V are enough to de ne all operations on sentences which have truth tables We also showed at the end of the previous lecture that we can de ne disjunction in terms of negation and conjunction AVBE A 8 11 and similarly we can de ne conjunction in terms of negation and disjunc tion AABE bAv B so either or n V provide a set of operations from which all operations with truth tables can be constructed The second set is very often used In the late 19th or early 20th century a man named Sheffer noticed that one operation is enough A B t is called the Sheffer stroke Computer scientists call it NAND because All E A 8 Now we can verify the following equivalences negation nA E AlA conjunction A B E AlBlAlB disjunction A V B E AlAlBlB So it is possible to express any operation on sentences with a truth table entirely in terms of the Sheffer stroke But would you want to There is an alternative AB is the truth table of an operation which computer scientists call NOR and for which there is actually an English grammatical construction A l 8 means neither A nor 8 Now we can verify the following suspiciously similar equivalences 12 negation nA E A l A disjunction A V B E A l B l A l B conjunction A B E A l A l B l B It is very interesting and may occasionally be useful in formal arguments about propositional logic that we can reduce all the operations to one op eration but facts about the way we think drive our desire to have all the operations n A V a and even lt gt as basic operations We would not reduce the reasoning techniques for all of these to rules for using l or even the more familiar 1 because that does not re ect the way we actually reason In the next lecture we will start introducing the basic rules for reasoning with the constructions of propositional logic on an informal level which we hope will actually be helpful in writing proofs in mathematical English 23 January 23 2009 proof strategy for natural de duction proofs In this lecture we introduce strategies for dealing with statements in proofs based on their logical form For each of the logical operators we present two different kinds of strategies one for proving a statement of that form and one for using a statement of that form which you have proved or shown to follow from your assumptions The method of proof we are describing presented in mathematical English in a highly structured form we will call natural deduction In this style of reasoning which we will conduct here in symbols but which can also be done in mathematical English we need to distinguish between statements which we are trying to prove which we will call goals and statements which we have assumed or shown to follow from our assumptions or proved unconditionally which I might sometimes call posits as in the Math 502 notes Always be careful in a proof to distiguish between what you know or can assume on the one hand and what you are trying to prove or deduce from current assumptions on the other 231 Conjunctions in proofs To deduce a statement of the form A B from your current assumptions deduce A from your current assumptions and then deduce B from your 13 current assumptions If you have shown that A 8 follows from your assumptions you can further conclude that A follows from your assumptions and that 8 follows from your assumptions 232 Implications in proofs To deduce a statement of the form A a B from your current assumptions add the new assumption A and adopt B as your new goal If you succeed in deducing 8 you can then conclude that A a 8 follows from your original assumptions and drop the temporary assumption A If you have shown that A a 8 follows from your current assumptions and that A follows from your current assumptions then 8 also follows from your current assumptions This is traditionally called the rule of modus ponens A way to phrase modus ptmens which starts out with just the implication sentence is this if you have shown that A a 8 follows from current assump tions adopt A as a new goal once you have deduced the goal A you will be able to draw the additional conclusion 8 233 Biconditionals in proofs To show that A lt gt 8 follows from your current assumptions prove that A a 8 follows from your current assumptions use the strategy above and that B a A follows from your current assumptions If one has shown that A lt gt 8 follows from your current assumptions and that A follows therefrom then 8 also follows If one has shown that A lt gt 8 follows from your current assumptions and that 8 follows therefrom then A also follows Both sets of rules for the biconditional follow directly from the equivalence A lt gt B E A a B B a A and the rules for conjunction and implication 234 An example with conjunction and implication and bicon ditional We prove Aa B C HAAB C Goal 1 A a B a C a A B a C Recall that to prove a biconditional we need to prove the implications in both directions To prove the implication we assume the hypothesis and adopt the conclusion as a new goal Assume 11 A a B a C Goal 11 A B a C This goal is another implication We use the same strategy Assume A 8 Goal 111 C Because we have assumed A B we can conclude From A and Assumption 11 we can deduce B a C by modus ponens Because we have assumed A B we can conclude 8 From 8 and B a C we can conclude C Thus we have shown that Goal 111 follows from the as sumption before it and the assumption before Goal 117 from which it follows that Goal 11 follows from the assumption be fore it7 from which Goal 1 follows We won7t always say this part when all goals have been shown7 the proof is over Goal 2 A B a C a A a B a C This is the second implication to be proved to establish the biconditional we are trying to prove We are now proving an implication Assume 21 A B a C Goal 21 A a B a C We are proving another implication Assume A Goal 211 B a C Yet another implication Assume 8 Goal 2111 C At this point we have completed the un packing of implications Our rst assumption is A B a C if we could deduce A B we would be able to conclude C by modus ponens In order to show A B we need to show A and B but both of these are assumptions we have made above So we can conclude A B and from this and Assump tion 21 we deduce C the current goal 2111 by modus ponens All goals are now established and the proof is complete The indented structure should help you to see the structure of the proof7 and in particular to see the scope of each assumption 235 Negation in proofs Negation and disjunction are perhaps a little trickier than conjunction and implication To show that A follows from your current assumptions7 add a new as sumption A and show that a contradiction BA l follows This is not proof by contradiction7 but the direct proof of a negation we will see proof by contradiction below If you have shown that A follows from your current assumptions7 you can further conclude A Notice that I am not giving a general rule for using a negative conclusion The strategy of proof by contradictorz follows from these two rules To show that a statement A of any logical form follows from your current assumptions7 assume A and deduce a contradiction This is a direct proof of the negation A from which the further conclusion A can be drawn 236 Disjunction in proofs To show that A V 8 follows from your current assumptions7 make an addi tional assumption A and show that 8 follows To show that A V 8 follows from your current assumptions7 make an additional assumption t and show that A follows Notice there are two similar symmetric strategies here Here is something important I omitted from my lecture but you will get it on Monday Suppose we have shown that A V 8 follows from our assumptions and we have a goal C of any logical form To show that C follows7 show that it follows if we replace the assumption A V B with A and also follows if we replace the assumption AVB with B This is the well known strategy of proof by cases which is the usual strategy for using a disjunction 237 Discussion and more examples The rules I have given so far are the of cial basic rules There are other ones which we will use I gave two other rules for disjunction in class Friday7 which actually follow from proof by cases with a little work From AVB and A deduce 8 From A V B and l deduce A These come out of the fact that A V B E A a E t a A I will show below how to deduce these rules well7 one of them from proof by cases A very important set of additional rules for implication follow from the equivalence of A a B with its contrapositive t a A proof by contrapositive To show that A a 8 follows from our current assumptions7 add a new assumption t and deduce the new goal A this is a proof of t a A so if we show the equivalence of implica tions with their contrapositives we justify this strategy modus tollens From A a B and t deduce A from t a A and l A follows by modus ponens We justify these additional rules of implication by the following proof Theorem A a B lt gt t a nA The proof of a biconditional falls apart into proofs of two implications Goal 1 A a B a t a A We prove an implication in the usual way Assume 11 A a 8 Goal 11 t a nA Another implication Assume l Goal 111 A We now have a strategy for proving negations Assume A Goal 1111 a contradiction From A and Assumption 11 we can deduce B by modus ponens From B and B assumed above we get the contradiction B l which achieves our goal Goal 2 t a A A a B We use the usual strategy for implication 17 Assume 21 t a A Goal 21 A a B One more implication to unpack Assume A Goal 211 8 Since goal 211 has no logical structure known to us7 the only strategy that might work is proof by contradiction Assume l Goal a contradiction From t and Assumption 21 we can deduce A We have also assumed A above7 so we can deduce the con tradiction A A and we are done More to follow in the next set Notice that I did make a change in this set from what I actually said in lecture I introduced the rule of proof by cases I will talk about this on Monday 24 Homework Set 1 This homework set is due next Monday a week from tomorrow as I write on the 25th If you do not understand the instructions for a problem7 ask in class or come see me in my of ce 1 3 One point I did not make under order of operations77 above was that one can drop more parentheses where associative operations are in volved A BAC E AAB C so we can indifferently write AABAC for either Show that implication is not associative7 using a truth table Show that the biconditional is associative7 using a truth table Verify each of the theorems in the previous day of lectures the two big examples using truth tables What can you say about truth tables by contrast with the form of reasoning introduced in the last lecture Can you see any relationship between them How would you contrast them I really want you to express some thoughts here if you can come up with any 3 4 Cf Again because of associativity7 we can write A V B V C V D and further things of that sort7 using conjunction7 disjunction7 or biconditional to link any number of sentences there is one more logical operation we can do this with The meaning of A V B V C V D is quite obvious the meaning of A lt gt B lt gt C lt gt D is rather less obvious Do some investigation Find out what A1 lt gt A2 lt gt lt gt Awl lt gt An means in general There is a simple description7 but it is not at all obvious without actually doing exarnples Make truth tables for n 3 and n 4 and you might get an idea l7rn sure you can nd this in a book sornewhere Please dont Write out A lt gt B using just the Sheffer stroke Write it out using just neither nor Boolean algebra There is a tradition of computational logic in which we write conjunction as it if it were multiplication and disjunction as if it were addition The following logical equivalences written as algebraic equations look somewhat familiar with some startling exceptions We use 0 for f and 1 for t We use 7a for u though this is not as good an analogy abba abcabc abcabac ab ba abc abc abc abac 00a 1aa 0a 1a 7ltabgt lt7agtltebgt agt a 7ltabgt iaib a7a Identify the de Morgan laws on this list Verify one of the distribu tive laws using a truth table If you nd any of the other statements startling7 feel free to verify them you get points if you are rst to identify an error How would I most conveniently write a a b Can you describe the relationship between the left hand and right hand columns of the table There is a simple description rnoreover7 if you 19 take any theorem of Boolean algebra and make the changes which take you from one column to the other you get another theorem of Boolean algebra Write an algebraic proof of the surprising distributive law a be a ba c by rst writing a be 77a 190 why can we do this then applying de Morgan7s law and the other distributive law l7ve given you the general idea write it out in detail CT more algebraic logic lnterpret 0 as false and 1 as true as in the previ ous problem Instead of considering the usual propositional operations as we do there start with a familiar system of algebra involving just 0 and 1 namely mod 2 arithmetic Which logical operation does mod 2 multiplication represent Hint it is familiar Which logical operation does mod 2 addition represent Hint it is less familiar but we have given a name for it and a truth table above Notice that mod 2 addition is of course associative so we have shown that another logical operation is associative Now for a little more fun suppose we interpret 0 as true and 1 as false What logical operations do the addition and multiplication of mod 2 arithmetic represent then 25 January 26 2009 Examples of natural deduction proofs On this day we did some examples to illustrate the style of reasoning de scribed the previous day Here is an example using just conjunction and implication Prove A a B B a C a A a C Its an implication Assume 1 A a B B a C Goal A a C Assume A 20

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

## Why people love StudySoup

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "Selling my MCAT study guides and notes has been a great source of side revenue while I'm in school. Some months I'm making over $500! Plus, it makes me happy knowing that I'm helping future med students with their MCAT."

#### "There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

#### "Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.