※ 引述《rodyforeter (rodyforeter)》之铭言： : : (3)如果α在条件证预设或归谬证法预设中的语句或语句函数里是自由出现的，不可以在 : : 　预设释放前，对它做UG。 : 这里我是这样想的 不知道对不对: : 因为x是自由存在於预设中，要验证这个预设能不能在任何情况下都成立，有两种情况 : 第一种如果x只代表某"一"个或者某"些" 那只能做EG不能做UG如此预设才能合法验证， : 第二种是x代表所有、任何 那就能做EG也能做UG都可以合法验证这个预设 : 所以为了让这个预设在各种(两种)情形中都能合法去验证，只能用EG而不能用UG，EG验证 : 能让两种情况都包含，相反UG就算验证出了预设也只能在x是代表所有、任何的情形成立 : 这种想法，也就是Fx x可能为非任何or任何，让我困惑 : 要怎麽样才能知道什麽时候Fx能做UG? 例如 Fx /(x)Fx 能不能做UG得证结论? 最不会让人误会的方式(也是我理解的方式), universal generalisation 是以下的推论规则(适用於任何系统): (UG) 假设 φ(x)是任何的open formula, 而 x 是出现在 φ里面 惟一的 free variable, 而假设 a 是在φ中没有出现的常元, 我们令 φ(a) 表示将 x 任何出现的地方都代换为 a 所产生 的句子(一个closed formula), 假设 y 是在φ中没有出现的 变元, 那麽, 若 φ(a) 可以被证明为定理, 则 (x)φ(x) 可以被证明为定理。 如果你用 |-φ 来表示 φ可以被证明为定理, 那麽这个推论规则通常会简写成: (UG) If |-φ, then |- (x)φ(x) (然後会加上一些说明, 但主要是关於变元如何代换的说明, 像我上面那个 比较复杂的式子讲的那样, 要全部取代且要是新的变元) 而会让你感到困惑的, 会是以下错误的UG (假UG) |- (φ -> (x)φ(x)) 仔细想想这两个有何差别, 一个说 If |-φ, then |- (x)φ(x), 也就是, 假设我们能证出φ, 则我们能证出 (x)φ(x), 也就是须要你已经证明了某个东西了, 你才能应用这个推论规则, 而另一个则是说(φ -> (x)φ(x)), 也就是他会容许你把这式子直接会来用, 而不需要你已经证出某个东西。 --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 81.107.38.67