一頓關于心智、機器和智能的哲學大餐！｜圖靈教育

關注風雲之聲

提升思維層次

導讀

一位試圖深入聊聊莎士比亞的女人被判定為計算機，因為“人類不會知道那麼多有關莎士比亞的事情……”

本文節選自 《量子計算公開課》第4章：“心智與機器”。為保證大家不錯過精彩内容，我們未曾删減，請大家耐心閱讀。

現在我們要開始講一些我知道你期待已久的東西：一頓關于心智、機器和智能的哲學大餐！

不過，首先讓我們讨論完可計算性。在本章中，我們将反複用到一個稱為谕示（oracle）的概念。這個概念很容易了解：假設我們擁有一個“黑箱”，或所謂“谕示”，它能夠立馬解決一些困難的計算問題，給出其結果。（當我還是大學新生時，有一次我跟導師談起了一個假想的“NP– 完全性精靈”可能帶來的後果：它将立馬告訴你，給定一個布爾表達式是不是可滿足的。導師不得不糾正我：它們 不叫“精靈”，它們叫“谕示”。這聽上去就專業多了！）

谕示似乎首先由圖靈在他 1938 年的博士論文中開始研究。顯然，任何會用一整篇論文來研究這些假想事物的人必定是位極端純粹的理論家，絕不會務實。圖靈的情況便是如此——事實上，在博士畢業後的 1939 至 1943 年，他都在研究 26個字母的某種深奧的對稱變換。

不管怎樣，如果給定問題 B 的一個谕示，問題 A 即可由一個圖靈機解決，那麼我們稱問題 A 圖靈可歸約（Turing reducible）到問題 B。換句話說，“A 不比 B 難”：如果我們有一個假想的裝置能夠解決 B，那我們也能夠解決 A。如果兩個問題互相圖靈可歸約，我們就稱兩者是圖靈等價的（Turing equivalent）。是以，比如，一個命題能否從集合論公理中得到證明的問題與停機問題就是圖靈等價的：如果你能夠解決其中一個問題，那麼你就能夠解決另一個。

現在，圖靈度（Turing degree）是指對于某個給定問題，所有與之圖靈等價的問題的集合。圖靈度有什麼例子？其實我們已經見過兩個例子了：(1) 可計算問題的集合，以及 (2) 與停機問題圖靈等價的問題的集合。說這兩者的圖靈度不相等，也就是以另一種方式說停機問題不可解。

有比這兩者更高的圖靈度嗎？換句話說，有什麼問題比停機問題更難，它即便借助停機問題的谕示也解決不了？好吧，考慮下述“超級停機問題”：給定一個擁有停機問題谕示的圖靈機，然後問它是否會停機。我們能夠證明即便擁有一般停機問題的谕示，這個超級停機問題仍然解決不了嗎？是的，我們可以！我們隻需拿出圖靈對于停機問題不可解的原始證明，然後“進行更新”，給所有機器都配上一個停機問題的谕示。證明的每一步都與原來的一模一樣，這時我們稱這個證明“相對化（relativize）了。

這裡有一個更微妙的問題：有沒有什麼問題的難度介于可計算問題和停機問題之間？這個問題最早在 1944 年由埃米爾·波斯特（Emil Post）提出，并最終在 1956 年由美國人理查德·弗裡德伯格（Richard Friedberg）和蘇聯人 A. A. 穆奇尼克（A. A. Muchnik）分别獨立解答。答案是肯定的。事實上，弗裡德伯格和穆奇尼克證明了一個更強的結論：存在兩個問題 A 和 B，給定一個停機問題的谕示，兩者均可解；但給定一個對方的谕示，兩者都不可解。這些問題可通過一個旨在消除所有可能使 A 歸約到 B，或者使 B 歸約到 A 的圖靈機的無窮過程加以構造。不幸的是，這樣得到的問題是極其不自然的；它們不像任何在實踐中可能遇到的問題。甚至直至今日，我們還沒有找到一個“自然”的、具有中間圖靈度的例子。

自從弗裡德伯格和穆奇尼克取得突破以後，有關圖靈度結構的諸多細節已被深入研究。這裡提一個最簡單的問題：如果兩個問題 A 和 B 均可歸約到停機問題，那麼是否一定存在一個可歸約到 A 和 B 的問題 C，使得任何可同時歸約到 A 和 B的問題都可歸約到 C ？想想吧！但現在是時候轉入下一個話題了……（順便一提，這個問題的答案是否定的。）

