精華 “等于”在數(shù)學中有多重含義

數(shù)學中有些概念相當模糊難懂，但“等于”的意義似乎是我們已經(jīng)掌握的。然而，數(shù)學家們實際上并不完全同意什么構(gòu)成兩個事物的相等，這可能會對日益使用的計算機驗證數(shù)學證明造成困擾。

這個學術(shù)爭議已經(jīng)持續(xù)了幾十年，但現(xiàn)在終于被提上日程，因為用于“形式化”或驗證證明的計算機程序需要明確的、具體的指令，而不是模棱兩可的數(shù)學概念定義，這些概念定義在計算機缺乏的背景下容易被誤解。

英國帝國理工學院的數(shù)學家Kevin Buzzard在與計算機程序員合作時遇到了這個問題，這促使他重新審視“這是等于那”的定義，挑戰(zhàn)有關(guān)平等的各種合理口號。

Buzzard在arXiv服務(wù)器上的預印本中寫道：“六年前，我以為我理解了數(shù)學上的平等。我認為它是一個定義明確的術(shù)語……然后我開始嘗試在計算機定理證明器中做碩士級別的數(shù)學，我發(fā)現(xiàn)平等是一個比我想象中更棘手的概念。”

等號(=)由威爾士數(shù)學家Robert Recorde于1557年發(fā)明，它優(yōu)雅地用兩條平行線表示放在兩邊的對象之間的對等關(guān)系。最初它并沒有流行起來，但隨著時間的推移，Recorde的直觀符號取代了拉丁詞組“aequalis”，并為計算機科學奠定了基礎(chǔ)。在其發(fā)明后的整整400年，等號首次作為計算機編程語言FORTRAN I的一部分被使用。

然而，平等的概念有更長的歷史，至少可以追溯到古希臘。現(xiàn)代數(shù)學家在實踐中使用這個術(shù)語時“相當松散”，Buzzard寫道。

在熟悉的用法中，等號建立了描述不相同數(shù)學對象代表相同價值或意義的方程，可以通過一些轉(zhuǎn)換和邏輯變換來證明。例如，整數(shù)2可以描述一對對象，1 + 1也可以。

但自19世紀末以來，數(shù)學家們使用了第二種平等定義，那時集合論出現(xiàn)了。

隨著集合論的發(fā)展，數(shù)學家對平等的定義也有所擴展。像{1, 2, 3}這樣的集合可以被認為與{a, b, c}這樣的集合“相等”，因為一種稱為規(guī)范同構(gòu)的隱含理解，它比較組結(jié)構(gòu)之間的相似性。

Buzzard告訴《新科學家》的Alex Wilkins：“這些集合以完全自然的方式相互匹配，數(shù)學家們意識到，假如我們也稱這些為相等會超級方便。”

然而，將規(guī)范同構(gòu)視為平等現(xiàn)在對試圖使用計算機形式化證明的數(shù)學家們造成了“真正的麻煩”，包括幾十年前的基礎(chǔ)概念。

Buzzard告訴Wilkins：“目前存在的任何[計算機]系統(tǒng)都無法捕捉像Grothendieck這樣的數(shù)學家使用等號的方式，”他指的是20世紀依靠集合論描述平等的領(lǐng)先數(shù)學家Alexander Grothendieck。

一些數(shù)學家認為他們應(yīng)該重新定義數(shù)學概念，以正式將規(guī)范同構(gòu)等同于平等。

Buzzard不相同意。他認為數(shù)學家與機器之間的不一致應(yīng)該促使數(shù)學家重新思考他們對像平等這樣基礎(chǔ)的數(shù)學概念的確切定義，以便計算機能夠理解它們。

Buzzard寫道：“當一個人被迫寫下自己的真實意思，不能躲在那些定義不清的詞語背后時，有時會發(fā)現(xiàn)自己需要做更多的工作，甚至重新思考某些想法應(yīng)該怎么樣呈現(xiàn)。”

本文譯自 ScienceAlert，由 BALI 編輯發(fā)布。

內(nèi)容來自：愛掏網(wǎng)