作者xcycl (XOO)
看板logic
标题Re: [讨论] 关于构造逻辑
时间Mon Feb 9 06:50:01 2015
※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 124.77.89.116
※ 文章网址: https://webptt.com/cn.aspx?n=bbs/logic/M.1423026514.A.572.html
1F：推 ppu12372: 构造逻辑到底是啥? 我GOOGLE後看了维基还是看不懂它是啥 02/04 16:32
2F：→ carelai: 就是排中律(exclusion of middle）不成立的普通逻辑 02/04 16:51
3F：推 ppu12372: 所以他是重新建立的一套系统,可能是只适用在某些状况瞜? 02/04 16:54
4F：→ ppu12372: 不然你随便看一个直言命题,排中律都成立呀 02/04 16:54
5F：推 suhorng: @1F: constructive logic, intuitionistic logic 02/04 21:03
6F：→ carelai: 排中律有可能不成立的，比如命题：圆周率pi中含7个数字7 02/04 21:18
7F：→ carelai: 的连续串。这个命题现在无法证明是真是假。 02/04 21:19
8F：推 ppu12372: 可是即使这个命题无法被证明,也没证明排中律不成立呀 02/04 21:28
排中律成不成立是依照不同的逻辑来说的，单纯就 forall P . P v ~ P 来说，
在构造式逻辑下是不成立的，验证的方式可以透过构造式逻辑的模型来判断。
例如由 实数的开集合跟交集联集 形成的代数结构，可作为构造式逻辑的模型，
A -> B 则是取「 A^c 联集 B 的 interior set」。那麽 ~P 则诠释成「 P -> 空集合」
也就是 A^c 的 interior set。在这个模型下可以看出排中律并不恒真。
9F：推 rossignols: （下列的说明可能不够精确）就我所知，构造逻辑的起 02/06 02:30
10F：→ rossignols: 源跟一些数学家对於「数学证明要长什麽样子，数学的 02/06 02:31
11F：→ rossignols: 基础才够稳固」的立场有关。有些数学家认为，有几分 02/06 02:31
12F：→ rossignols: 证据才能说几分话，想说P有证明，就要直接给出P的证 02/06 02:31
13F：→ rossignols: 明，不能用「非P没有证明所以P有证明」这种迂回的方 02/06 02:32
14F：→ rossignols: 式。非P没有证明，不能保证P一定有证明。 02/06 02:32
15F：→ rossignols: 构造逻辑没有要证明排中律不成立，而是，基於某些数 02/06 02:32
16F：→ rossignols: 学家对於「数学证明该长什麽样子的期望」，经过一些人 02/06 02:33
17F：→ rossignols: 研究後发现，要拒绝排中律，才能得到一套能够用来捕 02/06 02:33
18F：→ rossignols: 捉「那些数学家心中理想的数学证明」的逻辑系统。 02/06 02:33
19F：推 ppu12372: 如果是这样的话,那那些数学家也太一厢情愿了,只是感觉 02/06 13:08
20F：→ ppu12372: 反证法怪怪的就认为不该用,如果没有反证法,那非欧几何 02/06 13:09
21F：→ ppu12372: 就不会存在了,没有非欧几何,相对论也无法存在了 02/06 13:10
22F：→ suhorng: 为何阿? 这个怎麽推论的? 02/06 18:26
23F：推 rossignols: 这些数学家之所以持这样的立场，背後是有他们的考量 02/06 21:13
24F：→ rossignols: 的，不过因为我才疏学浅，不确定要怎麽讲述他们的考量 02/06 21:15
25F：→ rossignols: ，才不会让他们看起来很蠢或一厢情愿。 02/06 21:15
26F：→ rossignols: （我不确定构造逻辑的起源跟哥德尔不完备定理有没有 02/06 21:15
27F：→ rossignols: 关系，但，或许看了以下的说法会让你比较不那麽反感他 02/06 21:15
28F：→ rossignols: 们的立场？）哥德尔的不完备定理说，如果一个系统够强 02/06 21:16
29F：→ rossignols: （例如皮亚诺算数就够强），那麽在那个系统里，就会 02/06 21:16
30F：→ rossignols: 有一些为真的陈述P无法证明出来。难道我们要因为那个 02/06 21:17
31F：→ rossignols: 为真的陈述P没有证明，就说非P有证明吗？ 02/06 21:17
32F：→ rossignols: 在古典逻辑里，有些用反证法证出来的句子，其实不用 02/06 21:18
33F：→ rossignols: 反证法也证得出来，不过证明过程可能会比较复杂麻烦一 02/06 21:18
34F：→ rossignols: 点。 02/06 21:19
35F：推 rossignols: 我不确定拿哥德尔的不完备定理来说明这些数学家的考量 02/06 21:31
36F：→ rossignols: 合不合适。但总之，这些数学家的考量是，他们要的是「 02/06 21:31
37F：→ rossignols: 构式」的数学（跟我们数学教育里的建构式数学大概没 02/06 21:31
38F：→ rossignols: 啥关系），数学成果必须是一砖一瓦结结实实地盖上去 02/06 21:32
39F：→ rossignols: 的，这样他们才安心。 02/06 21:32
40F：→ rossignols: 漏字了：他们要的是「建构式」的数学 02/06 21:33
41F：推 ppu12372: 我认为你的说法依然无法表达出他们的考量,有一些为真的 02/06 23:33
42F：→ ppu12372: 陈述P无法证明出来,那麽如果运用了排中律,你只能说 02/06 23:35
43F：→ ppu12372: [陈述P可证]该命题为假,而不会说非P可证 02/06 23:37
44F：→ ppu12372: 我想如果我想了解他们的考量的话可能得去参考相关书籍吧 02/06 23:38
45F：推 rossignols: 我目前认为，这可能跟我们是在哪个层面上谈排中律有 02/07 01:39
46F：→ rossignols: 关。有一种对「P或非P」的诠释是，「要嘛P有证明，要 02/07 01:39
47F：→ rossignols: 嘛非P有证明」。采建构式的数学家不接受「要嘛P有证 02/07 01:40
48F：→ rossignols: 明，要嘛非P有证明」是不证自明的，所以在构造逻辑的 02/07 01:40
49F：→ rossignols: 系统里自然不允许排中律。 02/07 01:41
50F：→ rossignols: 逻辑系统里的排中律的意义，跟一般日常生活中使用的 02/07 01:41
51F：→ rossignols: 排中律的意义，可能不太一样。 02/07 01:41
另一个说法是，构造式逻辑具有计算意义，能够用构造式逻辑证明的描述，
自然就能够将目标造出来，要证明所有的自然数都可以写成 2n + k, k = 0, 1
自然就是给一个型式的构造，说明如何给定任意自然数，都能够推算成以上的形式。
这在当今逻辑的应用领域——形式验证——占了举足轻重的地位。
52F：推 ppu12372: 有道理,在你重新阐述他们对排中律的定义後我就大概能 02/07 11:51
53F：→ ppu12372: 理解他们的考量了 02/07 11:51
54F：→ ppu12372: 话说我在想构造逻辑中"排中律"的定义是否和形式逻辑中 02/07 11:54
55F：→ ppu12372: 的"排中律"的定义有些微的不同? 02/07 11:54
两者排中律的形式是一样的。另外补充一点，事实上我们可以将古典逻辑的语句
透过 Double-negation translation 翻译成构造式逻辑的语句，那麽当一个
语句是古典下恒真 iff 该翻译的语句是构造式恒真
也就是说，构造式逻辑是比古典逻辑还要更精微的语言，
而古典逻辑下不能够分辨可不可构造。
--
※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 85.180.232.188
※ 文章网址: https://webptt.com/cn.aspx?n=bbs/logic/M.1423435804.A.7CF.html
※ 编辑: xcycl (85.180.232.188), 02/09/2015 06:50:23