數學中的「相等」能在數理邏輯中嚴格定義嗎？

12-31

前幾天被同學問到這個問題，原問題是這樣的：在範疇論中，怎樣判斷範疇中的兩個對象是否相等？注意是相等不是同構；而且注意是在範疇論的框架中不是集合論的框架中。舉個具體的例子：範疇C以所有範疇作為對象，範疇之間的函子作為態；怎麼判斷兩個函子是相等的？表面上看，兩個函子相等，只要定義域相等，值域相等，對應關係相同就ok了；但問題來了，定義域是兩個範疇，也就是C中的對象，C中的兩個對象相等是什麼意思？問題又繞回來了。。
當然我知道直觀上這樣的問題似乎不是問題，當我想知道邏輯上怎樣用嚴格的形式語言定義相等；或者specific一些，像上述問題中，如果涉及的範疇不是小範疇的話，怎麼定義範疇中的對象是相等的？
最後扯個無關的話題：我們知道除了n=4的情況，R^n都只允許一種微分結構；但是這個「一種微分結構」是在微分同胚意義下成立的；也就是說我們寫出一個函數，它時而是可微的，時而是不可微的，但是我們並沒有改變R^n的微分結構；這種微分結構相同的定義真的是我們能接受的么？

我覺得這裡牽扯到的問題做一個博士論文應該是沒問題的。所以我就隨便扯扯。

從一階邏輯模型論的角度上來說，等於關係嚴格來說並不是一個對象或者符號上的關係，而是一個指稱上的關係。這是什麼意思？

首先我們有一套邏輯符號，然後我們有一套非邏輯符號，邏輯符號的解釋是固定的，但是非邏輯符號的解釋是不固定的，給一個模型的時候我們需要解釋這些非邏輯符號，這裡我們著重考察的是個體常元符號。

在解釋個體常元符號的時候，首先我們要確定一個論域，然後將個體常元符號解釋為論域中的對象。這類似於日常生活中見真人的過程：

——大家好，我是羅心澄。
——你他媽就是羅心澄啊，艹你大爺的。

大概這種感覺。為什麼這個見真人的過程如此重要？這實際上是在實踐上重要。歷史人物從某種意義上來說是不可靠的（當然從相同的意義上來說現實人物也是不可靠的），因為很有可能我們將不同的事件歸於同一個主體名下。但是這種面對面見人的過程，在一般情況下，是比較可靠的。除非我有一個和我衣著打扮完全一樣的雙胞胎，總是趁著你目光飄在別的地方就和我換一個位置。（當然日常生活中並沒有那麼嚴格的跨時間同一性，這導致除非我現在坐在你面前，否則你不能保證某個事件能不能歸在我名下 —— 如果我現在坐在你面前，那麼你至少可以保證此時此刻我沒有在做某些事情，但是有可能是通過時移錯覺故意製造不在場證明呢？Anscombe：你投毒的時候受害者沒死，受害者死的時候你沒在投毒，然而這說明不了任何問題。）

一階邏輯裡面為了處理量化的問題，還需要針對變數作出這樣那樣的限制和解釋，但是由於這個問題其實和變數的關係不大，因此我就略過變數了。當然，為了不減弱表達力，或者把問題說清楚，我們最好給 domain 裡面所有東西都各自配給一個對象語言中的名字。在不配的情況下，我們有兩套層次不同的符號，一套是對象語言中的符號，另一套是我們解釋對象語言符號中使用到的數學語言或者自然語言中的符號。但是為了要讓後者可在對象語言中也被完整地談論，我們最好將對象語言中的常元集合擴充到和我們要討論的數學結構的論域大小一樣大，這樣我們就得到了一套所有 domain 中的元素的名字。而另一套是某些我們需要特彆強調的常元的名字。

問題在於，對於前者，我們已經默認了對象的等於和不等是清楚的。如果我們給所有 domain 中的元素都對應上一個名字的話，我們相當於在說，對於 domain 中的任意 x， $d_x$ 是一個我們新引入的常元符號，這個常元符號的指稱是 D 中的 x。

