1계논리 연습문제 #3 [2013-5-27]

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

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


  1. 해답: [ @y(#x(F(x) & E(x) & (x _in f(y))) $ Rich(y)) ; @y(#x(G(x) & (x _in f(y))) $ Rich(y)) ; #x((x _in f(dKim)) & (G(x) | F(x))) ; @x((x _in f(dKim)) $ G(x) | E(x)) entails #x(F(x) & E(x) & (x _in f(dKim))) $ Rich(dKim) :@ elim 1 ;[ {c} (c _in f(dKim)) & (G(c) | F(c)) entails c _in f(dKim) :tautcnsq 6 ; G(c) | E(c) :@ elim 4,7 ; #x(G(x) & (x _in f(dKim))) $ Rich(dKim) :@ elim 2 ;[ G(c) entails G(c) & (c _in f(dKim)) :tautcnsq 6,10 ; #x(G(x) & (x _in f(dKim))) :# intro 11 ; Rich(dKim) :tautcnsq 12,9 ] ;[ E(c) entails [ F(c) entails F(c) & E(c) & (c _in f(dKim)) :tautcnsq 15,14,6 ; #x(F(x) & E(x) & (x _in f(dKim))) :# intro 16 ; Rich(dKim) :tautcnsq 17,5 ] ;[ ~F(c) entails G(c) & (c _in f(dKim)) :tautcnsq 6,19 ; #x(G(x) & (x _in f(dKim))) :# intro 20 ; Rich(dKim) :tautcnsq 21,9 ] ; Rich(dKim) :tautcnsq 15-18,19-22 ] ; Rich(dKim) :tautcnsq 8,10-13,14-23 ] ; Rich(dKim) :# elim 3,6-24 ] !line_cnc25
  2. 위 문제에서 라인 4를 ∀x∀y((x ∈ f(y)) ∧ F(x) → G(x) ∨ E(x))로 바꾸어서 형식증명을 찾아 보시오.

  3. 해답: [ @xR@yR@z@w(R(z,w,xR o yR) % #u(R(z,u,xR) & R(u,w,yR))) ; @z@w@xR(R(z,w,fInv(xR)) % R(w,z,xR)) entails [ {aR,bR,c,d} entails [ R(c,d,fInv(aR o bR)) entails R(d,c,aR o bR) :@ elim 2,4 ; #u(R(d,u,aR) & R(u,c,bR)) :@ elim 1,5 ;[ {e} R(d,e,aR) & R(e,c,bR) entails R(e,c,bR) :tautcnsq 7 ; R(c,e,fInv(bR)) :@ elim 2,8 ; R(d,e,aR) :tautcnsq 7 ; R(e,d,fInv(aR)) :@ elim 2,10 ; R(c,e,fInv(bR)) & R(e,d,fInv(aR)) :tautcnsq 9,11 ] ; #u(R(c,u,fInv(bR)) & R(u,d,fInv(aR))) :# elim 6,7-12 ; R(c,d,fInv(bR) o fInv(aR)) :@ elim 1,13 ] ;[ R(c,d,fInv(bR) o fInv(aR)) entails #u(R(c,u,fInv(bR)) & R(u,d,fInv(aR))) :@ elim 1,15 ;[ {e} R(c,e,fInv(bR)) & R(e,d,fInv(aR)) entails R(c,e,fInv(bR)) :tautcnsq 17 ; R(e,c,bR) :@ elim 2,18 ; R(e,d,fInv(aR)) :tautcnsq 17 ; R(d,e,aR) :@ elim 2,20 ; R(d,e,aR) & R(e,c,bR) :tautcnsq 21,19 ] ; #u(R(d,u,aR) & R(u,c,bR)) :# elim 16,17-22 ; R(d,c,aR o bR) :@ elim 1,23 ; R(c,d,fInv(aR o bR)) :@ elim 2,24 ] ; R(c,d,fInv(aR o bR)) % R(c,d,fInv(bR) o fInv(aR)) :tautcnsq 4-14,15-25 ] ; @xR@yR@z@w(R(z,w,fInv(xR o yR)) % R(z,w,fInv(yR) o fInv(xR))) :@ intro 3-26 ] !line_cnc27