可計算性的哲學基礎是邱奇 – 圖靈論題。它得名自艾倫·圖靈及其導師阿隆佐·邱奇，盡管他們對于“自己”的這個論題持何種态度還存在争議。簡單來說，邱奇 – 圖靈論題說的是，任何“自然地被視為可計算”的函數都可被一個圖靈機計算。或者換句話說，任何關于計算的“合理的”模型都将給出與圖靈機模型相同的可計算函數的集合，或者是其真子集。

這裡存在一個顯而易見的問題：這個命題是什麼類型的？這是一個表明何種函數在實體現實中可計算的經驗命題，還是一個關于“可計算”一詞含義的定義性命題，又或是跟兩者都沾點邊？

好吧，無論答案如何，邱奇 – 圖靈論題可謂極其成功。正如你可能知道的（并且我們之後也會讨論到），量子計算嚴肅挑戰了所謂的拓展邱奇 – 圖靈論題：任何自然地被視為可有效計算的函數都可被一個圖靈機有效計算。但在我看來，到目前為止，尚沒有什麼能夠嚴肅挑戰原始的邱奇 – 圖靈論題——不論是作為一個關于實體現實的命題，還是作為一個關于“可計算”的定義。

對于邱奇 – 圖靈論題的“不打緊”的挑戰則已經有很多。事實上，一些會議和期刊便專注于這些挑戰——你可以在網上搜尋“超計算”（hypercomputation）。我讀過其中一些材料，它們大多是這個思路：假設你能夠在一秒内完成一個計算的第一步，在二分之一秒内完成下一步，在四分之一秒内完成再下一步，在八分之一秒内完成再下一步，如此等等，那麼你便會在兩秒内完成無限次的計算！好吧，這聽上去有點兒傻，也許加入一個黑洞或其他什麼東西能讓它更特别一些。對于這樣的東西，那些守舊的圖靈反對派又能作何回應呢？（這讓我想起了一個關于超級計算機的笑話：它的運作速度如此之快，以至于它能在 2.5 秒内完成一個無限循環。）

我們應該立即質疑，要是大自然真希望賦予我們如此巨大的計算能力，它也不應該以如此乏味、無趣的方式實作。其中奧秘應當毫不費力就能被我們發現。不過，要想真正看清楚為什麼超計算的思路是錯誤的，你需要用到雅各布·貝肯施泰因（Jacob Bekenstein）和拉斐爾·布索（Raphael Bousso）等人提出的熵界（entropy bound）——這是實體學家自認為的對于量子引力為數不多的了解之一， 我們之後還會提起它。是以，邱奇 – 圖靈論題（甚至是其原始的、非拓展的版本）其實與實體學中一些最深刻的問題相關聯。而在我看來，自其誕生以來的 75 年裡，無論是量子計算，還是模拟計算，又或是任何其他東西，都沒能嚴肅挑戰到邱奇 – 圖靈論題。

另一個緊密相關的對于這種基于幾何級數的計算的質疑是，我們确實在某種程度上了解為什麼這種模型不合乎實體：我們相信，當時間短到 10-43 秒（普朗克尺度）時，時間的概念本身會開始瓦解。我們不知道在那裡具體會發生什麼。但無論如何，這種情況一點兒也不像（比如）量子計算。正如我們将要看到的，在量子計算中，沒有人能對理論何處會出錯、計算機何時會停止運作有絲毫定量的概念。這使得有人不禁猜想，計算機可能永遠都不會停止運作。

一旦進入普朗克尺度，你可能會說，讨論将真的變得非常複雜。你可能還會說，在實踐中，我們總是受限于噪聲和不完美。

但問題是，為什麼我們會受到限制？為什麼不能将一個實數放在寄存器中？我認為，如果你真的試圖讓讨論變精确，你終究避免不了要談到普朗克尺度。如果我們将邱奇 – 圖靈論題闡釋為一個關于實體現實的命題，那麼它應當包含這個現實中的所有東西，包括你兩耳之間的黏糊糊的神經網絡。當然，這将我們直接引向了我向你承諾過的一個戰事激烈的智力戰場。

