1+1=2の証明

「1+1=2を証明するにはどうするか」が気になってメモ

普通の証明はペアノの公理を使うらしい

普通の説明だと多分よくわからなさそうなのでLeanで証明されているものを見てみる

Leanの場合の1+1=2の証明

mathlib ver3の場合の定義。関係しそうなところだけ抽出。

code:src/algebra/ring/defs.lean

34 variables {α : Type u} {β : Type v} {γ : Type w} {R : Type x}

110 section has_one_has_add

111

113

114 lemma one_add_one_eq_two : 1 + 1 = (2 : α) := rfl

115

116 end has_one_has_add

mathlib4の場合の定義

code:Mathlib/Data/Nat/Cast/Defs.lean

theorem one_add_one_eq_two AddMonoidWithOne R : 1 + 1 = (2 : R) := by

apply congrArg

decide

AddMonoidWithOneがなんなのとか色々わからないことはある。なのでMathlib4のドキュメントを見る。

AddMonoidWithOneの定義: Mathlib.Data.Nat.Cast.Defs

one_add_one_eq_twoの定義: Mathlib.Data.Nat.Cast.Defs

モノイド(半群)は結合律、単位律を満たす構造

code:memo

theorem cast_one AddMonoidWithOne R : ((1 : ℕ) : R) = 1 := by

-- ↑1 = 1

theorem cast_add AddMonoidWithOne R (m n : ℕ) : ((m + n : ℕ) : R) = m + n := by

induction n with

| zero => simp

-- ↑(m + n) = ↑m + ↑n