日記2

自然演繹を積極的に用いたい．

命題 1.2.7　体は整域であること　9項

新妻弘『独習ガロア理論』近代科学社 2023

$a,b,c,...,x,y,z,......：1つの束縛変項$

$a_1,a_2,...,b_1,b_2,......：1つの自由変項$

$(R, +, \cdot)：１つの体$

とする．このとき $R$ は整域である．

(証明の方針)

　 $R$ を体である，と仮定し

①　 $∀a∀b［a∈R→［b∈R→［a≠0_R→b≠0_R］］］$

②　 $\vdash ∀a∀b［a∈R→［b∈R$

$→［a≠0_R→［b≠0_R→ab≠0_R］］］］$

をいう．

1　　　(1)　 $∀a∀b［a∈R→［b∈R→［a≠0_R→b≠0_R］］］$ 　　前提

1　　　(2)　 $∀b［a_1∈R→［b∈R→［a_1≠0_R→b≠0_R］］］$ 　　1. ∀-除去

1　　　(3)　 $a_1∈R→［b_1∈R→［a_1≠0_R→b_1≠0_R］］$ 　　2. ∀-除去

4　　　(4)　 $a_1∈R$ 　　仮定

1,4　　 (5)　 $b_1∈R→［a_1≠0_R→b_1≠0_R］$ 　　3,4. →-除去

6　　　(6)　 $b_1∈R$ 　　仮定

1,4,6　 (7)　 $a_1≠0_R→b_1≠0_R$ 　　5,6. →-除去

8　　　(8)　 $a_1≠0_R$ 　　仮定

1,4,6,8 (9)　 $b_1≠0_R$ 　　7,8. →-除去

10　　 (10)　 $a_1b_1≠0_R$ 　　仮定

1,4,6,8 (11)　 $b_1≠0_R→a_1b_1≠0_R$ 　　9-10. →-導入

1,4,6　 (12)　 $a_1≠0_R→［b_1≠0_R→a_1b_1≠0_R］$ 　　

8-11. →-導入

1,4　　 (13)　 $b_1∈R→［a_1≠0_R→［b_1≠0_R→a_1b_1≠0_R］］$ 　　

6-12. →-導入

1　　　(14)　 $a_1∈R→［b_1∈R→［a_1≠0_R$

$→［b_1≠0_R→a_1b_1≠0_R］］］$ 　　4-13. →-導入

1　　　(15)　 $∀b［a_1∈R→［b∈R→［a_1≠0_R$

$→［b≠0_R→a_1b≠0_R］］］］$ 　　　14. ∀-導入

1　　　 (16)　 $∀a∀b［a∈R→［b∈R→［a≠0_R$

$→［b≠0_R→ab≠0_R］］］］$ 　　　15. ∀-導入