精華 “等于”在數(shù)學(xué)中有多重含義
數(shù)學(xué)中有些概念相當(dāng)模糊難懂，但“等于”的意義似乎是我們已經(jīng)掌握的。然而，數(shù)學(xué)家們實(shí)際上并不完全同意什么構(gòu)成兩個事物的相等，這可能會對日益使用的計算機(jī)驗(yàn)證數(shù)學(xué)證明造成困擾。
這個學(xué)術(shù)爭議已經(jīng)持續(xù)了幾十年，但現(xiàn)在終于被提上日程，因?yàn)橛糜凇靶问交被蝌?yàn)證證明的計算機(jī)程序需要明確的、具體的指令，而不是模棱兩可的數(shù)學(xué)概念定義，這些概念定義在計算機(jī)缺乏的背景下容易被誤解。
英國帝國理工學(xué)院的數(shù)學(xué)家Kevin Buzzard在與計算機(jī)程序員合作時遇到了這個問題，這促使他重新審視“這是等于那”的定義，挑戰(zhàn)有關(guān)平等的各種合理口號。
Buzzard在arXiv服務(wù)器上的預(yù)印本中寫道：“六年前，我以為我理解了數(shù)學(xué)上的平等。我認(rèn)為它是一個定義明確的術(shù)語……然后我開始嘗試在計算機(jī)定理證明器中做碩士級別的數(shù)學(xué)，我發(fā)現(xiàn)平等是一個比我想象中更棘手的概念?！?/p>
等號(=)由威爾士數(shù)學(xué)家Robert Recorde于1557年發(fā)明，它優(yōu)雅地用兩條平行線表示放在兩邊的對象之間的對等關(guān)系。最初它并沒有流行起來，但隨著時間的推移，Recorde的直觀符號取代了拉丁詞組“aequalis”，并為計算機(jī)科學(xué)奠定了基礎(chǔ)。在其發(fā)明后的整整400年，等號首次作為計算機(jī)編程語言FORTRAN I的一部分被使用。
然而，平等的概念有更長的歷史，至少可以追溯到古希臘?，F(xiàn)代數(shù)學(xué)家在實(shí)踐中使用這個術(shù)語時“相當(dāng)松散”，Buzzard寫道。
在熟悉的用法中，等號建立了描述不相同數(shù)學(xué)對象代表相同價值或意義的方程，可以通過一些轉(zhuǎn)換和邏輯變換來證明。例如，整數(shù)2可以描述一對對象，1 + 1也可以。
但自19世紀(jì)末以來，數(shù)學(xué)家們使用了第二種平等定義，那時集合論出現(xiàn)了。
隨著集合論的發(fā)展，數(shù)學(xué)家對平等的定義也有所擴(kuò)展。像{1, 2, 3}這樣的集合可以被認(rèn)為與{a, b, c}這樣的集合“相等”，因?yàn)橐环N稱為規(guī)范同構(gòu)的隱含理解，它比較組結(jié)構(gòu)之間的相似性。
Buzzard告訴《新科學(xué)家》的Alex Wilkins：“這些集合以完全自然的方式相互匹配，數(shù)學(xué)家們意識到，假如我們也稱這些為相等會超級方便?！?/p>
然而，將規(guī)范同構(gòu)視為平等現(xiàn)在對試圖使用計算機(jī)形式化證明的數(shù)學(xué)家們造成了“真正的麻煩”，包括幾十年前的基礎(chǔ)概念。
Buzzard告訴Wilkins：“目前存在的任何[計算機(jī)]系統(tǒng)都無法捕捉像Grothendieck這樣的數(shù)學(xué)家使用等號的方式，”他指的是20世紀(jì)依靠集合論描述平等的領(lǐng)先數(shù)學(xué)家Alexander Grothendieck。
一些數(shù)學(xué)家認(rèn)為他們應(yīng)該重新定義數(shù)學(xué)概念，以正式將規(guī)范同構(gòu)等同于平等。
Buzzard不相同意。他認(rèn)為數(shù)學(xué)家與機(jī)器之間的不一致應(yīng)該促使數(shù)學(xué)家重新思考他們對像平等這樣基礎(chǔ)的數(shù)學(xué)概念的確切定義，以便計算機(jī)能夠理解它們。
Buzzard寫道：“當(dāng)一個人被迫寫下自己的真實(shí)意思，不能躲在那些定義不清的詞語背后時，有時會發(fā)現(xiàn)自己需要做更多的工作，甚至重新思考某些想法應(yīng)該怎么樣呈現(xiàn)?！?/p>
本文譯自 ScienceAlert，由 BALI 編輯發(fā)布。
內(nèi)容來自：愛掏網(wǎng)