而在談論後者的時候，比如說根據習慣，我們在談論自然數的時候一般將常元 $c_0$ 解釋成 0，即 $I(c_0):=0$ 或者 $overline{c_0}=0$ ，這意味著什麼？這意味著模型論的層面上我們建立了一個指稱關係， I 或者 overline 構成了一個解釋函數。而當我們將模型層面上的東西全部都拉到了對象語言的層面上之後，我們可以說 $c_0=d_0$ （左右的 0 的含義是不同的！比如說在別的某些模型中我可以有 $c_1 = d_{frac{37}{4}}$ 之類的東西），注意，這個地方「 $c_0$ 」沒有被一個解釋函數包裹著，看上去我們繞開了指稱問題，但是回到 Frege 的刁難上去：當我們在我們的對象語言中說這個表達式的時候，我們在表達什麼？顯然我們不是說這兩個符號相同，也不是在說這兩個符號的含義相同。我們是在說這兩個符號的指稱相同。指稱問題依舊繞不過去。

這裡的問題是，整個一階邏輯模型論在談論這種問題的時候，已經默認了模型中的對象清清楚楚地擺在那裡，我們不會弄錯，指稱關係說能建立就能建立，有必要的話指過去就行了。

問題是我們可以弄錯，最經典的例子是代數中的 i：

當我在說 i 的時候，你怎麼知道我說的不是 -i？

這個例子完美地展現出了 Max Black 的那個著名結論：萊布尼茲同一律的半邊，「性質相同保證同一性」，是錯的。

Black 的論證很狡詐：我們可以設想一個宇宙，這個宇宙中只有兩個完全一樣的球（或許在當代物理學的意義上沒有辦法完全一樣，那就想像這個宇宙服從的物理規律比較簡單，更像純粹的歐式幾何吧）：這兩個球是完全相同的，完全光滑的，什麼都是一樣的。當然，如果你跑進這個宇宙裡面，有了你作為參照系，你可以說左邊那個或者上面那個或者前面那個，或者離你更近的那個——但是這個宇宙中沒有你，所以你只能站在外面想這兩個球。於是你試圖建立一個座標系來說明問題。為了方便起見考慮平面的情況：你隨便建立一個座標系好了，你怎麼知道你建立的是這個座標系，而不是在和這兩個球的中點中心對稱的位置上的那個座標系呢？如果這兩個球是不可分辨的，那麼這兩個座標系也是不可分辨的，你試圖引入座標系來解決問題，但是這個解決方案僅僅是一個虛假的方案。同理，給球命名也是虛假的方案。最後你說，那我能不能說這裡沒有兩個球，只有一個球？答案是不行。我們無法區分 i 和 -i 不意味著我們要說 i = -i。

i 和 -i 的代數性質上是相同的，我們永遠都不知道自己在談論 i 還是 -i（別跟我說 i &> 0 而 -i &< 0，也別說座標平面的上下，這些都不 make sense），我們只知道 i 和 -i 是兩個不同的對象，但是如果真的有這兩個對象的話，我們永遠都不知道自己實際上是在指哪一個。它們處在柏拉圖的理念空間中，我們沒有辦法將自身摻合進去作為坐標。

既然在談論某個想像的宇宙的時候這種指稱關係是可疑的，那麼我們用一階邏輯描繪稍微複雜一點的數學系統的時候，這個指稱關係是同樣可疑的。當然這種可疑性並沒有使得我們在理論內部要將 i 和 -i 等同在一起，這種可疑性不過意味著這樣簡單的事實：對於兩個同構的系統，我們的邏輯語言沒有分辨力。 $mathbb{R}[i]cong mathbb{R}[-i]$ ，對於前者成立的結論，對於後者也同樣成立。

換一個角度來看，= 的推理規則中，引入規則只有一條，就是 x=x，其它的規則都是依賴於現有的等於關係去推新的等於關係。問題在於，如果我們僅僅按照 x=x 去進行推理，不加入任何額外的項之間的等於關係的假設，那麼我們就得到了一個 free term algebra，其它額外的公理都相當於是在這個 free object 上面做 quotient。問題在於，本質上來說這個 free term algebra 的結構本身並不在於具體的函數名和個體常元名，而僅僅關係到有多少個常元，多少個一元函數，多少個二元函數，這就和線性空間一樣，只要 base 的大小確定了，具體誰做 base 怎麼做都是無所謂的。所以你非要說你這個 free term algebra 裡面的那些對象就是這些 term，好，OK，但是它和其它無窮多個都是同構的，那你怎麼辦？

