[分析] 構造/非構造式證明

[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拿來用...)來描述

有關於這區別的專有名詞嗎

謝謝~

--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 59.102.225.191 (臺灣)
※ 文章網址: https://www.ptt.cc/bbs/Math/M.1659626215.A.35B.html
推 Vulpix      : 不過你可以把n^2/2拿去看看介於哪兩個完全平方數之
→ Vulpix      : 間啊。
V大你是說其中一種b_n的造法吧?
還是說a_n可以改寫成這樣?

又或是說我的問題變成 "實務上如何實作a_n" ?

推 Vulpix      : 這是造a_n分母的方法啊。
→ Vulpix      : 例如25/2介於9和16之間，分母就是3。
→ Vulpix      : a_5的分母是3。
對耶...這樣造a_n分母的方法跟其中一種b_n根本一模一樣XD
所以a_n算是...對的但是多此一舉的造法XD?

推 LPH66       : V 大的做法和你的做法的差別在於他把 r 的定義寫進
→ LPH66       : 做法了, 但你的就只有「令 r 是這個無理數
→ LPH66       : 然後求此式」, 實際上要怎麼計算你得依照定義去求
→ LPH66       : 現在你的 r 只有開根號所以還好辦
→ LPH66       : 如果是其他定義的話你要怎麼實際去算出來?
推 LPH66       : 至於有點題外, 你提的「電腦能算」數學上有個定義叫
→ LPH66       : 「可計算性」, 表示存在演算法能求出任意逼近
→ LPH66       : 這跟你的問題稍微離了遠一點就是
以根號2的例子來說, V大的做法(或是說是其中一種b_n)是"可計算性"
又可以說是給我這個a_n一種可計算性的算法

如果今天r是zeta(5)的話, 我這種a_n造法目前是不可計算?
但是絕對是合邏輯的構造性證明?

應該說我想確定的名詞是: 構造性證明又分可計算性跟不可計算性?
而迄今有演算法發表的都分類在"可計算性",
但不排除那些"不可計算性"的在未來會變"可計算"?
※ 編輯: znmkhxrw (59.102.225.191 臺灣), 08/05/2022 00:06:17
推 Vulpix      : ζ(5)就用傳統的級數定義嘍。其實要湊出你的a_n也
→ Vulpix      : 沒有那麼難。對每個n，先找一個離ζ(5)夠近的有理
→ Vulpix      : 數，然後去算n/那個有理數，再拿其整數部分作為分
→ Vulpix      : 母。
→ Vulpix      : 只不過很多餘而已……
聽你這麼說, 對於任何實數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) 都是可計算性 -- (未知)

而這個"未知"要變"正確"的話, 如果已經有"任何正實數都有可計算性解"這個定理
那就是正確的