有個有趣的曆史事實，會思考的機器的存在可能性不是人們在使用計算機多年後才漸漸意識到的。相反，他們在開始談論計算機的那個時刻便立馬想到了這一點。諸如萊布尼茨、查爾斯·巴貝奇、愛達·洛夫萊斯、艾倫·圖靈、約翰·馮·諾伊曼（John von Neumann）等人從一開始就意識到，計算機不隻是另一種蒸汽機或烤面包機；而由于它具有通用性，是以我們很難在談論計算機時不談到我們自身。

現在，我要求你暫時時放下這本書，抽幾分鐘讀一下圖靈第二著名的論文《計算機器與智能》（“Computing Machinery and Intelligence”）。

這篇論文的核心思想是什麼？我讀後的感覺是，它呼籲反對有機沙文主義。确實，圖靈在其中提出了一些科學論證、一些數學論證，以及一些認識論論證。但在所有這些論證背後其實暗含着一個道德論證：如果一台計算機能以與人類區分不出的方式與我們互動，那麼當然，我們可以說計算機并沒有“真正”在思考，它隻是在模拟。但基于同樣的理由，我們也可以說其他人沒有真正在思考，他們隻是假裝在思考。是以，憑什麼我們在一種情況下這樣說，而在另一種情況下又那樣說？

如果你允許我對此發表評論（好像我一直做的是别的事情似的……），那麼我會說，這個道德問題，這個雙重标準問題，是約翰·塞爾、羅傑·彭羅斯等“強人工智能質疑者”無法自圓其說的。人們确實能夠給出有分量的、有說服力的論證來駁斥會思考的機器的存在可能性。但這些論證的唯一問題是，它們也同樣駁斥了會思考的大腦的存在可能性！

舉個例子：一個常見的論證是，如果一台計算機看上去像是智能的，那其實隻是設計它的人類的智能的反映。但如果人類的智能也僅是造就它的數十億年生物演化過程的反映，這個論證又該得出什麼推論呢？人工智能質疑者無法誠實地思考這個類比，每每讓我感到非常失望。其他人具有的“質性”（qualia）和“關涉性”（aboutness）被簡單視作理所當然接受了。隻有機器的質性存在質疑。

但或許人工智能質疑者可以這樣反駁：我相信其他人在思考，是因為我知道我在思考，而其他人看上去跟我很相像——他們都有十根手指、腋毛，等等。但一個機器人看上去則大為不同——它由金屬制成，有天線，用輪子在室内移動，等等。是以，即便一個機器人表現得像在思考，誰又知道實際是怎樣的呢？但如果我接受這個論證，為什麼不能進一步推論？我為什麼不能說，我承認人類會思考，但至于狗和貓，誰知道呢？它們看上去跟我太不相像了。

在我看來，我們可以将關于人工智能的所有讨論分成兩類：源自圖靈 1950 年論文的 70%，以及在那之後半個多世紀新湧現的 30%。

是以在 60 多年之後，我們敢說，确實有些事情會讓艾倫·圖靈感到出乎意料。是什麼呢？其中之一是我們所取得的進展相較于當初的預期，是多麼微乎其微！你還記不記得圖靈做過一個可證僞的預測：

我相信在約 50 年後，我們将能夠程式設計擁有約 109 存儲容量的計算機，使得它們能夠如此好地進行模拟遊戲，以至于一位普通的裁判在經過五分鐘的質詢後正确判斷出它們是否為機器的機率不超70%。

那麼事實證明他的預測怎麼樣呢？首先，我們注意到他關于計算機本身的預測相當好。圖靈預測在 50 年後（也就是到 2000 年），我們将能夠程式設計擁有達 109 （即 1G）存儲容量的計算機。

但關于計算機通過模仿遊戲的預測呢？圖靈的預測怎麼樣了？

好吧，你們當中的一些人可能聽說過一個叫作ELIZA的程式，它由約瑟夫·魏岑鮑姆在 1966 年編寫。這個程式模拟了一個心理醫生，它始終重複你所說的話，不論你說的是什麼。魏岑鮑姆發現了一件驚人的事情，很多人對這個程式敞開了心扉！甚至有時，當你告訴他們，他們之前是在與一個程式（而且還是一個極其簡單的程式）對話時，他們都不相信你。

