首先科普一些常識，像是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)
1:
λf.λx.f x
2:
λ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
總之呢，其實吧，雖然證明上是公理推匯出定理，但是認知上很多時候是從定理設計公理，不要認為公理一定比定理更簡單。
此外，本人非專業人士，為防止誤導群眾，不喜請噴不要客氣。
首先科普一些常識，像是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)
1:
λf.λx.f x
2:
λ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
總之呢，其實吧，雖然證明上是公理推匯出定理，但是認知上很多時候是從定理設計公理，不要認為公理一定比定理更簡單。
此外，本人非專業人士，為防止誤導群眾，不喜請噴不要客氣。