自然演繹法によるε-N 論法の分析
M2010MM022 川邊達治
指導教員：佐々木克巳

1

はじめに

本研究の目的は、自然演繹法の推論規則を拡張して、εN 論法を用いた証明を導出図で表現すること、および、その表現を用いて対象とする証明のしくみを明らかにすることである。具体的には、ε-N 論法を用いて証明されている 11 の性質を対象とし、次の I,II を行った。

I これらの証明を導出図で表現するために必要な推論規則を整理し、[1] の推論規則に追加した。この追加によって拡張された導出図で、ε-N 論法の証明を表現した。

1 （実数を表す）対象変数 ϵ,ϵ1 ,ϵ2 ,…,a, b, α, β, M ,…
2 （自然数を表す）対象変数 n, n1 ,…,N, N1 ,…,m, i,…
3 定数記号 0,1,2,…
4 関数記号 +, −, ||, ·, /, ()2 ,√, k,…

5 述語記号 =, ̸=, <, ≤6 論理記号 ∧, ∨, →, ∀, ∃, ¬, ⊥注：関数記号 “·” は省略することもある。

これらの記号の意味をふつうに解釈して、論理式と実際の文とを対応させる。本稿では、対応する論理式と実際の文を同一視して、同じ記号で表すこととする。
11 の性質の仮定（H1 , H2 ,…とおく）と結論（C とおく）に対応する論理式は以下である。

II I の導出図から、ε-N 論法における変数に代入すべき項の選択の仕組みを考察した。2 つの視点、すなわち、それらの項が、どの変数に依存して決まるか、
１．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))および、それらの項がどのように選ばれるのかに焦H2 :∀ϵ2 (0 < ϵ2 → ∃N2 ∀n2 (N2 ≤ n2 → |bn2 − β| < ϵ2 ))点を絞って考察した。そして、その仕組みによって、C:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → |an + bn − (α + β)| < ϵ))
11 の性質における「代入すべき項」が選ばれること
２．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))を示し、実際の証明を記述した。
H2 :∀ϵ2 (0 < ϵ2 → ∃N2 ∀n2 (N2 ≤ n2 → |bn2 − α| < ϵ2 ))本稿では、対象とした 11 の性質、I の外観、II の選択のC:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → |an · bn − α · β| < ϵ))仕組みについて述べる。

2

対象とする性質

本研究が対象とする 11 の性質を以下に示す。ここでは、自然数 (1, 2,…) 全体の集合を N とおく。
１．2 つの数列 {ai },{bi }(i ∈ N) がどちらも収束するならば、数列 {ai + bi }(i ∈ N) も収束する。
２．2 つの数列 {ai }, {bi }(i ∈ N) がどちらも収束するな
らば、数列 {ai · bi }(i ∈ N) も収束する。
３．3 つの数列 {ai }, {bi }, {ci }(i ∈ N) があって、すべての n に対して、an ≤ bn ≤ cn を満たすとする。このとき、{ai } も {ci } がどちらも α に収束するならば、{bi } も同じ α に収束する。
４．数列 {ai }(i ∈ N) が収束ならば、数列 { a1i }(i ∈ N) も収束する。
５．数列 {ai }(i ∈ N) が α に収束するならば、数列i}(i ∈ N) も同じ α に収束する。
{ a1 +···+ai６．数列 {ai }(i ∈ N) が α に収束ならば、数列 {ai } の任意の部分列 {aki }(i ∈ N) も同じ α に収束する。
７．コーシー列が収束する部分列をもつならば、もとのコーシー列自身も収束する。
８．数列 {ai }(i ∈ N) が α(̸= 0) に収束するとき、ある番号 N に対し、n ≥ N のすべての n に対して an は α と同符号である。
９．数列 {ai }(i ∈ N) の収束先は一意である。
10．数列 {ai }(i ∈ N) が α に収束し、すべての n に対して an ≤ b であるならば、α ≤ b である。
11．数列 { 1i }(i ∈ N) が 0 に収束する。
これらの性質の証明を導出図で表現するために、論理式は次の言語を用いて定義する。

３．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))H2 :∀ϵ2 (0 < ϵ2 → ∃N2 ∀n2 (N2 ≤ n2 → |cn2 − α| < ϵ2 ))H3 :∀m(am ≤ bm ∧ bm ≤ cm )C:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → |bn − α| < ϵ))４．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))C:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → | a1n − α1 | < ϵ))５．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))nC:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → | a1 +···+a− α| < ϵ))n６．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))H3 :∀m(m ≤ km )C:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → |akn − α| < ϵ))７．H1 :∀ϵ1 (0 < ϵ1 →∃N1 ∀n1 ∀n1 ′ (N1 ≤ n1 ∧ N1 ≤ n1 ′ → |an1 − an1 ′ | < ϵ1 ))H2 :∀ϵ(0 < ϵ2 → ∃N2 ∀n2 (N2 ≤ n2 → |akn2 − α| < ϵ2 ))H3 :∀m(m ≤ km )C:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → |an − α| < ϵ))８．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))C:∃N ∀n(N ≤ n →(α > 0 → an > 0) ∧ (α < 0 → an < 0))
９．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))H2 :∀ϵ2 (0 < ϵ2 → ∃N2 ∀n2 (N2 ≤ n2 → |an2 − β| < ϵ2 ))H3 :α ̸= βC:⊥
10．H1 :∀ϵ1 (0 < ϵ1 → ∃N1 ∀n1 (N1 ≤ n1 → |an1 − α| < ϵ1 ))H2 :∀n2 (an2 ≤ b)
H3 :α > bC:⊥

