記号化により理解する証明のしくみ
2009SE193 永井千尋
指導教員：佐々木克巳

はじめにその組み合わせと，実際に行う推論に対応する規則を積み上げてできる図で表現する．
本研究の目的は，証明すべき文の記号化によって，そ性質 1. 整数 a, b, c, d が等式 a2 + b2 + c2 = d2 を満たすとの証明を導く過程を理解することである．具体的には，する．d が 3 の倍数でないならば，a, b, c の中に 3 の倍数
1. 証明すべき文の適切な記号化がちょうど 2 つあることを示せ ([6])．
2. 証明における各推論規則が用いられる理由[記号化]を考える．1 の理解には，[1],[4] を用いた．2 は，前件と「a, b, c の中に 3 の倍数が k 個ある」を P (k) とおく．
後件をペアにしたシークエントを基本表現とするシーク
今回は，「a, b, c の中に 3 の倍数がちょうど 2 個ある」のエント体系をもとに考える．特にその体系 SNK に基づくで，P (2) となる．これを用いて記号化する．すると，求推論については，SNK の性質から，その理由づけを行う．
める記号化は対象とする文は，[5],[6] から抽出した整数・実数の性質でa2 + b2 + c2 = d2 → 3 ̸ | d ⊃ P (2)ある．これらの性質に対し，その記号化，SNK に基づく証明，その推論を用いた理由，実際の証明を記述する． である．
本稿では，2 節で，用いる記号を導入し，シークエント [SNK に基づく証明]
図 1 に示す．
体系 SNK における推論の適用法を示す．3 節では，この[各推論の解説]研究で扱った具体的な証明のうち 2 つを示す．なお，SNK[1]∼[2]: SNK の優先順位から (⊃ 右) を選ぶ．
推論規則は，[3] に示されたものを使う．
[2]∼[3]: 3 ̸ | d から，3 で割ったときの余りに注目すると，2 記号法と体系 SNK
d = 3n + 1 ∨ d = 3n + 2 とおける．
[3]∼[4]: a2 + b2 + c2 = d2 が前提にあるので，これを用2.1 用いる記号と意味いるために d2 を計算する．
ここでは記号表現に用いる記号を導入する．
[4]∼[5]: 使用できる推論規則は，背理法 (RAA) のみであ• 論理記号：¬(でない), ∧(かつ), ∨(または), ⊃(ならる．また，¬P (2) は P (0) ∨ P (1) ∨ P (3) と同値であるこば), ∀(すべて/任意の), ∃(ある/存在する)とから，情報を取り出しやすいため，背理法を使う．
• 関係を表す記号：=, ∈, | (「x が y を割り切る」を [5]: P (0), P (1), P (3) の各場合について，a2 + b2 + c2 を
x | y と表現)
計算すると，3m, 3m + 2(m は整数) のいずれかになる．
よって，a2 + b2 + c2 = d2 に矛盾する．
• 関数を表す記号：普通の四則演算の記号と mod• 特定の集合を表す記号：Q(有理数全体), Z(整数全体) [実際の証明]
d は 3 の倍数でないので，2.2 SNK 推論規則の適用順序
d = 3n + 1, 3n + 2(n は整数)
体系 SNK における，シークエント S の証明は，S から のいずれかが成り立つ．それぞれの 2 乗を計算すると，SNK 推論規則を積み上げることによって作成できる．以d2 = (3n + 1)2 = 3(3n2 + 2n) + 1
下に，S からどのように SNK 推論規則を積み上げるべき
d2 = (3n + 2)2 = 3(3n2 + 4n + 1) + 1
かについて，[2] で述べられている方針を列挙する．
である．よって，• 上式が 2 つの規則 (∧ 右),(∨ 左),(⊃ 左) は後 (上) でd2 を 3 で割った余りは 1(∗1)
適用する．となる．ここで，背理法により，「a, b, c の中に 3 の倍数がちょうど 2 つある」の否定，すなわち，次の (i),(ii),(iii)• (∃ 左),(∀ 右),(∀ ⊃ 右) は先 (下) で適用する．
• SNK 推論規則の積み上げ方が明らかでないときは， のいずれかが成り立つとして矛盾を導く．
(i)a, b, c がすべて 3 の倍数のとき失敗しない規則 (上式と下式の証明可能性が同値で(ii)a, b, c のうち 1 つだけが 3 の倍数のときある規則) は先 (下) で適用する．
(iii)a, b, c がどれも 3 の倍数でないとき• 上式が下式より複雑な規則 (RAA),(cut) は後 (上) で(i) のとき，a2 + b2 + c2 は 3 で割り切れるので，a2 + b2 +適用する．
c2 = d2 より d2 も 3 の倍数．これは (∗1) に矛盾する．
(ii),(iii) のとき，(∗1) と同様にして，a2 + b2 + c2 を 3 で3 証明のしくみ割った余りは，(ii) のときは 2 となり，(iii) のときは 0 と
この節では，[5],[6] から抽出した整数・実数の性質 (2なる．これは，(∗1) に矛盾する．
つ) に対し，その記号化，SNK に基づく証明，その推論(i)〜(iii) より，d が 3 の倍数でないならば，a, b, c の中にを用いた理由，実際の証明を述べる．SNK に基づく証明
3 の倍数がちょうど 2 つある．
2は，与えられたシークエントから SNK 推論規則，または1√性質 2.a, b が有理数のとき，a+b 2 = 0 ならば a = b = 0 (ii)b ̸= 0 のとき√√であることを証明せよ．ただし， 2 は無理数である ([5])．
a+b 2=0√[記号化]
2 = − ab√√「x が有理数である」は x ∈ Q，「x が無理数である」は よって， 2 は有理数である．これは， 2 が無理数であx ̸∈ Q と記号化できるので，求める記号化はることに矛盾する．したがって，b ̸= 0 のときは起こら√√
2 ̸∈ Q, a ∈ Q ∧ b ∈ Q → a + b 2 = 0 ⊃ a = 0 ∧ b = 0 ない．
(i),(ii) より，a = b = 0 である．
である．
√
よって，a, b が有理数であるとき a + b 2 = 0 ならば[SNK に基づく証明]
a = b = 0 である．
2
図 2 に示す．
[各推論の解説][1]∼[2]: SNK の優先順位から (⊃ 右) を選ぶ．
[2]∼[3]: SNK の優先順位から選ぶと，(∧ 右) となる．その左の上式の証明図を示すと，以下のようになる．

