→ PPguest : 有沒有可能是這樣寫比精簡?反正floor(n/r)如V大所說08/05 16:43
→ PPguest : 有方法可以知道.看到這種東西讓人覺得頭好痛,也想問08/05 16:45
→ PPguest : 作者這樣寫到底是什麼意思?有什麼特別的作用?08/05 16:45
→ 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://www.ptt.cc/bbs/Math/M.1659890411.A.985.html
※ 編輯: bluepal (203.204.39.221 臺灣), 08/08/2022 22:28:33
推 znmkhxrw : 謝謝b大的分享 我吸收一下 謝謝 08/09 13:04
→ bluepal : 上篇h大把我寫的全包括進去了,而且用嚴謹數學符號 08/09 23:30
→ bluepal : 還有更細緻討論,跟各種條件下的實數,因為敘述P太抽 08/09 23:30
→ bluepal : 象,你可以取任給一個超越函數range中某element的 08/09 23:31
→ bluepal : preimage中任挑一個元素(定義在複數的超越函數)的 08/09 23:32
→ bluepal : real part當作給定實數... 08/09 23:32
→ bluepal : 或是亂給一個存在classical solution的偏微分方程 08/09 23:33
→ bluepal : 指定他的解作為剛才的超越函數...敘述怎麼寫都行 08/09 23:34
→ bluepal : 中間每次用到選擇公理當然構造那個實數更不可能 08/09 23:34
→ bluepal : 所以你的敘述比較象他說用十進位的類似柯西數列 08/09 23:35
→ bluepal : 我覺得他寫得很完整 08/09 23:36
→ bluepal : x大講的就是很正式的constructive proof 08/09 23:37
→ bluepal : 很抱歉我本篇濫用'構造'這個名詞 08/09 23:37
→ bluepal : 存在性有了'數列建構'才可能對 08/09 23:43
→ bluepal : 唯一性讓'數列建構'的選擇變多不用考慮跑掉 08/09 23:44
→ bluepal : 最後數列要收斂,程式上還要保證誤差 08/09 23:44
→ bluepal : 其實用簡單的fixed point定理想就是輪廓了 08/09 23:45
→ bluepal : 問題好像也不是全然出在選擇公理...h大點出你的訴求 08/09 23:52
→ bluepal : 就是程式上可行(也許),所以就是最後能用那個十進位 08/09 23:53
→ bluepal : 類似科西數列來表示每次證明中給出用到的數字的證明 08/09 23:55
→ bluepal : 那就是證明中的每個步驟都要避免無法做到這點的 08/09 23:56
→ bluepal : 和constructive proof也不是全然相同 08/09 23:56
→ bluepal : 我這篇提到的也只有用數列建構特定r,重點也只有數列 08/09 23:59
→ bluepal : 可是要證明中的每個步驟都用h大的形式好像才比較符 08/10 00:00
→ bluepal : 合'程式可實作證明'(如果這是你要的) 08/10 00:00
→ bluepal : 不過你標題和推文提到想了解constructive proof 08/10 00:01
→ bluepal : 所以x大那篇就是很正式的 08/10 00:02
→ bluepal : 那就看你需求...其他人的可以說都不用看XDDD 08/10 00:02
→ bluepal : 最後就是...如果你要的也不是程式可實作'全部證明' 08/10 00:06
→ bluepal : 只是想要用某個定理時,讓程式可以跑出想要的結果 08/10 00:07
→ bluepal : 那就不一定要在證明的時候要求'全部程式可實作' 08/10 00:07
→ bluepal : 只要運用定理跑結果的時候可實作就好了 08/10 00:08
→ bluepal : 也許根本是獨立於證明的另一套演算法 08/10 00:08
→ bluepal : 這裡比較像想讓證明本身可以拿來跑出結果,可是那個 08/10 00:09
→ bluepal : r讓你無法用這個證明跑結果 08/10 00:10
→ bluepal : 如果是這樣,其實就區分證明是否'可以拿來用程式跑結 08/10 00:10
→ bluepal : 果出來' 08/10 00:10
→ bluepal : 可否用證明程式跑結果出來,h大那邊有完整討論 08/10 00:11
→ bluepal : 邊想邊打抱歉,打完我自己看也很頭暈(?) 08/10 00:14
→ bluepal : 總之我覺得h大觀點比較全面性總結了除了x大以外的全 08/10 00:17
→ bluepal : 部,看起來也比較像你想問的(?) 08/10 00:18
→ bluepal : 我現在仔細看其他推文其實也都有問到重點,不過可能 08/10 00:27
→ bluepal : 大家都很省話吧(?),所以都問得很扼要 08/10 00:28
→ bluepal : constructive proof看起來是直接給出了可以拿來用的 08/10 00:29
→ bluepal : 證明, 但他不一定可計算.... 08/10 00:29
→ bluepal : 所以如果要的是可以拿來直接用,又是程式可以跑的 08/10 00:30
→ bluepal : 就是兩者交集...我是想說如果要便宜行事區分證明 08/10 00:30
→ bluepal : 就把他區分成可不可以拿來現成用程式跑出結果的證明 08/10 00:31
→ bluepal : 如果純應用的話..其實只要考慮有沒有對應的演算法就 08/10 00:31
→ bluepal : 好,知道已經被證明了也不用管他證明... 08/10 00:32
推 xcycl : Constructive proof 下寫出來的證明就是可判定程式 08/10 07:54
→ xcycl : 喔！ 08/10 07:54
→ xcycl : 可判定程式指的是有限時間內可計算出結果的程式。 08/10 07:56
推 xcycl : 但在直構邏輯內又可以證明所有的實數不可數，這一 08/10 08:54
→ xcycl : 時難說明清楚，還是先去看點現代構造式數學的介紹 08/10 08:54
→ xcycl : 搞懂點基礎，不然迷糊仗打不完。 08/10 08:54
→ bluepal : 謝謝x大說明,我還是不要碰這塊了,原PO看你的就可 08/10 22:28
→ bluepal : 光是那篇我就...覺得好可怕XDDD 08/10 22:47
→ bluepal : Constructive...感覺是非人(?)在念的...朝拜 08/10 22:48
→ bluepal : 自己END 08/10 22:53
→ hwanger : 如果是指這一個 那 Constructive proof 的意義就不 08/11 10:05
→ hwanger : 只是 proof by construction 而是要在特定的邏輯系 08/11 10:06
→ hwanger : 統(如intuitionistic type theory)下的 proof by 08/11 10:08
推 hwanger : construction 所以並不是單單 constructive math 中 08/11 10:12
→ hwanger : 有效的證明 08/11 10:13
推 hwanger : 畢竟constructive math中的流派很多 可參考 08/11 10:15
→ hwanger : Constructive Mathematics中的第三節 08/11 10:17
推 hwanger : 那可以解釋為何我們一開始認知不同 我打從一開始就 08/11 10:22
→ hwanger : 沒想過是否能把證明轉到特定的邏輯系統 很抱歉 08/11 10:23
推 hwanger : 抱歉一時不察 請忽略上面有關proofs as programs的 08/11 13:50
→ hwanger : 連結 太久沒碰 忘了這其實是在講 Curry–Howard 08/11 13:52
→ hwanger : correspondence 除了那個連結 其餘的回文保持不變 08/11 13:55
→ hwanger : 我用上面plato.standford中的這段話取代第一個連結 08/11 13:58
→ hwanger : Every constructive proof embodies an algorithm 08/11 13:58
→ hwanger : that, in principle, can be extracted and recast 08/11 13:59
→ hwanger : as a computer program 08/11 14:00