我想要區分的就是以上這件事而已, 所以才說是名詞定義問題(?

推 Vulpix      : 你的「實數」是什麼呢？是柯西數列或遞增有界數列
→ Vulpix      : 的等價類就直接抓一條數列來用，是區間套等價類就
→ Vulpix      : 抓區間套的上下界來用，是戴德金切斷也可以用區間
→ Vulpix      : 找交集裡的有理數做數列。不管你的實數是哪種都可
→ Vulpix      : 以做出數列來啊。
問到這邊好像有點混亂...
還是說我最初的問題本來就沒定義, 所以才導致我無法明確地講出怪的點@@?

最初單純就是: 我想要讓電腦逼近任何實數r, 可是如果用a_n:= n/floor(n/r)
              的話, 我根本還沒拿到r(雖然已經存在), 所以a_n行不通
              但是邏輯上a_n這樣的造法卻是正確的

而之後你V大你上面的回答好像是在說任何實數r, floor(n/r)都可以算出來

推 arrenwu     : 你想要證明什麼命題啊?
目前應該是定義"問題"耶...就是我無法用既有定義去描述為什麼我覺得怪
舉個極端的例子, 今天如果有個問題是:

請寫出演算法造出有理數列逼近ζ(exp(π)), ζ是zeta fucntion

我如果寫: 令a_n := n/floor(n/ζ(exp(π)))
在數學上是100分, 但是在實作上是0分, 因為拿不到floor(n/ζ(exp(π)))
除非我又去補充floor(n/ζ(exp(π)))的演算法

推 arrenwu     : 從你寫的問題看起來，是數值分析問題？
→ arrenwu     : 也就是「求 zeta(exp(π))的有理數估計值以及誤差
→ arrenwu     : 範圍」？
→ arrenwu     : 然後是要能實現在計算機上的演算法？
確實如果能 " 證明所有實數都有計算機上的演算法逼近 "--(●)
那我原文造的a_n也就很容易寫出演算法實現(由上述定理演算法先逼近r, 之後trivial)

如果(●)這個敘述是有定義而且正確的, 那就能緩解我所謂的
" a_n邏輯是對的但實作(for any real number)很怪 "的感覺
※ 編輯: znmkhxrw (59.102.225.191 臺灣), 08/05/2022 05:12:22
→ recorriendo : Computable reals 可以嚴謹定義啊
→ recorriendo : 程式只有可數無窮多 當然會有不可計算的實數
理解~

→ PPguest     : 有沒有可能是這樣寫比精簡?反正floor(n/r)如V大所說
→ PPguest     : 有方法可以知道.看到這種東西讓人覺得頭好痛,也想問
→ PPguest     : 作者這樣寫到底是什麼意思?有什麼特別的作用?
→ PPguest     :                    ^較
我在上篇的問題中需要這個定理:

------------------------
令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), 於是才有"很怪"的感覺

推 sunev       : 存在不代表可計算啊
推 arrenwu     : 你那個很怪的感覺來自於「不是很清楚在計算機上面
→ arrenwu     : 怎麼實作這些數值分析方法」
→ arrenwu     : 不妨去找些入門的書或影片看？
→ PPguest     : 看起來是我想太多,以為a_n也是資料教你逼近的方式
→ PPguest     : 要區分a_n和b_n,我也不知道有什麼專有名詞.
→ PPguest     : 不過你提到的"2^0.5的逼近方法",感覺有一點不明確
→ PPguest     : 我會腦補成"求2^0.5的10進位表示法到小數第幾位",
→ PPguest     : 資料教的逼近方式b_n直觀上大概就是指這個問題的
→ PPguest     : 演算法(的一部分,因為還要決定n要到多大才能停),
→ PPguest     : 但a_n卻不是.
→ PPguest     : a_n如果直接照著用電腦實做的話,感覺第一步是把r
→ PPguest     : 存成浮點數,但這步基本上就是我們要求的.
→ PPguest     : 感覺我只是用我自己的話在講你也知道的事情.
我覺得除非我定義"怪" 不然敘述起來都很模稜兩可XD
謝謝各位的討論~
※ 編輯: znmkhxrw (59.102.225.191 臺灣), 08/05/2022 21:48:04
推 arrenwu     : 不用想這麼複雜啊 你的問題其實是在數值方法上
→ cuylerLin   : 純推其他人的討論XD 來來回回看了好幾次，完全不知
→ cuylerLin   : 道這篇問題中文到底想問什麼......
推 LPH66       : 上面有人提了可計算的實數只有可數多個
→ LPH66       : 所以你的問題應該是在描述中你說「實數」的地方
→ LPH66       : 實際上應該要用「可計算實數」才對
→ LPH66       : 至於最一開始你的困惑應該是在於一個有點循環遞迴
→ LPH66       : 的性質: 你想找一個演算法算某個實數, 但你想用的
→ LPH66       : 演算法卻依賴於這個實數本身的計算結果
→ LPH66       : 這個除了另循他法外打不破的循環遞迴可能才是
→ LPH66       : 最一開始你的疑問的問題所在
對對對!! 我一開始的問題就是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
→ PPguest     : 如果要證明對於某個實數r,存在一個數列收斂到r
→ PPguest     : a_n:= n/(floor(n/r))是存在性證明還是構造性證明?
→ PPguest     : 感覺就很構造性證明啊?
這就是我上面那段疑惑的地方了:
<不可計算>的實數r, 其floor(nr)算是構造式嗎?