おわりに

4

この研究を行うにあたり，正しく記号化することで，文の構造や内容が見えてくるため，実証明がどのようにし√√て成り立っているのか理解できるということがわかった．
2 ̸∈ Q, a ∈ Q, b ∈ Q, a + b 2 = 0, a ̸= 0 →⊥(RAA)√√
また複雑な問題は，和文を直接記号化するのではなくキー
2 ̸∈ Q, a ∈ Q, b ∈ Q, a + b 2 = 0 → a = 0
ワードを抜き出して，それを記号に置き換えて記号化す
この図から，左の上式の証明が困難なものとわかるため，ることで，証明図が簡略化され見やすくなることがわかっ(cut) で排中律を入れる方法を用いる．
た．
[3]∼[4]: SNK の優先順位から (∨ 左) を選ぶ．
今後は，本研究をどのように数学教育に役立てていけ[4]∼[5]: [4] を下式とする (∧ 右) の右の上式を考えると，るかや，どのような時期にならば取り入れることが可能
左辺にも b ̸= 0 があることから，右辺の b = 0 は ⊥ でもなのかということも考えていきたい．
証明できるはずである．すなわち [4] は，[4] の右辺を ⊥にしても証明できることになる．このことから，(w 右) 参考文献
[1] 新井紀子：『数学は言葉』, 東京図書, 東京，2009.
を選ぶ．
[5]∼[6]: SNK の優先順位から (¬ 左) を選ぶ．
[2] 佐々木克巳: 『南山大学情報理工学部講義科目「数理[6]∼[7]: 「x は有理数である」は，x ∈ Q の他に ∃m ∈論理学」講義資料』,2011.
√aZ∃n ∈ Z(x = m)と表すことができる．左辺に
2=−nb[3] 佐々木克巳: 「シークエント体系の証明図から実証明があり，右辺も同じ様な形にしたいため，(∃ 右) を選ぶ．
を作る方法」, アカデミア情報理工学編第 11 巻, pp.35[実際の証明]√54,2011.
a + b 2 = 0 を仮定する．ここで，b = 0 または b ̸= 0
[4] 佐々木克巳: 『南山大学大学院数理情報研究科講義科は明らかなので，2 通りで場合分けをする．
目「数理論理学研究」補充資料 1』,2012.
(i)b = 0 のとき√[5] チャート研究所: 『新課程 チャート式 基礎からのa+b 2=0√
数学 I+A』, 数研出版, 東京,2003.
a = −b 2

a=0[6] 柳川高明: 『新課程 チャート式 数学 A』, 数研出版, 東京,2003.

よって，a = b = 0 である．

a2 + b2 + c2 = d2 , d2 = 3(3n2 + 2n) + 1 ∨ d2 = 3(3n2 + 4n + 1) + 1, P (0) ∨ P (1) ∨ P (3) →⊥a + b + c = d , d = 3(3n + 2n) + 1 ∨ d = 3(3n + 4n + 1) + 1 → P (2)22222222

a2 + b2 + c2 = d2 , d = 3n + 1 ∨ d = 3n + 2 → P (2)2a + b + c = d , 3 ̸ | d → P (2)[2]a2 + b2 + c2 = d2 → 3 ̸ | d ⊃ P (2)[1]2図122[4][3](⊃ 右)性質 1 の SNK に基づく証明√√
2 = − ab → 2 = − ab [7]
(∃ 右)
√
√
b ̸= 0, 2 = − ab → 2 ∈ Q [6](¬左)√√[5]b ̸= 0, 2 ̸∈ Q, 2 = − ab →⊥(w 右)√√√b = 0, a = −b 2 → a = 0 ∧ b = 0 b ̸= 0, 2 ̸∈ Q, 2 = − ab → a = 0 ∧ b = 0 [4](∨左)√√b ̸= 0 ∨ b = 0, 2 ̸∈ Q, a ∈ Q, b ∈ Q, a + b 2 = 0 → a = 0 ∧ b = 0 [3](cut, 排中律)√√
2 ̸∈ Q, a ∈ Q ∧ b ∈ Q, a + b 2 = 0 → a = 0 ∧ b = 0 [2](⊃ 右)√√2 ̸∈ Q, a ∈ Q ∧ b ∈ Q → a + b 2 = 0 ⊃ a = 0 ∧ b = 0 [1]図2

性質 2 の SNK に基づく証明[5](RAA)