※ 引述《rodyforeter (rodyforeter)》之铭言： : 标题: Re: [问题] 关於universal generalization 的restr … : 时间: Sat Jul 3 08:58:17 2010 : : OK 所以我想CP 的这种情况是可以做UG : : 那麽我又想 IP 的这种情况会是如何？？？？ : : 假设有个论证如下: : : 1. / : : 　　2.~Ax AIP : 3. : 4. : 5. : 6.Ax 2-5IP : : 重点来了 这里6.的自由变元可以做UG吗？ : : 我认为应该不行...难道有什麽神乎其技的方法能够像CP那样把这里也做UG？ 其实两个都可以。 所谓 CP/IP证明的限制, 是指说在还没有关起来的中间做UG, 像是以下两种证明都是不行的: 1. Fx ACP 2. (x)Fx UG 3. Fx->(x)Fx CP 4. (x)(Fx->(x)Fx) UG 其中第二步的UG是不行的。 1. (Fx & ~Fa) ACI 2. (x)(Fx & ~Fa) UG 3. (Fa & ~Fa) 2, UI 4. ~(Fx & ~Fa) 1-3 CP 5. (x)[~(Fx & ~Fa)] 4, UG 这里第二步的UG也是不行的。 而你说的那种情况做UG是可以的。因为UG其实是以下的後设定理的运用: Theorem: If a formula φ(x) with x as its free variable can be proved, then the formula (x)φ(x) can be proved。 而运用这个meta-theorem, 在你提到的CP和IP的证明当中其实是可以用的。 : : -- :

※ 发信站: 批踢踢实业坊(ptt.cc) : ◆ From: 61.231.226.220 : ※ 编辑: rodyforeter 来自: 61.231.226.220 (07/03 09:01) : → a3435357:5错了，应该是Bz 07/03 10:06 : → a3435357:可能没有这个必要，ip证法通常是假设结论的否定，求矛盾 07/03 20:59 : → a3435357:因为有矛盾故推翻假设，结论因此而得证，当run完一回ip证 07/03 21:00 : → a3435357:证明也结束了，也没有做UG的必要 07/03 21:01 这个讲法应该没错。 假设我们有一个证明, 是在做後一步用UG, 如以下形式: 1. ~φ(x) ... ... contradiction n. φ(x) IP n+1. (x)φ(x) UG 我们总是相对应的有以下的证明: 1. ~(x)φ(x) 2. (Ex)~φ(x) 3. ~φ(a) ... ... contradiction n. (x)φ(x) IP 这应该很容易在自然演译法的系统中当成一个後设定理证明出来。 这里主要的原因是, 如果在你的自然演译法系统中, 两个量词 (x)和(Ex) 都是原初, 且你又有EG, UG, EI, UI, 而且你还有两者转换的公式, 那麽其实它会有些是多余的, 因为UG其实相应於EI。 而如果你想要让你的系统简单一点, 像很多逻辑书的作者会这麽做, 你可以只保留universal quantifier, 然後定义 (Ex) 为 ~(x)~ 这麽做的话, 你有的是UG和UI而已, 也就是量词的introduction rule 和elimination rule (这也比较符合自然演译法的精神), 那麽你会发现你会需要在某些证明的最後一步做UG, 而无法直接假设否定导矛盾。 --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 81.107.38.67 这边如果你的1只是假设的前提, 而你还没证出什麽东西来时, 是不能做2.这一步的。 ※ 编辑: MathTurtle 来自: 81.107.38.67 (07/04 19:06)