很多年前，有人想出了一個好點子，将原始的 ELIZA 程式放進美國線上（AOL）的聊天室中，然後看會發生什麼。如果你到這個網站上去看，你會發現一些很好笑的對話（幸好是匿名的），包括試圖勾引這個程式、向它透露自己的感情，等等。下面這段對話是我的最愛，其中某男在最終對程式提出暗示之前，自稱計劃讀完文學學士學位，然後将“與星巴克展開商務合作”。

某男：我想你正在為戲弄我的感受而興奮不已。

ELIZA ：你的感受？

某男：不加入我的幻想來讓我感到沮喪。

ELIZA ：你的幻想？

某男：戀愛的幻想。

ELIZA ：這跟你讀完文學學士學位，然後将與星巴克展開商務合作有

絲毫關系嗎？

如今最先進的人機對話能力已經超過這個程度了，但也沒有超過那麼多。看上去，我們實際需要修正圖靈測試了：如果想要驗證一台計算機是否具有智能，那麼我們需要要求人類裁判具有某種最低水準的智能。

當然，這裡的一個問題在于，這些人一開始就假設自己是在與另一個人交談。而在圖靈測試中，裁判需要努力區分出人類和機器。是以，這不是真正的圖靈測試，隻是為了引人一笑罷了。不過，在過去幾十年裡，休·勒布納（Hugh Loebner）一直在做一個更接近于圖靈所設想的測試。在這裡，參與測試的人被告知他們需要努力區分出人類和計算機——但許多聊天記錄還是同樣慘不忍睹，不論是從機器智能的角度，還是人類智能的角度。（比如，一位試圖深入聊聊莎士比亞的女人被判定為計算機，因為“人類不會知道那麼多有關莎士比亞的事情……”）

你可能會好奇，如果讓計算機替代人類來質詢會怎樣？事實上，也有人這樣做了。路易斯·馮·阿恩（Luis von Ahn）獲得 2006 年麥克阿瑟獎，部分原因就是他在驗證碼（CAPTCHA）上所做的工作。驗證碼是一些網站用來區分合法使用者與垃圾郵件程式的測試。我敢說，你肯定遇到過它們——那些你需要重新輸入一遍的怪異扭曲的字母。這些測試的關鍵特性是，一台計算機應該能夠生成和評價它們，但不能夠通過它們！（很像教授為期中考試出題……）應該隻有人類能夠通過這些測試。是以簡單來說，這些測試是在利用人工智能的缺陷。（好吧，它們也是在利用單向函數求逆計算的困難性，對此我們稍後會說到。）

關于驗證碼的有趣一點是，它們引發了驗證碼程式員與人工智能程式員之間的一場軍備競賽。當我在美國加利福尼亞大學伯克利分校讀研時，我的一些研究所學生同學寫出了一個叫作 Gimpy 的程式 [1]，它能在大約 30% 的時間裡破解驗證碼。是以驗證碼不得不被加以強化，然後人工智能研究者再接再厲，想法破解……如此交替反複。誰會赢呢？

你看，當你注冊一個郵箱賬号時，你經常會直接面對一個古老的“何為人類”的謎題……

盡管人工智能在圖靈測試方面仍然任重道遠，但它們确實已經取得了一些重大進展。我們都知道卡斯帕羅夫與深藍的對戰，以及 IBM 的“沃森”在《危險邊緣》電視智力競賽中戰勝了人類冠軍肯·詹甯斯，赢得冠軍。可能不那麼衆所周知的是，1996 年，一個叫作 Otter 的程式 A 被用來解決一個困擾了數學家六十多年、連塔斯基（Alfred Tarski）及其他著名數學家都久攻不下的代數難題——羅賓斯猜想。（看起來，塔斯基幾十年來都把這個問題交給了他最得意的門生。但最終，他開始把它交給他最糟糕的弟子……）這個問題很容易陳述：給定三條公理：

● A 或 (B 或 C) = (A 或 B) 或 C，

● A 或 B = B 或 A，

● 非 ( 非 (A 或 B) 或非 (A 或非 (B)))=A，

我們能夠由此推導出非 ( 非 (A))=A 嗎？

我需要強調，這裡的證明不像阿佩爾和哈肯對于四色定理的證明那樣，計算機基本上隻是驗證數以千計的可能情況。在這裡，整個證明隻有 17 行長。一個人就能進行驗證，然後說：“對啊，我本該也能想到的。”（在原理上！）