11．C:∀ϵ(0 < ϵ → ∃N ∀n(N ≤ n → | n1 − 0| < ϵ))4

代入すべき項が依存する変数

これらの論理式において、異なる役割の束縛変数は異な
この節と次の第 5 節で、ε-N 論法における変数に代入る記号を用いた。また、11 の性質ができる限り同じ形にすべき項の選択の仕組みについて述べる。
なるように記号を選んだ。これらによって II の考察を行
とくに、この節では、代入すべき項が、どの変数に依存いやすくなるからである。さらに、性質６と性質７では、して決まるのかを考える。結果として、証明すべき性質仮定に部分列が現れる。部分列の定義はの仮定に ∀ϵi ∃Ni …、結論に ∀n… の文が現れるか否かで、その依存する変数の傾向をまとめることができた。以下
数列 {aki } が数列 {ai } の部分列に詳細を述べる。
⇔ ∀i∀j(i < j → ki < kj )11 の性質の証明に対応する導出図の一部は、本論文のであるが、この右辺から導かれる ∀m(m ≤ km ) を仮定と付録 A に示してある。それらはどれも図 1 の形、または、して加えている。
そこから不要な推論規則を削除した形でかける。図 1 の導出図から、変数に代入すべき項について次がわかる。
3 自然演繹法

• ϵ, N1 , N2 , n に代入すべき項は、[1] の推論規則の変自然演繹法は、実際の証明を体系的に表現するための 1数条件を満たす。本研究では、異なる役割の束縛変つの形式的方法である。そこでは、推論規則を定め、それ数に異なる記号を用いていることから、ϵ, N1 , N2 , nらを組み合わせることにより、実際の証明を表現していに代入すべき項は、それぞれ、ϵ, N1 , N2 , n とすればる。その組合せの表現を導出図とよぶ。より具体的には、よい。
導出図とは、論理式が平面上に樹上に配置された図形で• ϵ1 ,ϵ2 に代入すべき項は ϵ のみに依存する。
ある。樹の根にあたる部分にある論理式を結論、葉にあたる部分にある論理式を仮定と呼ぶ。この構成は、[1] の• N に代入すべき項は ϵ,N1 ,N2 のみに依存する。
推論規則と以下に示す「追加すべき推論規則」に従うも• n1 ,n2 ,n1 ′ に代入すべき項は ϵ,N1 ,N2 ,n のみに依存のとする。この「追加すべき推論規則」は、[2],[3] などにする。
あるε-N 論法での証明を導出図で表現するのに必要と判
ϵ1 , ϵ2 , N, n1 , n2 , n1 ′ は、各性質の仮定と結論に自由に現断したものである。導出図 P が与えられたとき、P は、Pれる変数にも依存するが、本研究ではそのことを明記しの解消されていない仮定から、P の結論を導く証明を表ない。
すことになる。
本研究で実際に作成した導出図で代入された項を、表1に示しておく。ただし、性質2 には 3 通りの証明があ追加すべき推論規則
り、それらを 2A、2B、2C とした。性質 4 についても同不等式に関するもの様である。表 1 から、依存する変数の表を作ると表 2 のようになる。
s≤ts<t∨s=t(≤ 導)(≤ 除)
表 2 から、N へ代入すべき項については、仮定にs<t∨s=ts≤t“∀ϵs<t t<us<ti ∃Ni ” が現れるか否かで次の傾向が読み取れる。
(T ran)(< +)s<us+u<t+u現れるとき（性質 1〜8）
：Ni に依存現れないとき（性質 11）：ϵ のみに依存
s<t 0<u(< ×A)
us < ut
ただし、性質 5 においては ϵ にも依存する。
同様に、n1 , n2 へ代入すべき項については、結論に “∀n”
(M AXDef ) 注 1
ai ≤ max(a1 , · · ·, an )が現れるか否かで次の傾向が読み取れる。
現れるとき（性質 1〜8）：n に依存
絶対値に関するもの現れないとき（性質 9,10）：Ni のみに依存t<00<t(AbsDef A)(AbsDef B)
ただし、性質5においては、Ni にも依存する。
|t| = t|t| = −tt=0(AbsDef C)|t| = 0|s| = |t + u|
(T riIne)|s| ≤ |t| + |u|