是或不是我都有辦法反駁自己...
※ 編輯: znmkhxrw (111.255.12.5 臺灣), 08/06/2022 14:04:18
→ PPguest     : 我的話大概就不會去管 構造性證明 和 可計算性
→ PPguest     : a_n和b_n的區別,一句話來說,不是每一個收斂到r的數
→ PPguest     : 列都能用在r的求值問題,感覺稍微把數列和求值問題的
→ PPguest     : 方法給分開一些.
對! 而且如同推文說的, 只要存在一個可計算的b_n, 那a_n的分母其實就把b_n拿來用就
一定是可計算性了XD

我會去管構造性證明以及用他下標題是因為腦中原本就有這個名詞的印象 而遇到<能不能
計算>的問題時勾起了我這個印象 就去思考彼此的關係
※ 編輯: znmkhxrw (111.255.12.5 臺灣), 08/06/2022 18:00:32
推 hwanger     : https://imgur.com/a/fOZ5L0N
推 hwanger     : https://imgur.com/ijkw9OS
→ xcycl       : https://doi.org/10.1090/bull/1556
→ xcycl       : 這篇把構造式數學講得很清楚
→ xcycl       : 這篇是專業的數學家深入淺出講得很好
→ xcycl       : 不要浪費時間看上面業餘的解釋了
→ xcycl       : （我指的是上面的推文）
推 LPH66       : 要講不可計算的實數也有像經典的柴廷常數
→ LPH66       : (給定程式語言, 隨機一個該語言程式停機的機率)
推 hwanger     : 可是原PO問的是一般的Constructive proof 也就是維
→ hwanger     : 基中的 effective proof
→ hwanger     : 不是指只能在constructive mathematics下有效的證
→ hwanger     : 明
推 hwanger     : 也就上面業餘解釋中提到的
→ hwanger     : 除非真的到 "建構主義者" 所堅持的地步
推 hwanger     : 最簡單的區分是 effective proof造出想要的物件後
→ hwanger     : 為了證明滿足所需的條件 有時會用 xcycl 提供的文章
→ hwanger     : 一開頭就禁用的排中律
推 hwanger     : effective proof 的目的是上面業餘解釋中提到的
→ hwanger     : 透過造出滿足 P 的 x 來證明該命題成立
→ hwanger     : 不是把底層邏輯全部打掉重來
推 hwanger     : 不過我本來就沒打算給什麼專業的解釋就是了 正如上
→ hwanger     : 面業餘解釋提到的
→ hwanger     : 畢竟 constructive proof 這個概念 在大部份的時候
→ hwanger     : 只是一種啟發性的想法
→ hwanger     : 上面業餘的解釋就單純解釋為什麼不可計算的
→ hwanger     : floor function 為什麼可以出現在一般的
→ hwanger     : constructive proof中
→ hwanger     : 而不是為了像 x大所提供的文章中一樣 探討
→ hwanger     : Archimedean property 在建構主義中有不有效
推 hwanger     : 所以上面的業餘解釋才會提到
→ hwanger     : 如果能夠接受 Archimedean property 是一個 "足夠
→ hwanger     : 直觀" 的性質的話
推 hwanger     : 雖然可能是業餘的書籍 不過可以參考一下
→ hwanger     : A Transition to Advanced Mathematics, Smith,
→ hwanger     : Eggen, Andre 中的 strategies for constructing
→ hwanger     : proof 一節
推 hwanger     : 上面打錯 應該是 proofs involving qualifiers 一節
推 hwanger     : 回過神來才發現 被牽著鼻子走了 上面那篇業餘的文章
→ hwanger     : 是在講 constructive proofs 又不是在講
→ hwanger     : constructive mathematics 我又不需要向專業的數學
→ hwanger     : 家解釋這兩個只是都有 constructive 這個單字的概念
→ hwanger     : 為什麼不同
→ xcycl       : 我不大確定你想的「一般的構造式證明」有沒有定義
→ xcycl       : 構造式數學是完全可以當作數學理論來討論
→ xcycl       : 不是一開始還在探索的哲學概念（或者說「主義」）
→ xcycl       : 當然沒受過相關教育或訓練的人不會曉得很正常
→ xcycl       : 原 po 說了想問這方面的專業知識，那這些「啟發」性
→ xcycl       : 的想法不就是來亂的嗎？
推 hwanger     : 所謂的 "一般的構造式證明" 就像
→ hwanger     : https://en.wikipedia.org/wiki/Mathematical_proof
→ hwanger     : 中的 3.5 Proof by construction 所述的 就只是某一
→ hwanger     : 類的證明技巧 我們頂多就只能如那篇業餘的文章 大概
→ hwanger     : 抓住那個感覺 很難給個定義
→ hwanger     : 可是偏偏在數學上大部份的時間裡 我們指一個證明是
→ hwanger     : Constructive proof 就是指 Proof by construction
→ hwanger     : 如果原PO是想問為什麼他的證明是在 constructive
→ hwanger     : mathematics 中是有效的 那就是我錯誤地假設了原PO
→ hwanger     : 的Constructive proof 的意義
→ hwanger     : 我那篇業餘文章中就假設了 ZF 集合論 所以本來就不
→ hwanger     : 是為了解釋那些只在 constructive mathematics 有效
→ hwanger     : 的證明
推 hwanger     : 那如果是這麼嚴格意義的Constructive proof 那英文
→ hwanger     : 維基中是有明確定義的
→ hwanger     : a proof that is valid in constructive mathematic
→ hwanger     : 另外可看
→ hwanger     : https://mathworld.wolfram.com 的 Constructive
→ hwanger     : proof 條目 我還蠻確定這些啟發性的想法不是來亂的
推 xcycl       : 原 po 都問到電腦能不能算，不是曖昧不明的 proof
→ xcycl       : by construction 了。
推 hwanger     : 如果真如 xcycl 你所言的 就是想問證明是否在
→ hwanger     : constructive mathematics 有效那也OK呀 只是一開始
→ hwanger     : 的問題就不存在了 因為constructive mathematics又
→ hwanger     : 沒限定只能研究可以計算的東西
推 hwanger     : 另外就是因為曖昧不明的 proof by construction 常
→ hwanger     : 常會給人一種證明就是演算法的感覺 才會想問電腦不
→ hwanger     : 能算的 還能算是"一般的"建構式證明嗎
推 hwanger     : 當然後面這個"常見"的問題是我對原文內容的超譯 畢
推 hwanger     : 竟只有你才看得懂原文想問什麼
→ xcycl       : 「一開始的問題」是指什麼？
→ xcycl       : 如果是古典數學的實數，那用 negative translation
推 hwanger     : 另外再提一點無關緊要的事 正如 xcycl 所提供的文章
→ xcycl       : 翻譯到構造式數學上討論
→ hwanger     : 所述的 因為constructive mathematics只有放棄排中
→ hwanger     : 律 所以並不是所有在constructive mathematics中的
→ hwanger     : 證明都是proof by construction
→ xcycl       : 我不想重複論文上面說的，那篇寫得也沒有很難
推 hwanger     : 正如上面那篇業餘的文章所述 我本來就看不懂「一開
推 hwanger     : ??? 我又沒有要你重複文章裡面的東西 又不是只有你
→ hwanger     : 讀過 constructive mathematics 我只是陳述並不是
→ hwanger     : 所有在constructive mathematics中的證明都是
→ hwanger     : proof by construction 這又不是你那篇文章中有提到
→ hwanger     : 到的觀念
→ hwanger     : 正如上面那篇業餘的文章所述 我本來就看不懂「一開
→ hwanger     : 始的問題」 我是從後來的討論去想原po想問什麼
推 hwanger     : 不過如前所述 如果考慮constructive mathematics
→ hwanger     : "(1) 構造式證明=可計算 "不會是一個問題
→ hwanger     : 因為constructive mathematics又沒限制只能研究可以
→ hwanger     : 計算的東西
哇...x大跟h大你們的訊息量太多了, 我吸收一下再回應, 謝謝!