還有什麼其他人工智能？還有一個極其複雜的人工智能系統，你們幾乎所有人都用過，并且今天說不定還會用到很多次。是什麼？對，搜尋引擎，比如谷歌。

你可能會看下這些例子——深藍、羅賓斯猜想、谷歌以及“沃森”，然後說，這些其實不是真正的人工智能。它們隻是一些利用聰明算法實作的大規模搜尋。但這樣的說法無疑會讓人工智能研究者感到惱怒。他們會說：如果你告訴 20 世紀60 年代的人們，30 年後我們将能夠戰勝國際象棋特級大師，然後問他們這算不算人工智能，他們會說，這當然算是人工智能！但當我們現在已經做到時，它卻不再是人工智能了——它僅僅是搜尋！（哲學家也有類似的抱怨：隻要哲學的某個分支得出了任何實實在在的東西，它就不再被稱為哲學！而是被稱為數學或科學。）

相較于圖靈時代的人們，我們現在還意識到了另外一件事。那就是，當我們試圖編寫程式模拟人類智能時，我們其實是在與數十億年的生物演化相較量，而這非常之艱難。由此可得到一個違反直覺的結論：讓計算機程式在國際象棋比賽中打敗卡斯帕羅夫，要比讓計算機識别不同光照條件下的人臉容易多了。常常是，對于人工智能來說最困難的任務，是那些對于五歲小孩來說不值一提的任務，因為這些功能已經通過演化融入我們的身體，我們甚至不加考慮就能做到。

在過去六十多年中，有沒有出現關于圖靈測試本身的新洞見？在我看來，沒有太多。不過從另一個角度，确實有一個著名的“未遂”洞見——塞爾的中文房間。這個論證在 1980 年左右被提出，它認為，即便一台計算機确實通過了圖靈測試，它也不會是智能的。事情是這樣的，假如你不會說中文。你坐在一個房間中，有人透過牆上的一個洞遞給你一張寫有中文問題的紙條，而你可以通過查閱一本規則手冊來回答問題（同樣也是用中文）。在這種情況下，你可能得以進行一場智能的中文對話，然而根據假設，你一句中文也不了解！是以，符号處理不意味着了解。

強人工智能支援者會如何回應呢？他可能會說，你或許不懂中文，但那本規則手冊懂中文！換句話說，了解中文是由你和規則手冊構成的系統湧現的一個特性，就像了解母語是你大腦中的神經元系統湧現的一個特性。

塞爾對此的回應是：好，那我把規則手冊背下來！這時，除了你的大腦之外沒有其他系統了，但你依舊不了解中文。對此，人工智能支援者會立刻反駁說：在這種情況下同樣存在另一個系統！假設你背下了規則手冊，我們就需要區分原始的你與新的、通過遵循所記憶的規則而生成的模拟存在——這個存在與你的唯一聯系可能是，它碰巧與你栖息于同一具軀體中。這個回應或許聽上去很瘋狂，但“瘋狂”隻是對從未接觸過計算機科學的人而言。對于一位計算機科學家來說，一個計算（比如，一個 LISP 解釋器）能夠通過嚴格執行規則生成另一個不同的、不相關的計算（比如，一個太空射擊遊戲）是完全合理的。

你看，就像我稍後會讨論的，我并不知道中文房間論證的結論是真還是假。我也不知道對于一個實體系統來說，“了解”中文需要什麼樣的必要或充分條件——我想，塞爾或其他任何人也不知道。但單單作為一個論證，中文房間的幾個方面始終困擾着我。其一是在我們應當預期直覺會非常不可靠的一類問題上， 會不自覺地訴諸直覺——“這隻是一本規則手冊！”其二是雙重标準：神經元系統可以了解中文，這一點被視為顯而易見的，而且完全不成問題，這使得人們根本不會去想為什麼規則手冊不能了解中文。其三，中文房間論證在如此大程度上建基于一個可能成問題的意象，換句話說，它試圖通過巧妙的表述避開整個計算複雜性的議題。它讓我們想象一個人迎來送往一堆紙條，卻對其内毫無了解和洞察，就像一些笨拙的新生在數學考試中寫下 (a +b)2=a2+b2 。但我們讨論的是多少張紙條？那本規則手冊到底有多大？而你需要以多快的速度查閱它，才能進行一場接近實時的智能的中文對話？如果規則手冊中的一頁對應于說中文的人的大腦中的一個神經元，那麼我們談論的這本“規則手冊”至少要有地球那麼大，可被一大群以接近光速穿行的機器人檢索查閱。當你将它表述成這樣子時，你可能就不再無法想象，由此生成的這個說中文的巨型實體可能擁有被我們稱為了解或洞察的東西。

