バー誘導

バー帰納法は、 LEJ Brouwerによって導入された直観主義数学で使用される推論原理です。バー帰納法の主な用途は、一様連続定理の導出に使用される重要な結果である扇定理の直観主義的導出です。

また、他の古典的な結果 に対する建設的な代替案を提供するのにも役立ちます。

この原理の目的は、自然数のすべての無限列（直観主義用語では選択列と呼ばれる）の特性を有限リストの特性に帰納的に還元することによって証明することです。バー帰納法は、スプレッド（特別な種類の集合） 内のすべての選択列に関する特性を証明するためにも使用できます。

選択シーケンスが与えられた場合、このシーケンスの要素の任意の有限シーケンスは、この選択シーケンスの初期セグメントと呼ばれます。 ${\displaystyle x_{0},x_{1},x_{2},x_{3},\ldots }$${\displaystyle x_{0},x_{1},x_{2},x_{3},\ldots ,x_{i}}$

現在、文献には 3 つの形式のバー帰納法が記載されており、それぞれが述語のペアに特定の制限を課し、主な違いは太字で強調表示されています。

有限の自然数列に関する 2 つの述語と、次の条件がすべて満たされる場合:${\displaystyle R}$${\displaystyle A}$

• すべての選択シーケンスには、ある時点で を満たす初期セグメントが少なくとも 1 つ含まれます(これは、 がバーであると表現されます)。${\displaystyle R}$${\displaystyle R}$
• ${\displaystyle R}$決定可能である（つまり、バーは決定可能である）。
• を満たすすべての有限シーケンスは、 も満たします（前述の有限シーケンスから始まるすべての選択シーケンスについて成り立ちます）。${\displaystyle R}$${\displaystyle A}$${\displaystyle A}$
• 有限列の 1 つの要素による拡張がすべて を満たす場合、その有限列は も満たします(これは上方遺伝であると言われることがあります)。${\displaystyle A}$${\displaystyle A}$${\displaystyle A}$

すると、空のシーケンスに対しては A が成り立つ と結論付けることができます(つまり、空のシーケンスから始まるすべての選択シーケンスに対して A が成り立ちます)。${\displaystyle A}$

このバー誘導の原理は、 AS Troelstra、SC Kleene 、および Albert Dragalinの著作で支持されています。

有限の自然数列に関する 2 つの述語と、次の条件がすべて満たされる場合:${\displaystyle R}$${\displaystyle A}$

• すべての選択シーケンスには、ある時点で を満たす一意の初期セグメントが含まれます(つまり、バーは細い)。${\displaystyle R}$
• を満たすすべての有限列はも満たします。${\displaystyle R}$${\displaystyle A}$
• 有限列の 1 つの要素による拡張がすべて を満たす場合、その有限列は も満たします。${\displaystyle A}$${\displaystyle A}$

すると、空のシーケンスに対してはそれが当てはまると結論付けることができます。 ${\displaystyle A}$

このバー帰納法の原理は、 Joan Moschovakisの著作で好まれており、（直観的に）決定可能なバー帰納法と同等であることが証明されています。

有限の自然数列に関する 2 つの述語と、次の条件がすべて満たされる場合:${\displaystyle R}$${\displaystyle A}$

• すべての選択シーケンスには、ある時点で条件を満たす少なくとも 1 つの初期セグメントが含まれます。${\displaystyle R}$
• 有限列が を満たす場合、その有限列のあらゆる可能な拡張も を満たします${\displaystyle R}$${\displaystyle R}$(つまり、バーは単調です)。
• を満たすすべての有限列はも満たします。${\displaystyle R}$${\displaystyle A}$
• 有限列の 1 つの要素による拡張がすべて を満たす場合、その有限列は も満たします。${\displaystyle A}$${\displaystyle A}$

すると、空のシーケンスに対してはそれが当てはまると結論付けることができます。 ${\displaystyle A}$

このバー誘導の原理は、 AS Troelstra、SC Kleene、Dragalin、Joan Moschovakisの研究で使用されています。

これらのスキーマに関する以下の結果は直観的に証明できます。

${\displaystyle {\begin{aligned}BI_{M}&\vdash BI_{D}\\[3pt]BI_{D}&\vdash BI_{T}\\[3pt]BI_{T}&\vdash BI_{ D}\end{整列}}}$

（記号「」は「回転式改札口」です。） ${\displaystyle \,\vdash \,}$

バー帰納法の追加のスキームは、もともとBrouwer (1975) によって「余分な」制限を含まない定理としてバー定理という名前で与えられました。しかし、この定理の証明は誤りであり、制限のないバー帰納法は直観的に有効であるとは考えられていません (これがなぜそうなのかの要約については、Dummett 1977 pp 94–104 を参照してください)。完全性のために、制限のないバー帰納法のスキームを以下に示す。 ${\displaystyle R}$

有限の自然数列に関する 2 つの述語と、次の条件がすべて満たされる場合:${\displaystyle R}$${\displaystyle A}$

• すべての選択シーケンスには、ある時点で条件を満たす少なくとも 1 つの初期セグメントが含まれます。${\displaystyle R}$
• を満たすすべての有限列はも満たします。${\displaystyle R}$${\displaystyle A}$
• 有限列の 1 つの要素による拡張がすべて を満たす場合、その有限列は も満たします。${\displaystyle A}$${\displaystyle A}$

すると、空のシーケンスに対してはそれが当てはまると結論付けることができます。 ${\displaystyle A}$

古典的な逆数学では、「バー帰納法」（）は、関係が整列している場合、任意の式に対して に対する超限帰納法のスキームがあることを述べる関連原理を表します。 ${\displaystyle BI_{D}}$${\displaystyle R}$${\displaystyle R}$

• LEJ Brouwer Brouwer, LEJ Collected Works、第1巻、アムステルダム：北ホラント（1975年）。
• ドラガリン、アルバート G. (2001) [1994]、「バー帰納法」、数学百科事典、EMS プレス
• マイケル・ダメット『直観主義の要素』クラレンドン・プレス（1977年）
• SC Kleene、RE Vesley、「直観主義数学の基礎：特に再帰関数との関係において」、North-Holland (1965)
• Michael Rathjen、「バールールとバー誘導におけるパラメータの役割」、Journal of Symbolic Logic 56 (1991)、第2号、715-730頁。
• AS Troelstra、Choice Sequences、Clarendon Press (1977) より
• AS TroelstraとDirk van Dalen 著、「数学における構成主義」、論理学と数学の基礎研究、Elsevier (1988)