"1 + 1 = 2" 是定義, 還是定理?

01-02

如果是定理, 怎麼證明?

首先科普一些常識，像是1+1=2這樣的東西，從現實中抽象出來，是最基礎的，可能也是最早的結論，大部分數學分支的起源也都是從現實中抽象出來的。

但是實際上公理並不是先抽象出來的就是公理，也不是簡單的就是公理，而是用最少的假設推導出其它結論，所需要的那些假設。

在現代數學裡面，存在不同的公理體系，從每一個完整的公理體系出發，理論上都能推導出整個數學。

比方說A B C D E五個結論，可能A B C作為公理能推導出D E，A B E也能推導出C D。

公理體系最開始一般都建立在一些數學的分支上，早年的公理後來都逐漸被發現一些問題逐漸完善，像是歐幾里得最開始搞的五公設，後來到希爾伯特填坑出來21公理體系。

後來還產生了研究不同公理體系之間映射關係的數學分支範疇論，反正我這智商是搞不太懂，就不誤導大家了。

說了這麼多，相信大家一定都理解了，對於 1+1=2這樣顯而易見的問題，一切不選定公理體系的證明都是耍流氓。

所以在證明1+1=2之前，要做四件事：

（1）選擇一個公理體系

（2）定義1

（3）定義2

（4）定義加法

下面我給出兩個公理體系下的定義和證明：

皮亞諾公理下證明

1和2都是自然數，自然數的定義，最有名的就是皮亞諾公理，從皮亞諾公理可以定義一階算術系統。但是實際上後來被人發現範疇性出了問題，又打了補丁。這個皮亞諾公理形式化定義估計也沒人願意看，我就通俗解釋一下：

一、定義0是自然數（其實有不同版本，比如從1開始，反正無所謂啦）

二、定義after概念，任何自然數的after也是自然數

三、兩個數a和b相等，完全等價於after(a)和after(b)相等

四、任何自然數的after都不是0

五、任何命題，滿足以下條件

（1）針對0為真

（2）從針對n為真能推導出針對after(n)為真

則它對所有自然數為真。

有了這五條定義，我們就能定義出整個自然數，它們是