當然，每個人在談論這些東西時，其實都在極力避免涉及意識的問題。你看，意識有着怪異的雙重性：一方面，它可以說是我們了解到的最神秘的東西；另一方面，它不僅是我們直接感覺到的東西，而且在某種意義上，它也是我們唯一直接感覺到的東西。你知道的，我思故我在，諸如此類。舉個例子，我可能錯誤地認為我的襯衫是藍色的（可能我産生了幻覺或者出于别的原因），但對于我認為它是藍色這件事情，我不會出錯。（如果我會出錯，那麼我們會得到一個無窮遞歸。）

有沒有其他東西也能帶來絕對确定的感覺？沒錯，是數學！順便一提，我認為數學與主觀經驗之間的這種相似性或許可以幫助解釋數學家的“準神秘主義”傾向。（我已經能夠聽到一些數學家倒吸了一口冷氣。真不好意思！）實體學家了解這一點很重要：當你與一位數學家交談時，你可能并不是在與一位畏懼真實世界因而退縮到自己的思想小天地的人交談，你可能是在與一位一開始就不認為真實世界有什麼“真”的人交談！

我的意思是，想一想我之前提到過的四色定理的計算機輔助證明。那個證明解決了一個有着百年曆史的未解之謎，但它的解決辦法是将問題歸約為數以千計的可能情況。為什麼有些數學家不相信這個證明，或者至少希望找到一個更好的證明？因為計算機“有可能會犯錯”嗎？好吧，這是個很弱的質疑，因為這個證明已經被多個獨立的團隊用不同的軟體和硬體反複驗證過了。再說了，人類也時常會犯錯誤！

我想，歸根結底，這裡的問題在于，存在一種觀念，在其中，四色定理已被證明；還存在另一種很多數學家所了解的證明的觀念，而這兩種觀念并不相同。

對于很多數學家來說，如果隻是一個實體過程（有可能是經典計算、量子計算、互動式協定等）運作完畢，然後就聲稱這個命題已被證明，那麼不論相信“這個實體過程是可靠的”的理由有多麼充分，一個命題都并未被證明。相反，隻有當數學家感到他們的心智可以直接感覺到其正确性時，這個命題才是被證明了的。

當然，我們很難直接讨論這些事情。但我在這裡試圖要指出的是，很多人的“仇視機器人情緒”很有可能源自以下兩個因素：

1. 一種直接的經驗确定，即認為機器人是有意識的——能夠感覺到色彩、聲音、正整數等，而不論其他人能不能；

2. 一種信念，即如果這些感覺隻是一個計算，則機器人不可能通過這種方式具有意識。

比如，我認為彭羅斯對于強人工智能的質疑就源自以上兩個因素。而他借助 哥德爾定理的論證隻是後加的裝飾。

在那些這樣想的人看來（在某些情緒下，我也屬于其中），賦予一個機器人意識等價于否認自己能夠意識到自己是有意識的。有沒有什麼體面的方法可幫助他們擺脫這個困境？也就是說，不暗含哪怕一點兒雙重标準（為我們自己和機器人制定不同規則）的方法？

我個人喜歡哲學家戴維·查默斯所提出的破解方法。簡單來說，查默斯所主張的是一種“哲學上的 NP 完全性歸約”：将一個謎歸約為另一個。他說，如果某一天，計算機在每一個可觀測的方面都能夠模拟人類，那麼我們不得不承認它們是有意識的，正如我們承認其他人是有意識的。至于它們如何才能變得有意識呢？——好吧，我們對此的了解程度就如同我們對一大群神經元如何能變得有意識的了解程度一樣，少之又少。确實，這是個謎，但這個謎看上去與另一個謎并沒有那麼不同。

思考題：

1.我們能否不失一般性地假設，一個計算機程式能夠讀取自身的源代碼？

2.要是在 19 世紀之前被稱作“水”的那個東西被事實證明是 CH4 而非 H2O，

那麼它還是水嗎？還是它會成為其他的東西？