부정 정리(Negation Theorem) 증명 질문

[익명(106.101)]

저 빨간 부분이 이해가 안됨

~(∀y)(∀z)~(∃x)~[(~Fxz∨(∀w)~[(Hxzw•~Hxzx)]]에서 부정 정리 적용하면

~(∃y)(∃z)~(∀x)~[(Fxz•(∃w)~[~Hxzw∨Hxzx]] 아님?

왜 (∃y)(∃z)~(∀x)~[(Fxz•(∃w)~[~Hxzw∨Hxzx]]냐? 부정("~") 하나는 어디로 간 거임?

왜냐하면 (∀x)(∃y)~[Fxy∨(∃z)[Gzy•(Hxz∨~Fxz)]]는

(∃x)(∀y)~[~Fxy•(∀z)[~Gzy∨(~Hxz•Fxz)]]로 제대로 ∀<->∃ 와 &<->∨ 와 원자식에 부정 넣어주는 거 다 적용해서 치환이 했잖아

이거 말고 양화사 전환 규칙 Quantifier exchange 규칙 알긴 함. 근데 지금 여기서는 Quantifier exchange 적용하고 있는 게 아니고 Quantifier exchange 적용하면 오히려 ~(∀y)(∀z)~(∃x)~[(~Fxz∨(∀w)~[(Hxzw•~Hxzx)]]에서

(∃y)(∃z)~(∀x)~[(Fxz•(∃w)~~[~Hxzw∨Hxzx]]가 되야지

즉 (∀w)~[(Hxzw•~Hxzx)]]부분이 (∃w)~~[~Hxzw∨Hxzx]]로 되야함. 부정 기호 계속 옆으로 옮기니까 당연함. 근데 (∃w)~[~Hxzw∨Hxzx]]임. 똑같이 부정 기호 하나가 쥐도 새도 모르게 사라져있음.

요약: 위 정리에 따르면 ~(∀y)(∀z)~(∃x)~[(~Fxz∨(∀w)~[(Hxzw•~Hxzx)]]은

~(∃y)(∃z)~(∀x)~[(Fxz•(∃w)~[~Hxzw∨Hxzx]] 또는 (∃y)(∃z)~(∀x)~[(Fxz•(∃w)~~[~Hxzw∨Hxzx]]가 되어야 옳지 않음?

어째서 (∃y)(∃z)~(∀x)~[(Fxz•(∃w)~[~Hxzw∨Hxzx]]인지 모르겠음.

[익명(106.101)]

책은 벤슨 메이츠 기호논리학 219p~225p 발췌임

[익명(180.83)]

이중부정이 삭제되어서임. 나는 그렇게 봄.

[익명(106.101)]

정확히 어떻게서인지 설명 가능?

[익명(180.83)]

VIII가 지시하는 절차는 넷임. 1. 연언과 선언 연산자의 교환 2. 양화사 간의 교환. 3. 리터럴 간의 교환. 4. 교환결과에 부정을 취하면, 원래의 식과 동치(이중부정은 제거). 네가지를 순서대로 다 해보면 -(y)(z)-(Ex)-(-Fxz+(w)-(Hxzw&-Hxzx)) ---> 1. -(y)(z)-(Ex)-(-Fxz&(w)-(Hxzw+-Hxzx)) ---> 2. -(Ey)(Ez)-(x)-(-Fxz&(Ew)-(Hxzw+-Hxzx)) ---> 3. -(Ey)(Ez)-(x)-(Fxz&(Ew)-(-Hxzw+Hxzx)) ---> 4.(Ey)(Ez)-(x)-(Fxz&(Ew)-(-Hxzw+Hxzx)). 보다시피 4번은 저 두 번째 빨간 강조 식과 동일함.

[익명(180.83)]

메이츠의 책이 상당히 난잡하므로 이해하려면 Duality 관련해서 검색해보면 더 쉬운 표기로 나옴.

[익명(180.83)]

두 번째 빨간 강조 식 아래의 식은 그냥 subformula에 드 모르간의 정리를 반복 적용해서 치환하는 거임. 그래서 VI를 반복해서 적용했다는 거고.

[익명(106.101)]

와 진짜 고마워