多嵌套量词的否定：将否定直接作用于P的命题改写问询

我明白你现在卡在“把否定推过量词”这个步骤上，其实教授说的方法就是让否定符号逐个“穿过”每个量词，每穿一个就换一次量词类型，直到最后否定直接贴在P上。咱们拿你的两个命题一步步拆解，就清楚了：

第一个命题：¬∃푥 ∃푦 푃(푥, 푦) #

咱们从最左边的否定开始，一步步推：

• 第一步：把否定推过∃푥，把∃换成∀，得到：∀푥 ¬∃푦 푃(푥, 푦)
• 第二步：再把否定推过∃푦，把∃换成∀，最后否定直接作用在P上，最终结果：∀푥 ∀푦 ¬푃(푥, 푦)

第二个命题：∃푥 ¬∀푦 ∃푧 ∀푤 푃(푥, 푦, 푧, w) #

这里否定一开始就在∀푦前面，咱们从这里开始推：

• 第一步：把否定推过∀푦，把∀换成∃，得到：∃푥 ∃푦 ¬∃푧 ∀푤 푃(푥, 푦, 푧, w)
• 第二步：把否定推过∃푧，把∃换成∀，得到：∃푥 ∃푦 ∀푧 ¬∀푤 푃(푥, 푦, 푧, w)
• 第三步：把否定推过∀푤，把∀换成∃，否定直接作用在P上，最终结果：∃푥 ∃푦 ∀푧 ∃푤 ¬푃(푥, 푦, 푧, w)

简单来说，就是否定符号像个“转换器”，每经过一个量词就把它的类型翻转（∃↔∀），一路推到P的前面就完成了，不用纠结只否定直接前置的量词，就是逐个往前推就行~

内容的提问来源于stack exchange，提问作者Jessica Tiberio