【附加前提引入时有的加否定谓词演算的推理中,附加前提引入有什么规则?为什么在推理过程中用到附加前提,有的前提要加否定,有的不加呢?例：前提：w→(˥(r∧s)→˥q),w,˥s结论：&#741】

　　附加前提引入时有的加否定

　　谓词演算的推理中,附加前提引入有什么规则?为什么在推理过程中用到附加前提,有的前提要加否定,有的不加呢?

　　例：前提：w→(˥(r∧s)→˥q),w,˥s

　　结论：˥q

　　˥(˥q)P（附加前提）

　　为什么要加否定?

　　证明：A→(B→C),˥D∨A,B˫D→C

　　DP(附加前提)

　　这个D是哪个D?是˫之前的D还是之后D→C中的D?

　　3.证明：(∀x)(G(x)∨Q(x))˫(∀x)G(x)∨(∃x)Q(x)

　　：

　　(1)˥((∀x)G(x)∨(∃x)Q(x))P(附加前提)

　　(2).....

　　这个附加前提，是˫符号后面的结论吗？为什么要加否定？

　　4.证明：(∀x)(G(x)∨Q(x))˫˥(∀x)G(x)→(∃x)Q(x)

　　（1）˥(∀x)G(x)P（附加前提）

　　（2）......

　　这个（1）步中的附加前提是˫符号后的结论中的˥(∀x)G(x)还是前提(∀x)(G(x)∨Q(x))演化过来的？如果是˫符号后的结论中的前提为什么这个没有加否定呢？