0 < |s|(Abs 公理)|t − u| = |s|(T riIneA)|t| − |u| ≤ |s||s · t| = |s||t|(AbsM ul)数に関するもの0<0(N umAxiB)

0<t(InverA)
0 < 1t
注 1：i は 1 ≤ i ≤ n を満たす自然数とする。

5

代入すべき項の選び方

前節では、代入すべき項が、どの変数に依存するかについて述べた。この節では、それをもう一歩踏み込んで、
ϵ1 , ϵ2 , N, n1 , n2 に代入すべき具体的な項の選び方について述べる。
導出図（図 1）より、その項は、各性質に応じた次の形の条件を満たすように選べばよい。

∀n1 P1 , ∀n2 P2 , H3 ⇒ ∀nP(1)

ただし、∀n1 P1 , ∀n2 P2 , H3 , ∀nP のそれぞれは、性質によってはなかったり、⊥ であったりする。(1) を満たす項はP1 , P2 , H3 ⇒ P(2)を満たすように選べばよい。n1 に複数の項を代入する場合もある。この場合は、その複数の項を

ステップ１は、三角不等式(i.1)
P1 [n1,1 /n], …, P1 [n1,ℓ /n1 ], P2 , H3 ⇒ P|X + Y | ≤ |X| + |Y |(3)などを用いる。ステップ２は、を満たす n1,1 , …, n1,ℓ として選ぶことになる。以下は (2)の場合で、説明を続ける。さらに、P が N ≤ n → Q で、Pi が Ni ≤ ni → Qi の形のときは、3 条件(i.2)

N ≤ n（前提）(i.3)|A| < ϵ（前提）1(i.4)|B| < ϵ（前提）2N ≤ n ⇒ N1 ≤ n1(4)N ≤ n ⇒ N2 ≤ n2(5)(i.6)|α| − ϵ1 < |an |（A = an − αの場合, (i.3) より）

N ≤ n, Q1 , Q2 , H3 ⇒ Q

(6)

(i.7)

|β| − ϵ2 < |bn |（B = bn − β の場合, (i.4) より）(i.8)|an | < M（{ai } の有界性より）(i.5) H（前提）
3または、2 条件

N ≤ n ⇒ N1 ≤ n1(7)N ≤ n, Q1 , P2 , H3 ⇒ Q(8)などを満たすように選べばよい。最初の 3 条件の場合には、ϵ1 ,ϵ2 に代入すべき項は、(6) を満たすように選ぶ。Nに代入すべき項は、3 条件を満たすように選ぶ。条件などを用いる。(i.6) は、三角不等式と (i.3) から|α| − |an | ≤ |an − α| < ϵ1なので、ここから得られる。(i.7) も同様である。また、
ステップ２において、ϵi ≤ 1αϵi ≤2′∀N (N ≥ N ⇒ (4))∀N (N ≥ N ′′ ⇒ (5))
∀N (N ≥ N ′′′ ⇒ (6))
を 満 た す、N ′ ,N ′′ ,N ′′′ を そ れ ぞ れ 求 め て 、N=max(N ′ , N ′′ , N ′′′ ) と す れ ば よ い 。他 の 場 合 も 同 様 である。
次に (4) を満たす、N ,n1 に代入すべき項の選び方を述べる（(5),(7) も同様である）。本研究では、次の 2 通りの選び方があった。
・N1 ≤ N を満たす N ,n1 = N1 , N1 + 1, …, n・(N, n1 ) = (N1 , n)
最後に (6) を満たす ϵ1 , ϵ2 , N, n1 , n2 に代入すべき項の選び方を 2 つ述べる。（(8) も同様である）。
(i) 1 つ目は、(6) が N ≤ n, |A| < ϵ1 , |B| < ϵ2 , H3 ⇒|C| < ϵ の形のときの選び方である。この選び方は、具体的には、次の 3 つのステップからなる。
ステップ１：|C| ≤ C ′ を満たす C ′ でなどの条件を加えて f を求めて、ステップ３において加えた条件と、f ≤ ϵ を満たすように ϵi 選ぶを方法 (i.9) も有効である。加えた条件が、ϵi ≤ 1 のときは、f ≤ ϵ を満たす
ϵi を ϵi ′ とすると、ϵi に代入すべき項は、ϵi = min(1, ϵi ′ )とすればよい。
(ii) 2 つ目は、(6) の Qi または Q が |A − α| < ϵ の形のときの選び方である。具体的には、|A − α| < ϵ をα − ϵ < A < α + ϵ に変形し「⇒」の前後を比較する方法である。(i) で述べた (i.9) も有効である。