所以說談論等同關係，到了某個層面上之後，是沒有意義的。絕大多數情況下兩個系統談論同構就足夠了。畢竟我們真正想要談論的，並不是符號本身，而是某種代數結構。

考慮了很久都沒有得到一個讓自己滿意的解釋，並且現在看來這個問題如果想不涉及任何技術細節的討論基本是不可能了，所以這個答案只是隨便寫寫。

如果你的範疇論是在某種集合論（比如ZFC）中建立的話，那麼這個範疇中的對象a,b之間的相等就是a,b作為集合的相等，這種集合的相等關係是在這套集合論里先天保證的。對於所有小範疇的範疇Cat來說，其中對象之間的相等就是小範疇們作為集合的相等，因為你的範疇論是在集合論里建立的，一個（小）範疇不過是一個五元組（O，A，domain，codomain，·）而已，O和A是兩個集合，domain和codomain是A到O的兩個一元函數，·是A上的一個部分二元函數，並且滿足相應的範疇公理，兩個小範疇的相等就是它們作為一個上述的五元組（一個集合）的相等。當然這種相等是不自然的，比如對於所有群的範疇，這種相等要求兩個群論域相同，並且群運算也完全相同，事實上，這個時候你都不需要關心這兩個對象是不是群了，你只要它們作為兩個二元組（G，·）相等。所以當我們在談論這種相等的時候根本沒有把它們當成群看，而是看成集合了。

一般認為，範疇中自然的相等是對象之間的同構。雖然我們可以不談論對象（0-cell）的相等而只談論它們的同構，但是對於兩個態射（1-cell）又要不可避免的談論他們的相等。一個例子就是問題里提到的在Cat裡面談論兩個函子的相等，這時談論兩個函子的相等又是不自然的。所以對於1-cell我們也應該談論它們的同構，而1-cell的同構是由2-cell來定義的。這個問題可以不斷的問下去，對於任意的n-範疇，我們總可以問它的n-cell之間的相等是什麼意思？最終都要提及那個不自然的集合相等。要避免提及這個相等我們必須直接定義∞-範疇，因為對於n-cell的同構都需要n+1-cell來定義。而一個n-範疇就是一個∞-範疇並且它的所有大於n的cell只有恆同，這時我們可以把n-cell的相等看成恆同n+1-cell。在這種觀點下，對於n-範疇來說，它的n-cell之間的同構與相等是一回事，因為它的n+1-cell 只有恆同。

對於n-範疇來說，直接談論n-cell之間的相等似乎也沒有那麼不自然。回到上面提到的例子，群範疇是一個1-範疇，它任意兩個對象之間的態射構成一個集合，這時談論兩個群之間的群同態的相等就不像談論兩個群相等那麼難受了。而Cat是一個2-範疇，兩個範疇之間的函子構成一個1-範疇，這時你不能直接談論函子之間的相等，而兩個函子之間的所有自然變換構成一個集合，所以可以談論函子之間的自然變換的相等。

這是cat裡面的evil問題，見http://ncatlab.org/nlab/show/principle+of+equivalence，所以直接要求對象的相等會不太自然，有趣的是數學物理裡面用到的dagger cat中為了定義unitarity恰需要對象相等這樣的條件

物理中類似的是規範性、GR中的協變性，在GR早期曾引起討論，比如Einstein的hole論證http://en.wikipedia.org/wiki/Hole_argument

可以啊。

first-order logic with equality不就是干這事的？First-order logic

這是真對象的相等，不是什麼公理下的相等，更不是什麼同構下的相等。你把函子相等看做定義域、值域、對應法則一樣就已經被洗腦了。範疇論或者用別的語言完全可以硬是把兩個定義域、值域、對應法則都一樣的函數看做兩個不同對象，只是這在大部分情況下既沒有必要又不符合直覺。這是集合論洗的腦，要治。

不能，在範疇論里沒有相等，只有同構。在範疇論里想等沒有意義。

我來寫一個，用Ext定義。

我們這樣定義相等:

①任意X任意Y任意u(u∈X←→u∈Y)→X=Y。

②別無其他。

這個定義基於″一切數學問題都是集合論的問題"的思想，一切謂詞都可表示為集合的關係，不知道行不行。

僅當拋磚引玉，歡迎大神批判。

相等，本身即為一種映射