Topic:論理と数学の基礎について/群の定義から実数の公理へ

群の定義 編集

モノイド 編集

0.(二項演算)

∀x1∀x2(x1∈a2∧x2∈a2holdsf1(x1,x2)∈a2∧(f1(x1,x2)=f1(x1,x2)holds(x1∈a2∧x2∈a2)))

1.(結合律)

∀x1∀x2∀x3f1(f1(x1,x2),x3)=f1(x1,f1(x2,x3))

2.(単位元)

∀x1(f1(a1,x1)=f1(x1,a1)∧f1(x1,a1)=x1)


以上、3つの命題を満たす関数記号 f1 と自由変数 a1,a2 をモノイド(a2,f1,a1) と書き、モノイド( ,+,0) と書く。

編集

3.(逆元)

∀x1∃x2(f1(x1,x2)=f1(x2,x1)∧f1(x2,x1)=a1)


この命題とモノイド(a2,f1,a1) の論理積を群(a2,f1,a1) と書き、群( ,+,0) と書く。

アーベル群 編集

4.(可換律)

∀x1∀x2f1(x1,x2)=f1(x2,x1)


この命題と群(a2,f1,a1) の論理積をアーベル群(a2,f1,a1) と書き、アーベル群( ,+,0) と書く。

述語と関数を対象化した論理記述 編集

モノイド 編集

B0.(二項演算)

∀x1∀x2(x1∈a2∧x2∈a2holds関(a3,(x1,x2))∈a2∧(関(a3,(x1,x2))=関(a3,(x1,x2))holds(x1∈a2∧x2∈a2)))

B1.(結合律)

∀x1∀x2∀x3関(a3,(関(a3,(x1,x2)),x3))=関(a3,(x1,関(a3,(x2,x3))))

B2.(単位元)

∀x1(関(a3,(a1,x1))=関(a3,(x1,a1))∧関(a3,(x1,a1))=x1)


この 3つの命題の論理積をモノイド(a2,a3,a1) と書き、モノイド( ,+,0) と書いて良い。

編集

B3.(逆元)

∀x1∃x2(関(a3,(x1,x2))=関(a3,(x2.x1))∧関(a3,(x2,x1))=a1)


この命題とモノイド(a2,a3,a1) の論理積を群(a2,a3,a1) と書き、群( ,+,0) と書いて良い。

アーベル群 編集

B4.(可換律)

∀x1∀x2関(a3,(x1,x2))=関(a3,(x2,x1))


この命題と群(a2,a3,a1) の論理積をアーベル群(a2,a3,a1) と書き、アーベル群( ,+,0) と書いて良い。

定義の全体クラス 編集

モノイド(a2,f1,a1),群(a2,f1,a1),アーベル群(a2,f1,a1)

S_1(a2)∨a2∈  ∧ ∀x1∀x2∀x3(f1(f1(x1,x2),x3)=f1(x1,f1(x2,x3))∨¬f1(f1(x1,x2),x3)=f1(x1,f1(x2,x3))) ∧ ∀x1(f1(a1,x1)=f1(x1,a1)∨¬f1(a1,x1)=f1(x1,a1)) ……[1]


モノイド(a2,a3,a1),群(a2,a3,a1),アーベル群(a2,a3,a1)

S_1(a2)∨a2∈  ∧ ∀x1∀x2∀x3 ( 関 ( a3, (関(a3,(x1,x2)),x3) ) = 関 ( a3, (x1,関(a3,(x2,x3))) ) ∨ ¬関 ( a3, (関(a3,(x1,x2)),x3) ) = 関 ( a3, (x1,関(a3,(x2,x3))) ) ) ∧ ∀x1 ( 関(a3,(a1,x1)) = 関(a3,(x1,a1)) ∨ ¬ 関(a3,(a1,x1)) = 関(a3,(x1,a1)) ) ……[2]


[1](a2,f1,a1) と [2](a2,a3,a1) は事実上同値である。

環の定義 編集

編集

1. アーベル群(a3,f1,a1)

2. モノイド(a3,f2,a2)

3. (分配律) ∀x1∀x2∀x3f2(x1,f1(x2,x3))=f1(f2(x1,x2),f2(x1,x3))∧f2(f1(x1,x2),x3)=f1(f2(x1,x3),f2(x2,x3))


この 3つの命題の論理積を環(a3,f1,f2,a1,a2) と書き、環( ,+,*,0,1) と書く。

可換環 編集

4.(可換律)

∀x1∀x2f2(x1,x2)=f2(x2,x1)