0, after(0), after(after(0), ……

卧槽這好像哪裡不對，實際上我們可以把after(0)簡寫為1，把after(after(0))簡寫為2，這樣，1和2的定義都有了。

再接下來，定義加法，皮亞諾公理是這樣的：

加法是滿足以下兩個條件的運算：

（1）0 + m =m

（2）after(n) +m = after(n +m)

好吧，1+1意思是

after(0) + after(0)

根據加法定義2，它等於

after(0 + after(0))

再根據加法定義1，它又等於

after(after(0))

這就是2。

λ公理體系下的證明

lambda公理體系下，自然數的定義被稱作邱奇數，它的定義是

0 ：

λf.(λx.x)

λf.λx.f x

λf.λx.f (f x)

加法：

λ m. λ n. λ f. λ x. m f (n f x)

看著很複雜，其實用白話說就是，lambda就是替換，自然數的定義就是替換幾遍，0就是不替換，x還是原來的x，而加法就是兩個函數先後替換。

我們把 1 + 1代入試試看：

1 + 1

= (λ m. λ n. λ f. λ x. m f (n f x)) 1 1

= λ f. λ x. 1 f (1 f x)

= λ f. λ x. (λ f. λ x. f x) f ((λ f. λ x. f x) f x)

= λ f. λ x. f (f x)

= 2

彩蛋，用JS代碼驗證邱奇數加法，把f和x換成任何函數和值，最後都會輸出true

var f = x =&> x * 2; var x = 5;


var ONE = f =&> (x =&> f(x));

var TWO = f =&> (x =&> f(f(x)));

var PLUS = (m, n) =&> (f =&> (x =&> m(f)(n(f)(x))));

console.log(PLUS(ONE, ONE)(f)(x) == TWO(f)(x))

總之呢，其實吧，雖然證明上是公理推導出定理，但是認知上很多時候是從定理設計公理，不要認為公理一定比定理更簡單。

此外，本人非專業人士，為防止誤導群眾，不喜請噴不要客氣。

@Belleve 提到的在 CoC 里用 lambda encoding 來表示 inductive definition 的 paper：

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/efficiency-of-lambdaencodings-in-total-type-theory/61BB015E068EAC16C6C31D5F7654F3AD

https://tfp2016.org/papers/TFP_2016_paper_10.pdf

我也來湊個熱鬧好了，用 GHC 的類型系統來「證明」 1 + 1 = 2：

{-# OPTIONS_GHC -Wall #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}


import Data.Type.Equality
data Nat

    = Zero

    | Succ Nat
type family Add x y where

    Add "Zero n = n

    Add ("Succ m) n = "Succ (Add m n)
type One = "Succ "Zero

type Two = "Succ One

onePlusOneEqualsTwo :: Add One One :~: Two onePlusOneEqualsTwo = Refl

用 Idris 或者 Agda 之類的其他 dependently-typed language 寫會好看很多，不過中心思想都一樣——規定好什麼是自然數（Peano numbers）、什麼是 1 和 2 （1 是 0 的後繼，2 是 1 的後繼）、什麼是自然數的加法、什麼是等於（propositional equality），然後 type checker 計算 normal form 並進行匹配。

以上這個例子太 trivial 了，來證個加法的結合律和交換律看看：

data SingNat :: Nat -&> * where SZero :: SingNat "Zero SSucc :: SingNat n -&> SingNat ("Succ n)


assoc :: SingNat x

      -&> SingNat y

      -&> SingNat z

      -&> Add x (Add y z) :~: Add (Add x y) z

assoc SZero _ _ = Refl

assoc (SSucc x") y z =

    case assoc x" y z of

        Refl -&> Refl

commune :: SingNat x -&> SingNat y -&> Add x y :~: Add y x commune m n = case (lemma0 m, lemma0 n) of (Refl, Refl) -&> case m of SZero -&> Refl SSucc m" -&> case n of SZero -&> Refl SSucc n" -&> case (commune m" n", commune m" n, commune m n") of (Refl, Refl, Refl) -&> Refl where lemma0 :: SingNat n -&> Add n "Zero :~: n lemma0 SZero = Refl lemma0 (SSucc n") = case lemma0 n" of Refl -&> Refl

陳宇的基本對了。。。

作為一個小學生居然不覺得這個是定義我真是嚇哭了。。。

自然數是根據 peano axiom 定義的數系，這個公理再證明中基本不需要的部分，我就掠過了。

公理：存在元素 0 ，屬於自然數。

公理：任意自然數的後繼數為自然數

（以上為 peano 公理的部分）

定義：自然數n的後繼數記作 n++

定義：0++=1，1++=2

好了，我們接著來定義自然數加法

對於任意自然數n，n+0=n，對於自然數m，n+(m++)=(n+m)++。

然後證明1+1=2

1+1 = 1+(0++) = (1+0)++ = 1++ = 2

證畢

CIC：Refl {a=Nat} {x=(S (S O))}

CoC：呃我記得 @Canto Ostinato 說過一個把 CIC 編碼到 CoC 的論文，忘記在哪了……

HoTT/Cubical：不熟，我只知道在 HoTT/Cubical 裡面對等號的處理十分有意思……召喚 @Minghao Liu @amalgamation

這是2的定義，不用證明也不能證明。

2的定義就是1的後繼數(後繼數可以理解為某個數+1), 即2 = 1 + 1, 這是定義.

3定義為2的後繼數, 3 = 2 + 1

4定義為3的後繼數, 4 = 3 + 1

以此類推

4 = 3 + 1是定義, 不需要證明, 4 = 2 + 2有點證明價值.

證明過程:

4 = 3 + 1 = (2 + 1) + 1 = 2 + (1 + 1) = 2 + 2

解釋一下:

4 = 3 + 1 ,這是根據4的定義

3 + 1 = (2 + 1) + 1 , 這是根據3的定義

(2 + 1) + 1 = 2 + (1 + 1) , 這是根據加法的結合律

2 + (1 + 1) = 2 + 2, 這是根據2的定義

定義是不需要也不能證明的。我定義1加上1的和是一個數，這個數叫2。

你需要學數學分析。

把一往後再數一個數，這個數叫二。如果改叫三也行，不過往後的數都得重新命名；如果改叫題主也無妨，不過得重新定義題主等於二。

我不怎麼懂數學，你就暫且看看罷了。

定義自然數：

0 是自然數
對於任何一個自然數 N，都有一個 S(N) 得出 N 的後繼數，且 S(N) 也是自然數

同時：S(N) = N + 1

證明：

因為 1 = S(0)
所以 1 是自然數，並且有後繼數 S(1)
又因為 1 + 1 = S(1) = 2
所以 1 + 1 ＝ 2.

1是最小的，比1大的裡面最小的那個我們叫他做2。那麼2隻能由1再加上1獲得。1+1=2是2的定義

標題被改了··

原標題

羅西法添加了問題

怎麼證明一加一等於二?

#96270596 ?2015-02-27 00:14:42

分割線————————————————————————————————————

哈這個問題挺有意思的，

我記得我小時候也有這樣的疑惑，進入這樣的誤區

我猜題主問的應該不是哥德巴赫猜想，很有可能是看到或聽到陳景潤證明1+2命題的相關報道文章，又查了下1+1沒有人證明出來，然後沒弄清概念就到這裡提問，1+1命題和1+1=2有著本質性的區別，以下我個人理解

哥德巴赫猜想：任一大於2的偶數都可寫成兩個質數之和，例如2+2=4，3+5=8，3+3=6，5+7=12。

質數：又叫素數，有無限個。質數定義為在大於1的自然數中，除了1和它本身以外不再有其他因數的數稱為質數。例如2，3，5，7，11

哥德巴赫猜想簡寫為1+1的命題

我的理解設一個質數為a,另一個為b,所以式子為1*a+1*b，簡化就是a+b，當未知量a,b為同一質數a=b時，式子可變形為a(1+1)，最終形態就是1+1。

陳景潤證明出來的是被簡寫為1+2的命題，即一個足夠大的偶數,都能分成1個質數+2和質數的積的形式,所以被簡寫為1+2。

為了好理解這句話還是列式，1*a+2*b，當a=b可簡化為a(1+2)，最終形態1+2

目前1+1還沒有被證明出來，陳景潤證明1+2的時候發表了詳細的證明過程，估計極其繁瑣複雜，全世界看得懂的人也寥寥無幾（包括耍壁虎的我和各位），所以我不認為知乎會有數學家會閑的蛋疼回答你這個問題。

而普通意義上的1+1=2或者1+2=3，是準則，是不需要也不用證明。

非要證明的話可引用皮亞諾公理

公理：大家一致認為的，有一些證明不出來。

定理：滿足一定條件，可以推導證明的。

Ⅰ 0是自然數；
Ⅱ 每一個確定的自然數a，都具有確定的後繼數a" ，a"也是自然數（數a的後繼數a"就是緊接在這個數後面的整數（a+1）。例如，1"=2，2"=3等等。）

那麼1=0"，2=1"=1+1=0"+0"=1+0"，可以通過0推導證明的叫做定理，所以1+1=2按著皮亞諾的說法是定理

這裡在轉載一篇科普貼

你不知道的事：阿拉伯數字由哪個國家的人發明？ - 印度 - IT之家

大概就是說數字是誰發明的，計數的數目發展過程

而我的理解更傾向於更古老的時代，比如石器時代等，古人類可能在摳腳的過程，打獵的過程中，生活中領悟到其中的奧義。

演化了某種計數方式，可能是類似圓圈，點，橫，豎，手勢，甚至簡畫（類似楔形文字和象形文字）來表達，比如1根手指計數就用一豎，以此類推

剛開始數少還方便，還可以用類似羅馬數字前三位那樣表達，但是隨著數的增加發現存在的問題，總不能類似這樣表達7=I I I I I I I

甚至畫出7個小矮人吧？然後研究了好多年，才找到解決方案，最後有人總結出了0~9。

先有1後有天，不認為遠古人能理解0的含義，沒有就不用畫唄。

估計動物潛意識中也會有這樣的數學基本認知吧加減法它們也會。

例1：非洲野牛在爭奪交配權，2-1=1，累死的牛沒資格耕肥沃的地

例2：在爭奪食物，2隻流浪鬣狗調戲單親媽媽非洲豹，最終女子寡不敵眾落荒而逃。流氓不可怕就怕流氓有文化，知道1+1=2並且&>1

假如會多國語言，也可以去動物世界採訪採訪問問他們如何證明的。

以上僅代表個人觀點，不嚴謹或錯誤請多包涵

分割線----------------------------------------------------------------------------------------------

「a + b」問題的推進

1920年，挪威的布朗證明了「9 + 9」。

1924年，德國的拉特馬赫證明了「7 + 7」。

1932年，英國的埃斯特曼證明了「6 + 6」。

1937年，義大利的蕾西先後證明了「5 + 7」, 「4 + 9」, 「3 + 15」和「2 + 366」。

1938年，蘇聯的布赫夕太勃證明了「5 + 5」。

1940年，蘇聯的布赫夕太勃證明了「4 + 4」。

1956年，中國的王元證明了「3 + 4」。稍後證明了「3 + 3」和「2 + 3」。

1948年，匈牙利的瑞尼證明了「1+ c」，其中c是一很大的自然數。

1962年，中國的潘承洞和蘇聯的巴爾巴恩證明了「1 + 5」，中國的王元證明了「1 + 4」。

1965年，蘇聯的布赫夕太勃和小維諾格拉多夫，及義大利的朋比利證明了「1 + 3 」。

1966年，中國的陳景潤證明了「1 + 2 」。

本來想說，是公理，沒法證明。

憋回去了，囧，漲姿勢了。

定義.....

自然數公理化定義.....

少年抄本陳天權看完第一章就懂了（只看第一章，別看太多，壞心情）

後繼映射之類的東西，看完就懂了超好理解，看完馬上對自然數是什麼東西有一個清醒的認識（未必，這句是廣告）

不請自來。

上面這麼多大神從各種角度各種分析，各種理論各種交代。我覺得很無聊啊。

在還沒有這些理論的時候就有壹加壹等於貳了，因為中國人發明這個比他們祖宗還早。

那麼回到正題。是定義還是定理。換個解釋就是1+1=2是因還是果。

那麼首先從源頭分析，自然數肯定是定義了，原始人類發明了也就是定義了0~9這十個數字。

然後是加法與等於，顯然也是定義了，原始人類將兩堆東西放在一起稱之為相加嘛，加完就是等於嘛

重點來了，那麼1+1=2是定義還是定理？

我的觀點是：定義。為什麼，因為沒有1+1就沒有數學，沒有減乘除，就更沒有以後。

這是基礎，是必須條件，所以，這是定義。而且，這應該是出現在2出現之前的定義，而不是自然數之後的定義，為什麼有2？因為有1，當兩個1放在一起時該怎麼記？於是出現了加法等於和1+1=2，然後才出現了3456……

所以發明的順序應該是：1、+、1+1、=、1+1=2、3、4、5……再之後是先有了減還是先有了進位那就說不清了，這也不是研究能研究出來的，都有可能。

難道2的定義不就是1加1嗎？

我數學不好……

我的想法就是，2的定義就是1+1，所以這個不用證明。

如果不是的話，那我問你，你怎麼定義2？

2總得有個定義吧。

嗯……一根手指加一根手指是兩根……

二的定義就是比一大一，也就是一加一。定義不需要證明。

"可證"的一定是"真的","真的"不一定是"可證"--哥德爾不完全性定理。

我不知道這個答案回答正確不正確，權當拋磚引玉。

1+1=2是公理還是定理？ - 知乎

隨便買本數學分析吧兄弟。

我就不上鏈接了。

（這個和「推理」有啥關係）