コンテンツへスキップ
Topos Uranos
日本語

自然数と論理式に関する帰納法

要約

命題論理の論理式は無限にあり、そのすべてについての主張には、一つずつ調べることによらない方法が必要である。この課はその方法を二段階で組み立てる。第一段は自然数に関する帰納法であり、単純な形と、単純な形から導かれる累積帰納法の形とがある。第二段は論理式の複雑さに関する帰納法、すなわち構造帰納法であり、長さに関する累積帰納法によって正当化される。これを用いて白丸と黒丸の言語の重みの補題（すべての論理式の重みは +1+1 であり、空でない真の語単位の接頭辞の重みはどれも高々 00 である）を証明し、そこから、どの論理式もほかの論理式の真の接頭辞ではないことを導き、さらにそこから一意読み取り可能性を導く。すなわち、各複合論理式は、先頭の黒丸と二つの成分とにただ一通りに分解される。最後に、一意読み取り可能性によって、論理式上の再帰的定義（長さ、変数と結合子の黒丸の個数、部分論理式、深さ）と、部分論理式への別の論理式の代入とが正当化される。

学習目標

  1. 単純な帰納法と累積帰納法によって自然数の性質を証明し、基底を確かめ、誤った帰納法の欠陥を突き止める。
  2. 変数と唯一の形成規則だけを場合として扱い、すべての論理式がある性質をもつことを複雑さに関する帰納法で証明する。
  3. 重みの補題を証明し、そこから、どの論理式もほかの論理式の真の接頭辞ではないこと、およびすべての複合論理式が一意に読み取れることを導く。
  4. 論理式上の関数（長さ、深さ、部分論理式、代入）を再帰によって定義し、それらの間の関係を帰納法で証明する。

すべての論理式についての主張

命題論理の言語の課では、白丸と黒丸と呼ぶ二つの記号 ∘\sigO と ∙\sigI、およびただ一つの形成規則から論理式を構成した。論理式は無限にあり、重要な主張の多くはそのすべてにかかわる。すべての論理式は黒丸で終わること、どの論理式も二通りには読めないこと、どの論理式でも変数が結合子の黒丸より一つ多いこと、などである。こうした主張は、研究している言語の論理式ではなく、その言語についての言明であり、メタ言語（数学的記法に助けられた日本語）で述べられる。したがって、その証明は形式体系の内部での演繹ではなく、形式体系を対象とする通常の数学的推論である。そのため、それはメタ理論的な証明、あるいは外的な証明と呼ばれる。

しかし、確かめた例をいくら集めても、無限個の対象についての主張は証明されない。このことから、有限回の確認から、ある性質が無限個の場合に成り立つと結論することを許す原理が必要になる。その原理が帰納法である。まず、なじみの深い自然数について述べ、次に、それに依拠する論理式について述べる。同じ道具が、メタ理論の単元で、演繹体系の健全性と完全性を証明することになる。