作者bluepal (艾利欧吕)
看板Math
标题Re: [分析] 构造/非构造式证明
时间Mon Aug 8 00:39:55 2022
※ 引述《znmkhxrw (QQ)》之铭言：
想用下面这个例子询问一下如标题的问题:
令r = 2^0.5
令a_n := n/(floor(n/r))
则我们知道a_n→r
那这样a_n算是2^0.5的构造性证明吗?
(或许要先定义采用的公设? 比如除法反元素与floor函数的存在性)
-----------------------------------------------------------
其实最初我想问的不知道怎麽下标题...
就是找"2^0.5的逼近方法", 一堆资料教你造递回/数列...的有理数逼近方式(假设叫b_n)
但是我问题就在於 a_n := n/(floor(n/r)) 也是一种逼近方式, 而且也是
有理数列
那b_n跟a_n就差在"
电脑能不能算"这个没定义的名词?
而a_n最大的不同是, 他把要逼近的r拿来用了
可是这步在逻辑上并没有错, 因为r本身存在了, 我只是要逼近他
我目前卡在
没有定义去区分a_n跟b_n有哪里不同
只能用一些
口述语言(电脑能不能算/把r拿来用...)来描述
有关於这区别的专有名词吗
谢谢~
1F：→ PPguest : 有没有可能是这样写比精简?反正floor(n/r)如V大所说08/05 16:43
2F：→ PPguest : 有方法可以知道.看到这种东西让人觉得头好痛,也想问08/05 16:45
3F：→ PPguest : 作者这样写到底是什麽意思?有什麽特别的作用?08/05 16:45
4F：→ PPguest : ^较08/05 16:47
我在上篇的问题中需要这个定理:
------------------------
令a_n是趋近於无穷大的正整数列
则对於任何正实数r, 都存在一条趋近於无穷大的正整数列b_n
使得a_n/b_n趋近於r
------------------------
证明就是取b_n = floor(a_n/r)就结束了
也就是因此, 我才看到a_n/b_n不就是一种趋近於r的有理数列吗
抑或是floor(nr)/n也是一种, 只要先有高斯函数的存在性
以上在数学逻辑都没有问题, 只是突然用实作逼近观点去想这件事, 发现我要藉助floor(
nr)逼近r, 但是我要藉助的东西却很难算(general r), 於是才有"很怪"的感觉
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
不好意思只留问题原意和原始问题。
*
证明无误，着眼点在存在性。
任何实数r本身可能为有理数或无理数，前者构造容易，後者由可前者建构。
*
你觉得怪的点应该在r为无理数时，因为写程式无法操作。
*
不过这样想就简明了：
如果r为无理数时程式完全可以操作
因为若"给定了"任何一个有理数r，最常见的给定方式是：
r=a/b, (a,b)=1, a和b为整数, b>0
当r为无理数时，如您所提2^0.5，程式无法按照你证明中的算式操作，
因为程式操作的都是有限步骤，然而b_n = floor(a_n/r)当中：
a_n/r，假设第一步a_0=1，光是1/(2^0.5)就无法以程式操作出无误差数字。
*
证明本身对於无理数之r正确，是因为先有了r的存在性，
给定任何实数r这句话本身，就隐含r存在，也存在着r的构造方式
(任何无理数皆可用有理数无穷数列逼近)，以2^0.5次方为例，
这个数字本身'2^0.5'其实仅是一种表达方式，表达一个数，存在性已证(由完备性)
而此数的性质是平方为2，此数也被认为该存在於数线上，
因此以完备性公理赋予其存在性，r的存在性才保证b_n中每个数字存在。
也就是说，b_n之所以存在，证明之所以成功，是仰赖给定了r，或是r的存在性。
然而很多存在性的证明都没有给构造方法(或说用程式操作方法)，例子太多了，
所以这个证明并不奇怪。
先证明了b_n存在性後，才依其存在性去构造b_n，数学上常见这样流程。
否则即使构造了一组数列，若b_n打从一开始就不可能存在，构造出的数列也不会
满足原条件。
*
其实完备性公理也只说了数线上那些"该存在的数字"，只要可以用有理数数列
逼近到误差比任何正有理数小，他就存在。不过那些"该存在的数字"，
在你给定这个数字同时，就是要给足它的资讯，像这里是该数的平方为2。
其他"该存在的数字"的资讯不枚盛举：
该数的某整数次方为某正整数
pi: 圆周长与直径长之比
e: 考虑以1/x从1开始积分的黎曼和，使其和为1的下界。
有了这个数字的等价资讯，才等同告知(给定)了该数字。
上述资讯的共同特徵都是可以用有理数来逼近，像2^0.5
可用最简单的十分逼近法以有理数逼近，得到 c_n(取递增数列c_0<2^0.5)
本题欲构造b_n = floor(a_n/r)，即可利用r=2^0.5之构造方法，取上述c_n
改令b'_n=floor(a_n/c_n)
因为集合{a_n/b_n}唯一limit point为r=2^0.5
且显见{a_n/b_n}之limit point(r=2^0.5) 亦为{a_n/b'_n}之limit point
因此由 a_n/b'_n 之极限亦为r
*上面的手法其实也是先利用了存在性的证明，来证明这个构造的结果有效。
此证明亦可以构造出r，只差在当初先做为前提的存在性要如何构造。
--
※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 203.204.39.221 (台湾)
※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1659890411.A.985.html
※ 编辑: bluepal (203.204.39.221 台湾), 08/08/2022 22:28:33
5F：推 znmkhxrw : 谢谢b大的分享 我吸收一下 谢谢 08/09 13:04
6F：→ bluepal : 上篇h大把我写的全包括进去了,而且用严谨数学符号 08/09 23:30
7F：→ bluepal : 还有更细致讨论,跟各种条件下的实数,因为叙述P太抽 08/09 23:30
8F：→ bluepal : 象,你可以取任给一个超越函数range中某element的 08/09 23:31
9F：→ bluepal : preimage中任挑一个元素(定义在复数的超越函数)的 08/09 23:32
10F：→ bluepal : real part当作给定实数... 08/09 23:32
11F：→ bluepal : 或是乱给一个存在classical solution的偏微分方程 08/09 23:33
12F：→ bluepal : 指定他的解作为刚才的超越函数...叙述怎麽写都行 08/09 23:34
13F：→ bluepal : 中间每次用到选择公理当然构造那个实数更不可能 08/09 23:34
14F：→ bluepal : 所以你的叙述比较象他说用十进位的类似柯西数列 08/09 23:35
15F：→ bluepal : 我觉得他写得很完整 08/09 23:36
16F：→ bluepal : x大讲的就是很正式的constructive proof 08/09 23:37
17F：→ bluepal : 很抱歉我本篇滥用'构造'这个名词 08/09 23:37
18F：→ bluepal : 存在性有了'数列建构'才可能对 08/09 23:43
19F：→ bluepal : 唯一性让'数列建构'的选择变多不用考虑跑掉 08/09 23:44
20F：→ bluepal : 最後数列要收敛,程式上还要保证误差 08/09 23:44
21F：→ bluepal : 其实用简单的fixed point定理想就是轮廓了 08/09 23:45
22F：→ bluepal : 问题好像也不是全然出在选择公理...h大点出你的诉求 08/09 23:52
23F：→ bluepal : 就是程式上可行(也许),所以就是最後能用那个十进位 08/09 23:53
24F：→ bluepal : 类似科西数列来表示每次证明中给出用到的数字的证明 08/09 23:55
25F：→ bluepal : 那就是证明中的每个步骤都要避免无法做到这点的 08/09 23:56
26F：→ bluepal : 和constructive proof也不是全然相同 08/09 23:56
27F：→ bluepal : 我这篇提到的也只有用数列建构特定r,重点也只有数列 08/09 23:59
28F：→ bluepal : 可是要证明中的每个步骤都用h大的形式好像才比较符 08/10 00:00
29F：→ bluepal : 合'程式可实作证明'(如果这是你要的) 08/10 00:00
30F：→ bluepal : 不过你标题和推文提到想了解constructive proof 08/10 00:01
31F：→ bluepal : 所以x大那篇就是很正式的 08/10 00:02
32F：→ bluepal : 那就看你需求...其他人的可以说都不用看XDDD 08/10 00:02
33F：→ bluepal : 最後就是...如果你要的也不是程式可实作'全部证明' 08/10 00:06
34F：→ bluepal : 只是想要用某个定理时,让程式可以跑出想要的结果 08/10 00:07
35F：→ bluepal : 那就不一定要在证明的时候要求'全部程式可实作' 08/10 00:07
36F：→ bluepal : 只要运用定理跑结果的时候可实作就好了 08/10 00:08
37F：→ bluepal : 也许根本是独立於证明的另一套演算法 08/10 00:08
38F：→ bluepal : 这里比较像想让证明本身可以拿来跑出结果,可是那个 08/10 00:09
39F：→ bluepal : r让你无法用这个证明跑结果 08/10 00:10
40F：→ bluepal : 如果是这样,其实就区分证明是否'可以拿来用程式跑结 08/10 00:10
41F：→ bluepal : 果出来' 08/10 00:10
42F：→ bluepal : 可否用证明程式跑结果出来,h大那边有完整讨论 08/10 00:11
43F：→ bluepal : 边想边打抱歉,打完我自己看也很头晕(?) 08/10 00:14
44F：→ bluepal : 总之我觉得h大观点比较全面性总结了除了x大以外的全 08/10 00:17
45F：→ bluepal : 部,看起来也比较像你想问的(?) 08/10 00:18
46F：→ bluepal : 我现在仔细看其他推文其实也都有问到重点,不过可能 08/10 00:27
47F：→ bluepal : 大家都很省话吧(?),所以都问得很扼要 08/10 00:28
48F：→ bluepal : constructive proof看起来是直接给出了可以拿来用的 08/10 00:29
49F：→ bluepal : 证明, 但他不一定可计算.... 08/10 00:29
50F：→ bluepal : 所以如果要的是可以拿来直接用,又是程式可以跑的 08/10 00:30
51F：→ bluepal : 就是两者交集...我是想说如果要便宜行事区分证明 08/10 00:30
52F：→ bluepal : 就把他区分成可不可以拿来现成用程式跑出结果的证明 08/10 00:31
53F：→ bluepal : 如果纯应用的话..其实只要考虑有没有对应的演算法就 08/10 00:31
54F：→ bluepal : 好,知道已经被证明了也不用管他证明... 08/10 00:32
55F：推 xcycl : Constructive proof 下写出来的证明就是可判定程式 08/10 07:54
56F：→ xcycl : 喔！ 08/10 07:54
57F：→ xcycl : 可判定程式指的是有限时间内可计算出结果的程式。 08/10 07:56
58F：推 xcycl : 但在直构逻辑内又可以证明所有的实数不可数，这一 08/10 08:54
59F：→ xcycl : 时难说明清楚，还是先去看点现代构造式数学的介绍 08/10 08:54
60F：→ xcycl : 搞懂点基础，不然迷糊仗打不完。 08/10 08:54
61F：→ bluepal : 谢谢x大说明,我还是不要碰这块了,原PO看你的就可 08/10 22:28
62F：→ bluepal : 光是那篇我就...觉得好可怕XDDD 08/10 22:47
63F：→ bluepal : Constructive...感觉是非人(?)在念的...朝拜 08/10 22:48
64F：→ bluepal : 自己END 08/10 22:53
66F：→ hwanger : 如果是指这一个 那 Constructive proof 的意义就不 08/11 10:05
67F：→ hwanger : 只是 proof by construction 而是要在特定的逻辑系 08/11 10:06
68F：→ hwanger : 统(如intuitionistic type theory)下的 proof by 08/11 10:08
69F：推 hwanger : construction 所以并不是单单 constructive math 中 08/11 10:12
70F：→ hwanger : 有效的证明 08/11 10:13
71F：推 hwanger : 毕竟constructive math中的流派很多 可参考 08/11 10:15
73F：→ hwanger : Constructive Mathematics中的第三节 08/11 10:17
74F：推 hwanger : 那可以解释为何我们一开始认知不同 我打从一开始就 08/11 10:22
75F：→ hwanger : 没想过是否能把证明转到特定的逻辑系统 很抱歉 08/11 10:23
76F：推 hwanger : 抱歉一时不察 请忽略上面有关proofs as programs的 08/11 13:50
77F：→ hwanger : 连结 太久没碰 忘了这其实是在讲 Curry–Howard 08/11 13:52
78F：→ hwanger : correspondence 除了那个连结 其余的回文保持不变 08/11 13:55
79F：→ hwanger : 我用上面plato.standford中的这段话取代第一个连结 08/11 13:58
80F：→ hwanger : Every constructive proof embodies an algorithm 08/11 13:58
81F：→ hwanger : that, in principle, can be extracted and recast 08/11 13:59
82F：→ hwanger : as a computer program 08/11 14:00