この命題と環(a3,f1,f2,a1,a2) の論理積を可換環(a3,f1,f2,a1,a2) と書き、可換環( ,+,*,0,1) と書く。

述語と関数を対象化した論理記述 編集

編集

B1. アーベル群(a3,a4,a1)

B2. モノイド(a3,a5,a2)

B3. (分配律)

∀x1∀x2∀x3関(a5,(x1,関(a4,(x2,x3))))=関(a4,(関(a5,(x1,x2)),関(a5,(x1,x3))))∧関(a5,(関(a4,(x1,x2)),x3))=関(a4,(関(a5,(x1,x3)),関(a5,(x1,x3))))


この 3つの命題の論理積を環(a3,a4,a5,a1,a2) と書き、環( ,+,*,0,1) と書いて良い。

可換環 編集

B4.(可換律)

∀x1∀x2 関(a5,(x1,x2))=関(a5,(x2,x1))


この命題と環(a3,a4,a5,a1,a2) の論理積を可換環(a3,a4,a5,a1,a2) と書き、可換環( ,+,*,0,1) と書いて良い。

定義の全体クラス 編集

環(a3,f1,f2,a1,a2)、可換環(a3,f1,f2,a1,a2)

[1](a3,f1,a1)∧[1](a3,f2,a2)∧∀x1∀x2∀x3(f2(x1,f1(x2,x3))=f1(f2(x1,x2),f2(x1,x3))∨¬f2(x1,f1(x2,x3))=f1(f2(x1,x2),f2(x1,x3))∨f2(f1(x1,x2),x3)=f1(f2(x1,x2),f2(x2,x3)))……[3]


環(a3,a4,a5,a1,a2) 、(a3,a4,a5,a1,a2)

[2](a3,a4,a1)∧[2](a3,a5,a2)∧∀x1∀x2∀x3関(a5,(x1,関(a4,(x2,x3))))=関(a4,(関(a5,(x1,x2)),関(a5,(x1,x3))))∨¬関(a5,(x1,関(a4,(x2,x3))))=関(a4,(関(a5,(x1,x2)),関(a5,(x1,x3))))∨関(a5,(関(a4,(x1,x2)),x3))=関(a4,(関(a5,(x1,x3)),関(a5,(x1,x3))))……[4]


[3](a3,f1,f2,a1,a2) と [4](a3,a4,a5,a1,a2) は事実上同値である。

体の定義 編集

1. 可換環(a3,f1,f2,a1,a2)

2. ( 0 以外の * の逆元)

∀x1∃x2(¬x1=a1⇒f2(x1,x2)=a2)

3. ( 0 と 1 は異なる)

¬a1=a2


この 3つの命題の論理積を体(a3,f1,f2,a1,a2) と書き、体( ,+,*,0,1) と書く。

述語と関数を対象化した論理記述 編集

B1. 可換環(a3,a4,a5,a1,a2)

B2. ( 0 以外の * の逆元)

∀x1∃x2(¬x1=a1⇒関(a5,(x1,x2))=a2)

B3. ( 0 と 1 は異なる)

¬a1=a2


この 3つの命題の論理積を体(a3,a4,a5,a1,a2) と書き、体( ,+,*,0,1) と書いて良い。

定義の全体クラス 編集

体(a3,f1,f2,a1,a2)

[3](a3,f1,f2,a1,a2)


体(a3,a4,a5,a1,a2)

[4](a3,a4,a5,a1,a2)

実数の公理 編集

「I」

体(a3,f1,f2,a1,a2)

「II」

(a)(完全性を満たす二項関係)

∀x1∀x2(x1∈a3∧x2∈a3holds(P1(x1,x2)∨P1(x2,x1))∧(P1(x1,x2)∨¬P1(x1,x2)holds(x1∈a3∧x2∈a3)))

(b) (推移性)

∀x1∀x2∀x3(P1(x1,x2)∧P1(x2,x3)⇒P1(x1,x3))

(c)(無差別関係)

∀x1∀x2(P1(x1,x2)∧P1(x2,x1)⇔x1=x2)

(d)

∀x1∀x2∀x3(P1(x1,x2)⇒P1(f1(x1,x3),f1(x2,x3)))

(e)