6

最後に

本論文では、新たな推論規則を導入し、自然演繹の枠組みを拡張することで、数列の収束に関するε-N 論法の証明を導出図で表現することができた。さらに、その過程の中で生じる変数の選択の結果を元に、代入すべき項の選択方法をまとめることが出来た。この方法を用いることで、実際の証明を書く際に、定義に合う記述が出来|A|, |B| の式(9) るようになる。多くの文献の中では、その部分が省略し|an |, |bn |, n の式て記述してあるので、なぜ、その項を代入するのか、との形のものを求める。ただし、x1 , x2 , …, xm の式とは、 いう疑問を解決することが出来た。
x1 , x2 , …, xm についての多項式ですべての係数が正であ 参考文献るもののことである。
[1] 鹿島亮：『数理論理学』. 朝倉書店, 東京,2009.
ステップ２：C ′ < f となる f で、ϵ1 , ϵ2 , N, n1 , n2 のみ[2] 一樂重雄：『集合と位相 そのまま使える答えの書きで表現されたものを求める。
方』. 講談社サイエンティフィク, 東京,2001.
ステップ３：f ≤ ϵ を満たすように ϵ1 , ϵ2 , N, n1 , n2 に代入すべき項を選ぶ。
最初の 2 つのステップで得られる C ′ , f は、|C| ≤ C ′ < fを満たすので、ステップ３で求めた項が、それぞれに代入すべき項だとわかる。

『微積分と集合 そのまま使える答えの書き[3] 飯高茂：方』. 講談社サイエンティフィク, 東京,1999.

∀n1 (…

)(∀ 除)

..
.
..
∀ϵ2 …
.
(∀ 除)
..
∀ϵ…
0<ϵ0<ϵ122 → ∃N2 …
.
(∀ 除)
(→ 除)
(→ 除)
0 < ϵ10 < ϵ1 → ∃N1 …
∃N2 …
(→ 除)
∃N1 …
∃N 〜
(∃ 除)
∃N 〜
(→ 導)
0 < ϵ → ∃N 〜(∀ 導)∀ϵ( … )
図 1 導出図の一般形

表1
変数

ϵ1ϵ2

１2A2B2C

ϵ2ϵ2３4A
4B
５６７８2A の ϵ′ は −1 +〜)..
.

n1n2n1 ′mnnnnnnnn--|β|ϵ′min(1, ϵ′′ )

ϵ2M

ϵ2|α|

max(N1 , N2 )max(N1 , N2 )max(N1 , N2 )max(N1 , N2 )ϵϵmax(N1 , N2 )nn-n-

N1n----

N1n---

ϵ-ϵ2ϵ2|α−β|2N1 ,N1 + 1,…,nknnnmax(N1 , N2 )N1-nmax(N1 , N2 )N1-kn-nn-|α−β|2max(N1 , N3 )N1max(N1 , N2 )N1[ 1ϵ ] + 1|α|-α−b--(∀ 除)..
.
∀n〜(∃ 導)∃N 〜(∃ 除)|α|ϵ′min(1, ϵ′′ )|α|2 ϵmin( |α|2 , 2 )|α|2 ϵ1+|α|ϵϵ2９1011代入すべき項
N∀n2 (-√2(a −α+…+aN1 −α)ϵϵ
1 + |αβ|を表す。 2B の ϵ′′ は 1+|α|+|β|を表す。 ５の N3 は [ 1] + 1 を表す。
ϵ表2変数

ϵ1ϵ2

１2A2B
2C
３4A4B
５６７８９1011ϵϵ
ϵϵϵϵϵϵϵϵなし
なし
なし-ϵϵϵϵϵϵϵなし-依存する変数
Nn1

N1 , N2
N1 , N2
N1 , N2
N1 , N2
N1 , N2
N1N1
N1 , ϵ
N1N1 , N2
N1ϵnnnnnnn
N1 , nnnn
N1 , N2N1-n2n1 ′mnnnnn−nN1 , N2N1-n-nnn-