推 hwanger     : 不過一樣 這些都是我的超譯 如果 xcycl 你想
→ hwanger     : 把問題移到constructive mathematics 請儘管這麼做
→ hwanger     : 沒有問題 畢竟只有你才有資格講constructive math
→ xcycl       : 啊，抱歉，我原本說的「上面的推文」並不是針對
→ xcycl       : hwanger 而是整體推文看下來的，想說為什麼這麼激烈
→ xcycl       : 才想到我是接在 hwanger 下回的，有這層意思
推 hwanger     : 呃...上面的爭論也就只是對 constructive proof的定
→ hwanger     : 義有不同的觀點...畢竟不論哪個 floor function都是
→ hwanger     : 可以用的
推 cuylerLin   : x大別在意XD 他也不是第一次腦補錯誤假設和態度激烈
→ cuylerLin   : 了......過來人路過（菸）
→ hwanger     : https://www.shorturl.at/gimP2
→ hwanger     : www.ptt.cc/bbs/Math/M.1599859449.A.B4F.html
→ PPguest     : 感覺8/6前的推文大家似乎都避開討論這篇的標題XD
→ PPguest     :                              ^不
→ recorriendo : 因為不知道原Po到底想問什麼(其實我到現在還是不知
→ recorriendo : 道
推 LPH66       : 我覺得甚至原 PO 自己也不是真的很清楚他的問題
→ LPH66       : 到底在哪裡...「可計算性」這個名詞我很前面有推過
→ LPH66       : 但當時我以為那和他的問題所在有一點遠
→ LPH66       : 是在這之後來回討論了好幾次之後才發現
→ LPH66       : 原來他的問題裡面可能還有這麼一層在
→ LPH66       : 所以才有我在六號時的推文說一開始他有可能卡在那裡
→ LPH66       : 會以為有點遠的原因其實跟他原文敘述有關:
→ LPH66       : 這篇標題以及他的敘述是在講「構造式證明」
→ LPH66       : 跟「可計算性」是好像有點有關但又好像不太一樣
→ LPH66       : (或者可能他口中的這種「構造」其實就是演算法?
→ LPH66       :  只是個猜測就是了啦) 所以才會大家都在困惑
→ recorriendo : 我感覺get到一點原PO的癥結點了 我認為是input/outp
→ recorriendo : ut的問題  如果你手上已經有(或"構造"出)r的值 那當
→ recorriendo : 然可以用這個方法構造出你要的數列
→ recorriendo : 沒有input的值 像h大的Re(ζ(–π+ie))一例 當然變
→ recorriendo : 不出你要的序列  或許可以把原PO想要的"構造"定義成
→ recorriendo : (1)整數可"構造" (2)給一演算法且input可"構造"則
→ recorriendo : output也可"構造"
→ recorriendo : 另外 你完全可以case by case證明特定floor(n/r)可
→ recorriendo : "構造" 就算floor(x) in general不可"構造"  例如你
→ recorriendo : 的原例floor(n/2^0.5)可以找到不需2^0.5值的演算法
推 LPH66       : 如果是這種「構造」定義的話那其實就是可計算數了
回覆以上:
------------

沒錯就是我到目前認識的定義無法嚴格描述我的問題, 才導致總總猜測跟模稜兩可
這裡簡短整理綜合以上的資訊

<定義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
推 LPH66       : 「有演算法=可計算性」這玩意叫做 Church-Turing
→ LPH66       : thesis, 目前大家都認為這個等號是對的
原來有這個名詞, 謝謝L大~
※ 編輯: znmkhxrw (59.102.225.191 臺灣), 08/18/2022 21:22:45