1樓：FRANK
Theorem
plus_theorm
:forallxy
:nat,x
=y->Sx
=Sy.
Proof
.introsxy
.introsH.
rewrite
->H.
reflexivity
.Qed.
2樓：KevinYao1224
n++先返回n，再n+=1，m++同理，所以n++的值就是n，m++的值就是m，那麼因為n=m所以n++=m++。
手動狗頭
3樓：耿天宇
建議題主補充一下你這個問題裡所說的皮亞諾公立都有什麼內容。按照維基百科上給的這九條（https://
en.wikipedia.org/wiki/Peano_axioms
）公理7就就包含了你這個命題。
4樓：藥罐子千里冰封
你這個不是用皮亞諾公理證明，是要用等號的性質證明。
假設你這個等號是指兩個自然數的 canonical form 相等 (類似 MLTT 裡面的 Id)，那麼 n=m 意味著任何表示式中的 n 可以被替換為 m (Id type 的 elimination rule)，那麼我們把根據自反性成立的 n++=n++ 右邊的 n 替換為 m 即可證明結論。
5樓：MarvelousJustice
emmm 個人看書的時候把這個當做了數理邏輯裡頭相等的替換公理。
現在看到了函式回來回答一波，自然數的++運算可以看成一種函式運算，書裡嚴格證明了函式運算是滿足替換公理的。
6樓：endoresu
重新看了一下皮亞諾公理，第二條關於直接後繼的定義是明確乙個自然數只有乙個直接後繼，即可以把直接後繼運算子看成是乙個函式f，那麼f(n) = n++。函式的性質：相同的輸入有相同的結果。
如果直接把定義中乙個自然數只有乙個直接後繼改成有若干個直接後繼，就形成了類似於歐幾里得第五公設問題的情況，這個假設在皮亞諾公理的範圍內沒有矛盾。但是稍微範圍擴大一點，比如把兩個自然數可比較（要麼a ≤ b要麼a > b）的定義放在一起，會導致得出並非任意兩個自然數都可比較的結論，這種自然數就不是我們常規理解的自然數了。
以下句子是否能替代皮亞諾公理的第五條？
Chuck 我認為是等價的。但是題主所給出的 的定義太難用。我們嘗試用分層遞迴的方式來定義之。前四條公理已經告訴了我們0以及 後繼 具有了什麼性質，並且現在我們的手頭上有乙個集合N，我們來定義乙個N上的大於關係，之後再加入 題主的第五公理 N的結構就將被固定下來。記對映滿足 構造集合 並且 令二元關...
皮亞諾公理中的 0 是自然數 是在定義 0，還是在定義自然數？
反射序數 自然數這東西理論上無法定義，你只能去相信它存在。相信它存在之後，你還需要去相信它的一些性質。PA就是其性質的一部分。乙個模型由乙個集合，一些常量，一些函式，一些關係構成。在PA的模型的定義裡，首先會指出，這個模型必須有乙個特定的滿足之後某些要求的常量。至於這個常量叫什麼名字，只需根據方便來...
皮亞諾公理的第二條所說的後繼數有確切定義嗎？
為了保證推理能最大限度避開直觀干擾，幾何學中的點 線 面的名詞可以換成杯子 椅子 桌子，這些名詞本身指什麼不重要，只要符合同樣的公理，也應該得到同樣的定理。後繼當然可以解釋為 1.不過，如果你願意，也可以把負整數視為自然數，那麼後繼就成了 1.一般把自然數建立在集合論的基礎上，空集解釋為0，解釋為1...