代入原理,+
2017/2/1
thm2.4とthm2.5を追加変更しました
〇健全な研究室
さトぅー
「天々城、代入原理はどうするの？
アレがないと=の変形はキツイわよ」
天々城
「あー、そうだナ。
しかもまた帰納法」
■meta_thm2.1(論理式の代入原理)
t_0,...,t_n,u_0,...,u_n:項
x_0,...,x_n:変数記号
φ:論理式
すべての自然数nについて
{(t_0 = u_0),...,(t_n = u_n)} |- ( (...(φ[t_0/x_0])...[t_n/x_n]) ⇔ (...(φ[u_0/x_0])...[u_n/x_n]) )
proof
・n = 0のとき
1 (∀x (∀y ((x = y)⇒((φ[x/x_0])⇒(φ[y/x_0]))))) [Ax7]
2 ((t_0 = u_0)⇒((φ[t_0/x_0])⇒(φ[u_0/x_0]))) [AAel 1]
3 (t_0 = u_0) [ax]
4 ((φ[t_0/x_0])⇒(φ[u_0/x_0])) [⇒el 3,2]
5 ((u_0 = t_0)⇒((φ[u_0/x_0])⇒(φ[t_0/x_0]))) [AAel 1]
6 (u_0 = t_0) [=の可換性 3]
7 ((φ[u_0/x_0])⇒(φ[t_0/x_0])) [⇒el 6,5]
8 ((φ[t_0/x_0])⇔(φ[u_0/x_0])) [⇔in 4,7]
よって、すべての論理式φと項t_0,u_0と変数記号x_0について
{(t_0 = u_0)} |- ( (φ[t_0/x_0]) ⇔ (φ[u_0/x_0]) )
・n = kのとき
{(t_0 = u_0),...,(t_k = u_k)} |- ( (...(φ[t_0/x_0])...[t_k/x_k]) ⇔ (...(φ[u_0/x_0])...[u_k/x_k]) )
とすると、n = k+1のとき
1 (t_0 = u_0) [ax]
:
:
k+1 (t_k = u_k) [ax]
k+2 ( (...(φ[t_0/x_0])...[t_k/x_k]) ⇔ (...(φ[u_0/x_0])...[u_k/x_k]) )
[n = kのとき{(t_0 = u_0),...,(t_k = u_k)} |- ( (...(φ[t_0/x_0])...[t_k/x_k]) ⇔ (...(φ[u_0/x_0])...[u_k/x_k]) )]
k+3 (t_(k+1) = u_(k+1)) [ax]
k+4 ( ((...(φ[t_0/x_0])...[t_k/x_k])[t_(k+1)/x_(k+1)]) ⇔ ((...(φ[u_0/x_0])...[u_k/x_k])[u_(k+1)/x_(k+1)]) )
[ すべての論理式φと項t_0,u_0と変数記号x_0について{(t_0 = u_0)} |- ( (φ[t_0/x_0]) ⇔ (φ[u_0/x_0]) ) ]
よって
{(t_0 = u_0),...,(t_k = u_k),(t_(k+1) = u_(k+1))}
|- ( ((...(φ[t_0/x_0])...[t_k/x_k])[t_(k+1)/x_(k+1)]) ⇔ ((...(φ[u_0/x_0])...[u_k/x_k])[u_(k+1)/x_(k+1)]) )
数学的帰納法より、
すべての自然数nについて
{(t_0 = u_0),...,(t_n = u_n)} |- ( (...(φ[t_0/x_0])...[t_n/x_n]) ⇔ (...(φ[u_0/x_0])...[u_n/x_n]) )
■
天々城
「自分で証明しておいてなんだが、なにが起こったかんだって感じだ」
さトぅー
「一気に代入できるってだけでしょ」
エーリル
「確かに」
ディアナ
「長いですからね、多少は仕方ないでしょう」
天々城
「いやわかってるんだがナ、強力な一般性の前に圧倒されたんだ」
■meta_thm2.2(項の代入原理)
t_0,..,t_n,u_0,...,u_n,v:項
x_0,...,x_n:変数記号
すべての自然数nについて
{(t_0 = u_0),...,(t_n = u_n)} |- ( (...(v[t_0/x_0])...[t_n/x_n]) = (...(v[u_0/x_0])...[u_n/x_n]) )
proof
1 (t_0 = u_0) [ax]
:
:
n+1 (t_n = u_n) [ax]
n+2 ( ( (...(v[t_0/x_0])...[t_n/x_n]) = ( (...(v[t_0/x_0])...[t_n/x_n]) )
⇔( (...(v[t_0/x_0])...[t_n/x_n]) = (...(v[u_0/x_0])...[u_n/x_n]) ) ) [論理式の代入原理 1,...,n+1]
n+3 ( (...(v[t_0/x_0])...[t_n/x_n]) = ( (...(v[t_0/x_0])...[t_n/x_n]) ) [=の反射性]
n+4 ( (...(v[t_0/x_0])...[t_n/x_n]) = (...(v[u_0/x_0])...[u_n/x_n]) ) [⇔elL 2,3]
■
天々城
「強力な一般性を使えば、項の代入原理は秒殺できる」
エーリル
「強力な一般性」
天々城
「ここから本題だ。今から自然数を調べる」
エーリル
「やった」
天々城
「まずは小手調べだ。
圧倒的表現力に恐れおののくがいい」
■thm2.1
0:定数記号
S:項数1の関数記号
m,n:変数記号
PA |- (∀m ((m = 0)∨(∃n (m = S(n)))))
proof
1 (0 = 0) [=の反射性]
2 ((0 = 0)∨(∃n (0 = S(n)))) [∨inR 1]
k:変数記号
3 ((k = 0)∨(∃n (k = S(n)))) [ax]
4 (k = 0) [ax]
5 (S(k) = S(0)) [項の代入原理 4]
6 (∃n (S(k) = S(n))) [∃in 5]
7 ((S(k) = 0)∨(∃n (S(k) = S(n)))) [∨inL 6]
8 ((k = 0)⇒((S(k) = 0)∨(∃n (S(k) = S(n))))) [⇒in 7 el 4]
9 (∃n (k = S(n))) [ax]
10 (k = S(n)) [ax]
11 (S(k) = S(S(n))) [項の代入原理 10]
12 (∃n (S(k) = S(n))) [∃in 11]
13 ((k = S(n))⇒(∃n (S(k) = S(n)))) [⇒in 12 el 10]
14 (∀n ((k = S(n))⇒(∃n (S(k) = S(n))))) [∀in 13]
15 (∃n (S(k) = S(n))) [∃el 9,14]
16 ((S(k) = 0)∨(∃n (S(k) = S(n)))) [∨inL 15]
17 ((∃n (k = S(n)))⇒((S(k) = 0)∨(∃n (S(k) = S(n))))) [⇒in 16 el 9]
18 ((S(k) = 0)∨(∃n (S(k) = S(n)))) [∨el 3,8,17]
19 (((k = 0)∨(∃n (k = S(n))))⇒((S(k) = 0)∨(∃n (S(k) = S(n))))) [⇒in 18 el 3]
20 (∀k (((k = 0)∨(∃n (k = S(n))))⇒((S(k) = 0)∨(∃n (S(k) = S(n)))))) [∀in 19]
21 (∀m ((m = 0)∨(∃n (m = S(n))))) [数学的帰納法 3,20]
■
天々城
「これはどんな自然数にも一つ前の自然数があるか、0のいずれかだって話だナ」
エーリル
「圧倒的表現力だ」
ディアナ
「命題論理に比べると情報量が全然違いますね」
天々城
「圧倒的表現力を上げた分、文字数も圧倒的増加。
当たり前といえば当たり前だナ」
ディアナ
「確かにそういう考え方もあると思います」
天々城
「ここから先は、巷で流行りの計算の順序に関する定理だ」
■thm2.2(+の結合性)
m,n,l:変数記号
+:項数2の関数記号
PA |- (∀m (∀n (∀l (((m+n)+l) = (m+(n+l))))))
proof
1 (∀n ((n+0) = n)) [PA2]
2 (((m+n)+0) = (m+n)) [∀el 1]
3 ((n+0) = n) [∀el 1]
4 ((m+(n+0)) = (m+n)) [項の代入原理 3]
5 ((m+n) = (m+(n+0))) [=の可換性 4]
6 (((m+n)+0) = (m+(n+0))) [=の推移性 2,5]
k:変数記号
7 (((m+n)+k) = (m+(n+k)) [ax]
8 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
9 (((m+n)+S(k)) = S(((m+n)+k))) [AAel 8]
10 (S(((m+n)+k)) = S((m+(n+k)))) [項の代入原理 7]
11 ((m+S((n+k))) = S((m+(n+k)))) [AAel 8]
12 (S((m+(n+k))) = (m+S((n+k)))) [=の可換性 11]
13 ((n+S(k)) = S((n+k))) [AAel 8]
14 ((m+(n+S(k)))=(m+S((n+k)))) [項の代入原理 13]
15 ((m+S((n+k))) = (m+(n+S(k)))) [=の可換性 14]
16 (((m+n)+S(k)) = (m+(n+S(k)))) [=の4推移性 9,10,12,15]
17 ((((m+n)+k) = (m+(n+k))⇒(((m+n)+S(k)) = (m+(n+S(k))))) [⇒in 16 el 7]
18 (∀l (((m+n)+l) = (m+(n+l)))) [数学的帰納法 6,17]
19 (∀n (∀l (((m+n)+l) = (m+(n+l))))) [∀in 18]
20 (∀m (∀n (∀l (((m+n)+l) = (m+(n+l)))))) [∀in 19]
■
天々城
「だから、自然数の足し算のかっこの位置は変えられる」
エーリル
「言われてみれば((1+2)+3)と(1+(2+3))は同じか」
ディアナ
「やはり命題論理とは表現力が違いますね。
項の操作ができるだけでここまで差があるとは」
天々城
「普通の数学は一階述語論理で議論できるからナ。
定義さえわかれば感覚もつかめて、最終的に大体なんとかなる」
■thm2.3(+の左単位元)
n:変数記号
+:項数2の関数記号
PA |- (∀n ((0+n) = n))
proof
1 (∀n ((n+0) = n)) [PA2]
2 ((0+0) = 0) [∀el 1]
k:変数記号
3 ((0+k)=k) [ax]
4 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
5 ((0+S(k)) = S((0+k))) [AAel 4]
6 (S((0+k)) = S(k)) [項の代入原理 3]
7 ((0+S(k)) = S(k)) [=の推移性 5,6]
8 (((0+k)=k)⇒((0+S(k)) = S(k))) [⇒in 7 el 3]
9 (∀k (((0+k)=k)⇒((0+S(k)) = S(k)))) [∀in 8]
10 (∀n ((0+n) = n)) [数学的帰納法 2,9]
■
天々城
「これはPA2と見比べた方がいい」
(∀n ((0+n) = n)) [自然数と+の左単位元]
(∀n ((n+0) = n)) [PA2]
エーリル
「0とnが反対になってる」
天々城
「そう。PA2は自然数と+の右単位元があると言っているわけだ」
エーリル
「単位元ってなに？」
天々城
「なにか合わせたときに変えないモノなんだが、PA2と自然数と+の左単位元が定義そのものだからナ」
エーリル
「定義なら仕方がない」
天々城
「そしてお前らに+の魔境を見せてやる」
エーリル
「＋の魔境」
天々城
「+の可換性を証明しようとすると、((k+S(m)) = (S(k)+m))の変形をする瞬間に+が牙をむく。
だからその前に倒す」
■thm2.4
k,m:変数記号
S:項数1の関数記号
+:項数2の関数記号
PA |- (∀k (∀m ((k+S(m)) = (S(k)+m))))
proof
1 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
2 ((k+S(0)) = S((k+0))) [AAel 1]
3 (∀n ((n+0) = n)) [PA2]
4 ((k+0) = k) [∀el 3]
5 (S((k+0)) = S(k)) [項の代入原理 4]
6 (S(k) = (S(k)+0)) [∀el 3]
7 ((k+S(0)) = (S(k)+0)) [=の3推移性 2,5,6]
l:変数記号
8 ((k+S(l)) = (S(k)+l)) [ax]
9 ((k+S(S(l))) = S((k+S(l)))) [AAel 1]
10 (S((k+S(l))) = S((S(k)+l))) [項の代入原理 8]
11 ((S(k)+S(l)) = S((S(k)+l))) [AAel 1]
12 (S((S(k)+l)) = (S(k)+S(l))) [=の可換性 11]
13 ((k+S(S(l))) = (S(k)+S(l))) [=の3推移性 9,10,12]
14 (((k+S(l)) = (S(k)+l))⇒((k+S(S(l))) = (S(k)+S(l)))) [⇒in 13 el 8]
15 (∀l (((k+S(l)) = (S(k)+l))⇒((k+S(S(l))) = (S(k)+S(l))))) [∀in 14]
16 (∀m ((k+S(m)) = (S(k)+m))) [数学的帰納法 7,15]
17 (∀k (∀m ((k+S(m)) = (S(k)+m)))) [∀in 16]
■
天々城
「無事に倒せたから本番だ」
■thm2.5(+の可換性)
m,n:変数記号
+:項数2の関数記号
PA |- (∀m (∀n ((m+n) = (n+m))))
proof
1 (∀n ((n+0) = n)) [PA2]
2 ((m+0) = m) [∀el 1]
3 (∀n ((0+n) = n)) [+の左単位元]
4 ((0+m) = m) [∀el 3]
5 (m = (0+m)) [=の可換性 4]
6 ((m+0) = (0+m)) [=の推移性 2,5]
k:変数記号
7 ((m+k) = (k+m)) [ax]
8 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
9 ((m+S(k)) = S((m+k))) [AAel 8]
10 (S((m+k)) = S((k+m))) [項の代入原理 7]
11 ((k+S(m)) = S((k+m))) [AAel 8]
12 (S((k+m)) = (k+S(m))) [=の可換性 11]
13 (∀k (∀m ((k+S(m)) = (S(k)+m)))) [thm2.4]
14 ((k+S(m)) = (S(k)+m)) [AAel 13]
15 ((m+S(k)) = (S(k)+m)) [=の4推移性 9,10,12,14]
16 (((m+k) = (k+m))⇒((m+S(k)) = (S(k)+m))) [⇒in 15 el 7]
17 (∀k (((m+k) = (k+m))⇒((m+S(k)) = (S(k)+m)))) [∀in 16]
18 (∀n ((m+n) = (n+m))) [数学的帰納法 6,17]
19 (∀m (∀n ((m+n) = (n+m)))) [∀in 18]
■
天々城
「+の魔境は超えたナ」
エーリル
「+の魔境だ……」