∀x1∀x2(P1(a1,x1)∧P1(a1,x2)⇒P1(a1,f2(x1,x2))

「III」 (上限・下限性質)

∀x1(∀x2(x2∈x1⇒x2∈a3)∧∃x2x2∈x1∧∃x2∀x3(x3∈x1⇒P1(x3,x2))⇒∃x2(∀x3(x3∈x1⇒P1(x3,x2))∧∀x3∃x4(¬P1(x2,x3)⇒(¬P1(x4,x3)∧x4∈x1))))∧∀x1(∀x2(x2∈x1⇒x2∈a3)∧∃x2x2∈x1∧∃x2∀x3(x3∈x1⇒P1(x2,x3))⇒∃x2(∀x3(x3∈x1⇒P1(x2,x3))∧∀x3∃x4(¬P1(x3,x2)⇒(¬P1(x3,x4)∧x4∈x1))))


以上 7つの命題の論理積を 実数(a3,f1,f2,a1,a2,P1)と書き、実数( ,+,*,0,1,≦)とも書き、実数の公理とする。この公理を満たす対象があるとき、自由変数 a3 を満たす集合   が実数体である。

述語と関数を対象化した論理記述 編集

「I」

体(a3,a4,a5,a1,a2)

「II」

(a)(完全性を満たす二項関係)

∀x1∀x2(x1∈a3∧x2∈a3holds(述(a6,(x1,x2))∨述(a6,(x2,x1)))∧(述(a6,(x1,x2))∨¬述(a6,(x1,x2))holds(x1∈a3∧x2∈a3)))

(b) (推移性)

∀x1∀x2∀x3(述(a6,(x1,x2))∧述(a6,(x2,x3))⇒述(a6,(x1,x3)))

(c)(無差別関係)

∀x1∀x2(述(a6,(x1,x2))∧述(a6,(x2,x1))⇔x1=x2)

(d)

∀x1∀x2∀x3(述(a6,(x1,x2))⇒述(a6,(関(a4,(x1,x3)),関(a4,(x2,x3)))))

(e)

∀x1∀x2(述(a6,(a1,x1))∧述(a6,(a1,x2))⇒述(a6,(a1,関(a5,(x1,x2)))))

「III」 (上限・下限性質)

∀x1( ∀x2(x2∈x1⇒x2∈a3)∧∃x2x2∈x1∧∃x2∀x3(x3∈x1⇒述(a6,(x3,x2))) ⇒∃x2( ∀x3(x3∈x1⇒述(a6,(x3,x2))) ∧ ∀x3∃x4(¬述(a6,(x2,x3))⇒(¬述(a6,(x4,x3))∧x4∈x1)) ) ) ∧ ∀x1( ∀x2(x2∈x1⇒x2∈a3)∧∃x2x2∈x1∧∃x2∀x3(x3∈x1⇒述(a6,(x2,x3))) ⇒ ∃x2( ∀x3(x3∈x1⇒述(a6,(x2,x3))) ∧ ∀x3∃x4(¬述(a6,(x3,x2))⇒(¬述(a6,(x3,x4))∧x4∈x1))) )


以上 7つの命題の論理積を 実数(a3,a4,a5,a1,a2,a6)と書き、実数( ,+,*,0,1,≦)とも書き、実数の公理とする。

公理の全体クラス 編集

実数(a3,f1,f2,a1,a2,P1)

[3](a3,f1,f2,a1,a2)∧∀x1∀x2(P1(x1,x2)∨¬P1(x1,x2)∨P1(x2,x1))∧∀x1∀x2∀x3(P1(x1,x2)∨¬P1(x1,x2)∨P1(x1,x3)∨P1(x2,x3))∧∀x1∀x2(P1(x1,x2)∨¬P1(x1,x2)∨P1(f1(x1,x3),f1(x2,x3)))∧∀x1∀x2(P1(a1,x1)∨¬P1(a1,x1)∨P1(a1,x2)∨P1(a1,f2(x1,x2)))

実数(a3,a4,a5,a1,a2,a6)

[4](a3,a4,a5,a1,a2)∧∀x1∀x2(述(a3,(x1,x2))∨¬述(a3,(x1,x2))∨述(a3,(x2,x1)))∧∀x1∀x2∀x3(述(a3,(x1,x2))∨¬述(a3,(x1,x2))∨述(a3,(x1,x3))∨述(a3,(x2,x3)))∧∀x1∀x2(述(a3,(x1,x2))∨¬述(a3,(x1,x2))∨述語(a3,(関(a4,(x1,x3)),関(4,(x2,x3)))))∧∀x1∀x2(述(a3,(a1,x1))∨¬述(a3,(a1,x1))∨述(a3,(a1,x2))∨述(a3,(a1,関(a5,(x1,x2)))))


上記 2つの、公理の全体クラスを示す述語命題は同値である。