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) と書き、モノイド(<math>\mathbb{R}</math>,+,0) と書く。

===群===

3.（逆元）

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


この命題とモノイド(a2,f1,a1) の論理積を群(a2,f1,a1) と書き、群(<math>\mathbb{R}</math>,+,0) と書く。

===アーベル群===

4.（可換律）

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


この命題と群(a2,f1,a1) の論理積をアーベル群(a2,f1,a1) と書き、アーベル群(<math>\mathbb{R}</math>,+,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) と書き、モノイド(<math>\mathbb{R}</math>,+,0) と書いて良い。

====群====

B3.（逆元）

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


この命題とモノイド(a2,a3,a1) の論理積を群(a2,a3,a1) と書き、群(<math>\mathbb{R}</math>,+,0) と書いて良い。

====アーベル群====

B4.（可換律）

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


この命題と群(a2,a3,a1) の論理積をアーベル群(a2,a3,a1) と書き、アーベル群(<math>\mathbb{R}</math>,+,0) と書いて良い。

===定義の全体クラス===
モノイド(a2,f1,a1),群(a2,f1,a1),アーベル群(a2,f1,a1)

S_1(a2)∨a2∈<math>\mathbb{S_0}</math>
∧
∀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∈<math>\mathbb{S_0}</math>
∧
∀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) と書き、環(<math>\mathbb{R}</math>,+,*,0,1) と書く。 

===可換環===

4.（可換律）

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


この命題と環(a3,f1,f2,a1,a2) の論理積を可換環(a3,f1,f2,a1,a2) と書き、可換環(<math>\mathbb{R}</math>,+,*,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) と書き、環(<math>\mathbb{R}</math>,+,*,0,1) と書いて良い。

====可換環====

B4.（可換律）

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


この命題と環(a3,a4,a5,a1,a2) の論理積を可換環(a3,a4,a5,a1,a2) と書き、可換環(<math>\mathbb{R}</math>,+,*,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) と書き、体(<math>\mathbb{R}</math>,+,*,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) と書き、体(<math>\mathbb{R}</math>,+,*,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)<!-- o -->

∀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))))
<!--
a1⊂a2iff∀x1(x1∈a1⇒x1∈a2)
a1={}⇔∀x1￢x1∈a1
-->


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

===述語と関数を対象化した論理記述===
「I」

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

「II」

(a)（完全性を満たす二項関係）
<!--
∀x1∀x2(x1∈a3∧x2∈a3holds(P1(x1,x2)∨P1(x2,x1))∧(P1(x1,x2)∨￢P1(x1,x2)holds(x1∈a3x2∈a3)))
-->

∀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(P1(x1,x2)∧P1(x2,x3)⇒P1(x1,x3))
-->

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

(c)（無差別関係）
<!--
∀x1∀x2(P1(x1,x2)∧P1(x2,x1)⇔x1=x2) しかし実際は，逆の⇒は不要だよね。
-->

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

(d)<!-- ∀x1∀x2∀x3(P1(x1,x2)⇒P1(f1(x1,x3),f1(x2,x3))) -->

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

(e)
<!--
∀x1∀x2(P1(a1,x1)∧P1(a1,x2)⇒P1(a1,f2(x1,x2))
-->

∀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)))
)

<!--
∀x1(∀x2(x2∈x1⇒x2∈a3)∧￢∀x2￢x2∈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)∧￢∀x2￢x2∈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)))
)

a1⊂a2iff∀x1(x1∈a1⇒x1∈a2)
a1={}⇔∀x1￢x1∈a1
-->

以上 7つの命題の論理積を 実数(a3,a4,a5,a1,a2,a6)と書き、実数(<math>\mathbb{R}</math>,+,*,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つの、公理の全体クラスを示す述語命題は同値である。

[[カテゴリ:実数]]