1계논리 연습문제 #2 [2012-12-8]

[게시판 2 (IE only)] [Proofmood 홈]

다음의 두 형식증명을 완성하시오.


  1. [ @x@y((x _subseteq y) % @z((z _in x) $ (z _in y))) ; @x@y@z((z _in x _cup y) % (z _in x) | (z _in y)) ; @x@y@z(x _in y _subseteq z $ (x _in z)) entails [ (a _subseteq c) & (b _subseteq c) entails [ {z} entails [ z _in a _cup b entails (z _in a) | (z _in b) :@ elim 2,6 ;[ entails z _in a _subseteq c :tautcnsq 4,8 ; z _in c :Rule ? ] ;[ z _in b entails :Rule ? ; z _in c :@ elim 3,12 ] ; z _in c :tautcnsq 7,8-10,11-13 ] ] ; @z((z _in a _cup b) $ (z _in c)) :Rule ? ; :Rule ? ] ; (a _subseteq c) & (b _subseteq c) $ (a _cup b _subseteq c) :tautcnsq 4-16 ] !line_cnc17

  2. [ @x((x _in cB) % (x _in cA) & (x _notin f(x))) ; (a _in cA) & (f(a) = cB) entails [ a _in cB entails (a _in cA) & (a _notin f(a)) :@ elim 1,3 ; a _notin f(a) :Rule ? ; a _notin cB := elim ; ^ :Rule ? ] ;[ a _notin cB entails a _notin f(a) := elim ; (a _in cA) & (a _notin f(a)) :tautcnsq 2,9 ; a _in cB :@ elim 1,10 ; :Rule ? ] ; ^ :tautcnsq 3-7,8-12 ] !line_cnc12