作者znmkhxrw (QQ)
看板Math
标题[分析] 构造/非构造式证明
时间Thu Aug 4 23:16:53 2022
想用下面这个例子询问一下如标题的问题:
令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拿来用...)来描述
有关於这区别的专有名词吗
谢谢~
--
※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 59.102.225.191 (台湾)
※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1659626215.A.35B.html
1F：推 Vulpix : 不过你可以把n^2/2拿去看看介於哪两个完全平方数之 08/04 23:42
2F：→ Vulpix : 间啊。08/04 23:42
V大你是说其中一种b_n的造法吧?
还是说a_n可以改写成这样?
又或是说我的问题变成 "实务上如何实作a_n" ?
3F：推 Vulpix : 这是造a_n分母的方法啊。08/04 23:47
4F：→ Vulpix : 例如25/2介於9和16之间，分母就是3。08/04 23:49
5F：→ Vulpix : a_5的分母是3。08/04 23:50
对耶...这样造a_n分母的方法跟其中一种b_n根本一模一样XD
所以a_n算是...对的但是多此一举的造法XD?
6F：推 LPH66 : V 大的做法和你的做法的差别在於他把 r 的定义写进08/04 23:55
7F：→ LPH66 : 做法了, 但你的就只有「令 r 是这个无理数08/04 23:56
8F：→ LPH66 : 然後求此式」, 实际上要怎麽计算你得依照定义去求08/04 23:56
9F：→ LPH66 : 现在你的 r 只有开根号所以还好办08/04 23:57
10F：→ LPH66 : 如果是其他定义的话你要怎麽实际去算出来?08/04 23:57
11F：推 LPH66 : 至於有点题外, 你提的「电脑能算」数学上有个定义叫08/04 23:59
12F：→ LPH66 : 「可计算性」, 表示存在演算法能求出任意逼近08/04 23:59
13F：→ LPH66 : 这跟你的问题稍微离了远一点就是 08/05 00:00
以根号2的例子来说, V大的做法(或是说是其中一种b_n)是"可计算性"
又可以说是给我这个a_n一种可计算性的算法
如果今天r是zeta(5)的话, 我这种a_n造法
目前是不可计算?
但是绝对是合逻辑的构造性证明?
应该说我想确定的名词是:
构造性证明又分可计算性跟不可计算性?
而迄今有演算法发表的都分类在"可计算性",
但不排除那些"不可计算性"的在未来会变"可计算"?
※ 编辑: znmkhxrw (59.102.225.191 台湾), 08/05/2022 00:06:17
14F：推 Vulpix : ζ(5)就用传统的级数定义喽。其实要凑出你的a_n也08/05 00:47
15F：→ Vulpix : 没有那麽难。对每个n，先找一个离ζ(5)够近的有理08/05 00:47
16F：→ Vulpix : 数，然後去算n/那个有理数，再拿其整数部分作为分08/05 00:47
17F：→ Vulpix : 母。08/05 00:47
18F：→ Vulpix : 只不过很多余而已……08/05 00:47
听你这麽说, 对於任何实数r, 如果已经有"可计算性"的构造有理数解q_n→r
则令 a_n := n/floor(n/q_n), 都可以得到a_n→r, 而且a_n也是可计算的
所以才说多此一举?
如果是这个意思我完全可以接受
只是我这篇想要的区别是:(以下正确吗?)
对於任何正实数r>0, a_n := n/floor(n/r) 都是构造解 -- (正确)
对於任何正实数r>0, a_n := n/floor(n/r) 都是可计算性 -- (未知)
而这个"未知"要变"正确"的话, 如果已经有"任何正实数都有可计算性解"这个定理
那就是正确的
我想要区分的就是以上这件事而已, 所以才说是名词定义问题(?
19F：推 Vulpix : 你的「实数」是什麽呢？是柯西数列或递增有界数列08/05 01:16
20F：→ Vulpix : 的等价类就直接抓一条数列来用，是区间套等价类就08/05 01:16
21F：→ Vulpix : 抓区间套的上下界来用，是戴德金切断也可以用区间08/05 01:16
22F：→ Vulpix : 找交集里的有理数做数列。不管你的实数是哪种都可08/05 01:16
23F：→ Vulpix : 以做出数列来啊。08/05 01:16
问到这边好像有点混乱...
还是说我最初的问题本来就没定义, 所以才导致我无法明确地讲出怪的点@@?
最初单纯就是: 我想要让电脑逼近任何实数r, 可是如果用a_n:= n/floor(n/r)
的话, 我根本还没拿到r(虽然已经存在), 所以a_n行不通
但是
逻辑上a_n这样的造法却是正确的
而之後你V大你上面的回答好像是在说
任何实数r, floor(n/r)都可以算出来
24F：推 arrenwu : 你想要证明什麽命题啊?08/05 01:33
目前应该是定义"问题"耶...就是我无法用
既有定义去描述
为什麽我觉得怪
举个极端的例子, 今天如果有个问题是:
请写出
演算法造出有理数列逼近ζ(exp(π)), ζ是zeta fucntion
我如果写: 令a_n := n/floor(n/ζ(exp(π)))
在数学上是100分, 但是在实作上是0分, 因为拿不到floor(n/ζ(exp(π)))
除非我又去补充
floor(n/ζ(exp(π)))的演算法
25F：推 arrenwu : 从你写的问题看起来，是数值分析问题？08/05 04:56
26F：→ arrenwu : 也就是「求 zeta(exp(π))的有理数估计值以及误差08/05 04:57
27F：→ arrenwu : 范围」？08/05 04:57
28F：→ arrenwu : 然後是要能实现在计算机上的演算法？ 08/05 04:58
确实如果能 " 证明所有实数都有
计算机上的演算法逼近 "--(●)
那我原文造的a_n也就很容易写出演算法实现(由上述定理演算法先逼近r, 之後trivial)
如果(●)这个叙述是有定义而且正确的, 那就能缓解我所谓的
" a_n逻辑是对的但实作(for any real number)很怪 "的感觉
※ 编辑: znmkhxrw (59.102.225.191 台湾), 08/05/2022 05:12:22
29F：→ recorriendo : Computable reals 可以严谨定义啊08/05 15:44
30F：→ recorriendo : 程式只有可数无穷多 当然会有不可计算的实数08/05 15:46
理解~
31F：→ PPguest : 有没有可能是这样写比精简?反正floor(n/r)如V大所说08/05 16:43
32F：→ PPguest : 有方法可以知道.看到这种东西让人觉得头好痛,也想问08/05 16:45
33F：→ PPguest : 作者这样写到底是什麽意思?有什麽特别的作用?08/05 16:45
34F：→ 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), 於是才有"很怪"的感觉
35F：推 sunev : 存在不代表可计算啊08/05 17:29
36F：推 arrenwu : 你那个很怪的感觉来自於「不是很清楚在计算机上面 08/05 20:36
37F：→ arrenwu : 怎麽实作这些数值分析方法」 08/05 20:36
38F：→ arrenwu : 不妨去找些入门的书或影片看？ 08/05 20:36
39F：→ PPguest : 看起来是我想太多,以为a_n也是资料教你逼近的方式 08/05 20:46
40F：→ PPguest : 要区分a_n和b_n,我也不知道有什麽专有名词.08/05 21:30
41F：→ PPguest : 不过你提到的"2^0.5的逼近方法",感觉有一点不明确08/05 21:30
42F：→ PPguest : 我会脑补成"求2^0.5的10进位表示法到小数第几位",08/05 21:30
43F：→ PPguest : 资料教的逼近方式b_n直观上大概就是指这个问题的08/05 21:31
44F：→ PPguest : 演算法(的一部分,因为还要决定n要到多大才能停),08/05 21:31
45F：→ PPguest : 但a_n却不是.08/05 21:31
46F：→ PPguest : a_n如果直接照着用电脑实做的话,感觉第一步是把r08/05 21:31
47F：→ PPguest : 存成浮点数,但这步基本上就是我们要求的.08/05 21:32
48F：→ PPguest : 感觉我只是用我自己的话在讲你也知道的事情.08/05 21:32
我觉得除非我定义"怪" 不然叙述起来都很模棱两可XD
谢谢各位的讨论~
※ 编辑: znmkhxrw (59.102.225.191 台湾), 08/05/2022 21:48:04
49F：推 arrenwu : 不用想这麽复杂啊 你的问题其实是在数值方法上08/05 21:51
50F：→ cuylerLin : 纯推其他人的讨论XD 来来回回看了好几次，完全不知 08/05 22:22
51F：→ cuylerLin : 道这篇问题中文到底想问什麽...... 08/05 22:22
52F：推 LPH66 : 上面有人提了可计算的实数只有可数多个08/06 04:37
53F：→ LPH66 : 所以你的问题应该是在描述中你说「实数」的地方08/06 04:37
54F：→ LPH66 : 实际上应该要用「可计算实数」才对 08/06 04:37
55F：→ LPH66 : 至於最一开始你的困惑应该是在於一个有点循环递回 08/06 04:38
56F：→ LPH66 : 的性质: 你想找一个演算法算某个实数, 但你想用的 08/06 04:39
57F：→ LPH66 : 演算法却依赖於这个实数本身的计算结果 08/06 04:39
58F：→ LPH66 : 这个除了另循他法外打不破的循环递回可能才是08/06 04:40
59F：→ LPH66 : 最一开始你的疑问的问题所在08/06 04:40
对对对!! 我一开始的问题就是L大你推文的第二段, 之後板友的举例一些实数r都可<计算
>floor(nr)後, 才让我朝着你推文第一段的方向问: 是否所有实数都能<计算>floor(nr)
回到标题的话, 对於那些<不可计算>的实数, floor(nr)就是存在性证明而非构造性证明
罗?
https://en.m.wikipedia.org/wiki/Constructive_proof
wiki看起来好像也没正式定义, 但是有感觉, 但又有模糊的空间
比如有上界的实数子集S都有确上界supS, 那我写出supS时算是构造式吗? 如果是的话,
那对於那些存在性证明的元素我都给他一个符号x就说他是构造式, 这样很怪
如果不是的话, 代表构造式证明要可以算, 那不就是<可计算>了?
总结来说, 是否:
(1) 构造式证明=可计算
(2) 那些不可计算的实数r, 证明中写出floor(nr)就不算是构造性证明
※ 编辑: znmkhxrw (114.137.52.114 台湾), 08/06/2022 10:31:26
60F：→ PPguest : 如果要证明对於某个实数r,存在一个数列收敛到r 08/06 12:20
61F：→ PPguest : a_n:= n/(floor(n/r))是存在性证明还是构造性证明? 08/06 12:22
62F：→ PPguest : 感觉就很构造性证明啊?08/06 12:22
这就是我上面那段疑惑的地方了:
<不可计算>的实数r, 其floor(nr)算是构造式吗?
是或不是我都有办法反驳自己...
※ 编辑: znmkhxrw (111.255.12.5 台湾), 08/06/2022 14:04:18
63F：→ PPguest : 我的话大概就不会去管 构造性证明 和 可计算性08/06 14:52
64F：→ PPguest : a_n和b_n的区别,一句话来说,不是每一个收敛到r的数08/06 14:54
65F：→ PPguest : 列都能用在r的求值问题,感觉稍微把数列和求值问题的08/06 14:57
66F：→ PPguest : 方法给分开一些.08/06 14:57
对! 而且如同推文说的, 只要存在一个可计算的b_n, 那a_n的分母其实就把b_n拿来用就
一定是可计算性了XD
我会去管构造性证明以及用他下标题是因为脑中原本就有这个名词的印象 而遇到<能不能
计算>的问题时勾起了我这个印象 就去思考彼此的关系
※ 编辑: znmkhxrw (111.255.12.5 台湾), 08/06/2022 18:00:32
70F：→ xcycl : 这篇把构造式数学讲得很清楚 08/09 02:51
71F：→ xcycl : 这篇是专业的数学家深入浅出讲得很好 08/09 02:52
72F：→ xcycl : 不要浪费时间看上面业余的解释了 08/09 02:52
73F：→ xcycl : （我指的是上面的推文） 08/09 02:53
74F：推 LPH66 : 要讲不可计算的实数也有像经典的柴廷常数 08/09 03:10
75F：→ LPH66 : (给定程式语言, 随机一个该语言程式停机的机率) 08/09 03:10
76F：推 hwanger : 可是原PO问的是一般的Constructive proof 也就是维 08/09 06:26
77F：→ hwanger : 基中的 effective proof 08/09 06:27
78F：→ hwanger : 不是指只能在constructive mathematics下有效的证 08/09 06:29
79F：→ hwanger : 明 08/09 06:29
80F：推 hwanger : 也就上面业余解释中提到的 08/09 06:40
81F：→ hwanger : 除非真的到 "建构主义者" 所坚持的地步 08/09 06:41
82F：推 hwanger : 最简单的区分是 effective proof造出想要的物件後 08/09 06:45
83F：→ hwanger : 为了证明满足所需的条件 有时会用 xcycl 提供的文章 08/09 06:47
84F：→ hwanger : 一开头就禁用的排中律 08/09 06:49
85F：推 hwanger : effective proof 的目的是上面业余解释中提到的 08/09 06:54
86F：→ hwanger : 透过造出满足 P 的 x 来证明该命题成立 08/09 06:55
87F：→ hwanger : 不是把底层逻辑全部打掉重来 08/09 06:57
88F：推 hwanger : 不过我本来就没打算给什麽专业的解释就是了 正如上 08/09 07:17
89F：→ hwanger : 面业余解释提到的 08/09 07:18
90F：→ hwanger : 毕竟 constructive proof 这个概念 在大部份的时候 08/09 07:19
91F：→ hwanger : 只是一种启发性的想法 08/09 07:19
92F：→ hwanger : 上面业余的解释就单纯解释为什麽不可计算的 08/09 07:22
93F：→ hwanger : floor function 为什麽可以出现在一般的 08/09 07:23
94F：→ hwanger : constructive proof中 08/09 07:24
95F：→ hwanger : 而不是为了像 x大所提供的文章中一样 探讨 08/09 07:29
96F：→ hwanger : Archimedean property 在建构主义中有不有效 08/09 07:29
97F：推 hwanger : 所以上面的业余解释才会提到 08/09 07:33
98F：→ hwanger : 如果能够接受 Archimedean property 是一个 "足够 08/09 07:33
99F：→ hwanger : 直观" 的性质的话 08/09 07:34
100F：推 hwanger : 虽然可能是业余的书籍 不过可以参考一下 08/09 07:58
101F：→ hwanger : A Transition to Advanced Mathematics, Smith, 08/09 07:58
102F：→ hwanger : Eggen, Andre 中的 strategies for constructing 08/09 08:00
103F：→ hwanger : proof 一节 08/09 08:00
104F：推 hwanger : 上面打错 应该是 proofs involving qualifiers 一节 08/09 08:17
105F：推 hwanger : 回过神来才发现 被牵着鼻子走了 上面那篇业余的文章 08/09 08:29
106F：→ hwanger : 是在讲 constructive proofs 又不是在讲 08/09 08:30
107F：→ hwanger : constructive mathematics 我又不需要向专业的数学 08/09 08:31
108F：→ hwanger : 家解释这两个只是都有 constructive 这个单字的概念 08/09 08:33
109F：→ hwanger : 为什麽不同 08/09 08:34
110F：→ xcycl : 我不大确定你想的「一般的构造式证明」有没有定义 08/09 10:18
111F：→ xcycl : 构造式数学是完全可以当作数学理论来讨论 08/09 10:18
112F：→ xcycl : 不是一开始还在探索的哲学概念（或者说「主义」） 08/09 10:20
113F：→ xcycl : 当然没受过相关教育或训练的人不会晓得很正常 08/09 10:20
114F：→ xcycl : 原 po 说了想问这方面的专业知识，那这些「启发」性 08/09 10:23
115F：→ xcycl : 的想法不就是来乱的吗？ 08/09 10:24
116F：推 hwanger : 所谓的 "一般的构造式证明" 就像 08/09 10:38
118F：→ hwanger : 中的 3.5 Proof by construction 所述的 就只是某一 08/09 10:40
119F：→ hwanger : 类的证明技巧 我们顶多就只能如那篇业余的文章 大概 08/09 10:42
120F：→ hwanger : 抓住那个感觉 很难给个定义 08/09 10:43
121F：→ hwanger : 可是偏偏在数学上大部份的时间里 我们指一个证明是 08/09 10:46
122F：→ hwanger : Constructive proof 就是指 Proof by construction 08/09 10:47
123F：→ hwanger : 如果原PO是想问为什麽他的证明是在 constructive 08/09 10:50
124F：→ hwanger : mathematics 中是有效的 那就是我错误地假设了原PO 08/09 10:51
125F：→ hwanger : 的Constructive proof 的意义 08/09 10:53
126F：→ hwanger : 我那篇业余文章中就假设了 ZF 集合论 所以本来就不 08/09 10:54
127F：→ hwanger : 是为了解释那些只在 constructive mathematics 有效 08/09 10:55
128F：→ hwanger : 的证明 08/09 10:56
129F：推 hwanger : 那如果是这麽严格意义的Constructive proof 那英文 08/09 10:59
130F：→ hwanger : 维基中是有明确定义的 08/09 11:00
131F：→ hwanger : a proof that is valid in constructive mathematic 08/09 11:00
132F：→ hwanger : 另外可看 08/09 11:02
134F：→ hwanger : proof 条目 我还蛮确定这些启发性的想法不是来乱的 08/09 11:05
135F：推 xcycl : 原 po 都问到电脑能不能算，不是暧昧不明的 proof 08/09 11:06
136F：→ xcycl : by construction 了。 08/09 11:06
137F：推 hwanger : 如果真如 xcycl 你所言的 就是想问证明是否在 08/09 12:05
138F：→ hwanger : constructive mathematics 有效那也OK呀 只是一开始 08/09 12:05
139F：→ hwanger : 的问题就不存在了 因为constructive mathematics又 08/09 12:07
140F：→ hwanger : 没限定只能研究可以计算的东西 08/09 12:07
141F：推 hwanger : 另外就是因为暧昧不明的 proof by construction 常 08/09 12:10
142F：→ hwanger : 常会给人一种证明就是演算法的感觉 才会想问电脑不 08/09 12:11
143F：→ hwanger : 能算的 还能算是"一般的"建构式证明吗 08/09 12:12
144F：推 hwanger : 当然後面这个"常见"的问题是我对原文内容的超译 毕 08/09 12:16
145F：推 hwanger : 竟只有你才看得懂原文想问什麽 08/09 12:19
146F：→ xcycl : 「一开始的问题」是指什麽？ 08/09 12:35
147F：→ xcycl : 如果是古典数学的实数，那用 negative translation 08/09 12:36
148F：推 hwanger : 另外再提一点无关紧要的事 正如 xcycl 所提供的文章 08/09 12:36
149F：→ xcycl : 翻译到构造式数学上讨论 08/09 12:37
150F：→ hwanger : 所述的 因为constructive mathematics只有放弃排中 08/09 12:38
151F：→ hwanger : 律 所以并不是所有在constructive mathematics中的 08/09 12:39
152F：→ hwanger : 证明都是proof by construction 08/09 12:40
153F：→ xcycl : 我不想重复论文上面说的，那篇写得也没有很难 08/09 12:44
154F：推 hwanger : 正如上面那篇业余的文章所述 我本来就看不懂「一开 08/09 12:45
155F：推 hwanger : ??? 我又没有要你重复文章里面的东西 又不是只有你 08/09 12:47
156F：→ hwanger : 读过 constructive mathematics 我只是陈述并不是 08/09 12:48
157F：→ hwanger : 所有在constructive mathematics中的证明都是 08/09 12:49
158F：→ hwanger : proof by construction 这又不是你那篇文章中有提到 08/09 12:50
159F：→ hwanger : 到的观念 08/09 12:50
160F：→ hwanger : 正如上面那篇业余的文章所述 我本来就看不懂「一开 08/09 12:51
161F：→ hwanger : 始的问题」 我是从後来的讨论去想原po想问什麽 08/09 12:52
162F：推 hwanger : 不过如前所述 如果考虑constructive mathematics 08/09 12:55
163F：→ hwanger : "(1) 构造式证明=可计算 "不会是一个问题 08/09 12:56
164F：→ hwanger : 因为constructive mathematics又没限制只能研究可以 08/09 12:58
165F：→ hwanger : 计算的东西 08/09 12:58
哇...x大跟h大你们的讯息量太多了, 我吸收一下再回应, 谢谢!
166F：推 hwanger : 不过一样 这些都是我的超译 如果 xcycl 你想 08/09 13:03
167F：→ hwanger : 把问题移到constructive mathematics 请尽管这麽做 08/09 13:05
168F：→ hwanger : 没有问题 毕竟只有你才有资格讲constructive math 08/09 13:06
169F：→ xcycl : 啊，抱歉，我原本说的「上面的推文」并不是针对 08/09 13:34
170F：→ xcycl : hwanger 而是整体推文看下来的，想说为什麽这麽激烈 08/09 13:35
171F：→ xcycl : 才想到我是接在 hwanger 下回的，有这层意思 08/09 13:36
172F：推 hwanger : 呃...上面的争论也就只是对 constructive proof的定 08/09 14:50
173F：→ hwanger : 义有不同的观点...毕竟不论哪个 floor function都是 08/09 14:52
174F：→ hwanger : 可以用的 08/09 14:53
175F：推 cuylerLin : x大别在意XD 他也不是第一次脑补错误假设和态度激烈 08/09 15:46
176F：→ cuylerLin : 了......过来人路过（菸） 08/09 15:46
178F：→ hwanger : webptt.com/cn.aspx?n=bbs/Math/M.1599859449.A.B4F.html 08/09 17:38
179F：→ PPguest : 感觉8/6前的推文大家似乎都避开讨论这篇的标题XD 08/09 20:05
180F：→ PPguest : ^不 08/09 20:07
181F：→ recorriendo : 因为不知道原Po到底想问什麽(其实我到现在还是不知 08/10 13:01
182F：→ recorriendo : 道 08/10 13:01
183F：推 LPH66 : 我觉得甚至原 PO 自己也不是真的很清楚他的问题 08/10 18:41
184F：→ LPH66 : 到底在哪里...「可计算性」这个名词我很前面有推过 08/10 18:41
185F：→ LPH66 : 但当时我以为那和他的问题所在有一点远 08/10 18:41
186F：→ LPH66 : 是在这之後来回讨论了好几次之後才发现 08/10 18:42
187F：→ LPH66 : 原来他的问题里面可能还有这麽一层在 08/10 18:42
188F：→ LPH66 : 所以才有我在六号时的推文说一开始他有可能卡在那里 08/10 18:43
189F：→ LPH66 : 会以为有点远的原因其实跟他原文叙述有关: 08/10 18:45
190F：→ LPH66 : 这篇标题以及他的叙述是在讲「构造式证明」 08/10 18:45
191F：→ LPH66 : 跟「可计算性」是好像有点有关但又好像不太一样 08/10 18:46
192F：→ LPH66 : (或者可能他口中的这种「构造」其实就是演算法? 08/10 18:46
193F：→ LPH66 : 只是个猜测就是了啦) 所以才会大家都在困惑 08/10 18:47
194F：→ recorriendo : 我感觉get到一点原PO的症结点了 我认为是input/outp 08/10 20:48
195F：→ recorriendo : ut的问题 如果你手上已经有(或"构造"出)r的值 那当 08/10 20:49
196F：→ recorriendo : 然可以用这个方法构造出你要的数列 08/10 20:50
197F：→ recorriendo : 没有input的值 像h大的Re(ζ(–π+ie))一例 当然变 08/10 20:55
198F：→ recorriendo : 不出你要的序列 或许可以把原PO想要的"构造"定义成 08/10 20:56
199F：→ recorriendo : (1)整数可"构造" (2)给一演算法且input可"构造"则 08/10 20:58
200F：→ recorriendo : output也可"构造" 08/10 20:58
201F：→ recorriendo : 另外 你完全可以case by case证明特定floor(n/r)可 08/10 21:06
202F：→ recorriendo : "构造" 就算floor(x) in general不可"构造" 例如你 08/10 21:07
203F：→ recorriendo : 的原例floor(n/2^0.5)可以找到不需2^0.5值的演算法 08/10 21:10
204F：推 LPH66 : 如果是这种「构造」定义的话那其实就是可计算数了 08/11 02:30
回覆以上:
------------
没错就是我到目前认识的定义无法严格描述我的问题, 才导致总总猜测跟模棱两可
这里简短整理综合以上的资讯
<定义1>
构造性证明(constructive proof)有其严格定义
而非构造性证明称作存在性证明
<定义2>
可计算性有其严格定义, 又称做可构造性, 描述的对象是实数
<问题1> 以下关於《任何实数都存在有理数列逼近》的证明是构造性还是存在性证明
pf: 对任何实数r, 令a_n:=floor(nr)/n, 则a_n→r
<答案1> 构造性证明(具体原因涉及<定义1>)
<问题2> 对任何实数r, floor(nr)都可计算(采用<定义2>)
<答案2> 否! 只有可数个实数r其floor(nr)才可计算(具体原因涉及<定义2>)
而我目前是看成"有演算法 = 可计算性"
如果不是的话, 还要再定义何谓"有演算法", 问题又会有分支
就先不引入"演算法"这个词汇了
※ 编辑: znmkhxrw (59.102.225.191 台湾), 08/12/2022 02:16:41
205F：推 LPH66 : 「有演算法=可计算性」这玩意叫做 Church-Turing 08/12 17:58
206F：→ LPH66 : thesis, 目前大家都认为这个等号是对的 08/12 17:59
原来有这个名词, 谢谢L大~
※ 编辑: znmkhxrw (59.102.225.191 台湾), 08/18/2022 21:22:45