ColloquiumNO.230
|
皆さん、ニュートン線ってご存知ですか。
この問題以外でもニュ−トン線という問題はありますけど。
では、問題です。
中心が Ｏ の円に外接する四角形ＡＢＣＤの対角線ＡＣの中点をＮ，対角線ＢＤの中点をＭとすると、
３点Ｍ、Ｏ，Ｎは図のように一直線上にあることを示してください。
なお、この3点Ｍ、Ｏ、Ｎを通る直線をニュートン線という。
ヒント：補助線を使って適当な三角形を作り、その面積を比べてみてください。
出展：パズルでひらめく補助線の幾何学 （講談社：中村義作著）
注：この記事に関する投稿の掲載は、２００８年５月19日以降とします。
問題１
問題２
問題３
問題４
なお、問題２は log(1+ｘ)、問題３は sin ｘ、問題４は cos ｘ になります。
§１．対象式と関係式
以下§3までは、「概要」でWell-Difined性の説明を十分に行ったと考え、特に詳しい説明は設けない。
つけたとしても、コメント程度である。
１．記号，記号列
数学的理論Ｔで用いる記号は、次の三種類である。
１゜論理記号： τ，ou，〜．
２゜文字 ： これは原則として任意である．
３゜特殊記号： これは個々の理論によって、随時導入される．
Ｔにおける記号列とは、Ｔの記号を一列に並べて書いたものである。
定義とは、記号列の省略記法である。
２．構成手続き
あらゆる特殊記号は、重みと呼ばれる整数を持つ。
ある記号列がτで始まるか、一つの文字である場合、それを第一種と呼ぶ。
そうでない場合、第二種と呼ぶ。
Ｔにおける構成手続きとは、次の条件の一つを満たす記号列の列Ａのことである。
a) Ａは一つの文字である。
b) 記号列の列の中に、Ａより前に、第二種の記号列Ｂがあり、Ａは〜Ｂである．
c) 記号列の列の中に、Ａより前に、第二種の記号列ＢとＣがあり、ＡはＢouＣである．
d) 記号列の列の中に、Ａより前に、第二種の記号列Ｂと文字xがあり、Ａはτx(Ｂ)である．
e) Ｔにおける重みｎの特殊記号sと、記号列の列の中にＡより前にあるｎ個の第一種記号列
Ａ1，Ａ2，･･･，Ａnがあり、Ａは、sＡ1Ａ2･･･Ａnである．
Ｔの構成手続き中に現れる、第一種記号列をＴの対象式，第二種記号列をＴの関係式と呼ぶ。
a)より、全ての文字を理論において採用でき、それは対象を表しうる。
b)より、Ａが関係式なら、〜Ａも関係式である。
c)より、ＡとＢが関係式なら、ＡouＢも関係式である。
d)より、Ａが関係式でxが文字なら、τx(Ａ)は対象式である。
e)より、Ａ1，Ａ2，･･･，Ａnが対象式で、sが重みｎの特殊記号なら、sＡ1Ａ2･･･Ａnは関係式である。
b)とc)を使うことにより、ＡとＢが関係式なら、〜ＡouＢも関係式となる。
以後、この関係式を表す省略記法として、
Ａ⇒Ｂ
を採用する。Ａ⇒Ｂの意味については、後述する。
記号列Ｒに含まれる文字xを、全て同時に記号列Ｔに置き換えて得られる記号列の省略記法を、以後、
(Ｔ|x)Ｒ
で定義する。
§２．公理
「概要」で述べたようにここでの目的は、理論の公理を与えた後では、
それらに対して適用する機械的な計算規則（恒真関係を返す組み込み関数）を与えることである。
以下はその公理と計算規則の導入である（仕様定義といえる）。計算規則のことは、シェーマと呼ぶ。
１．公理
１゜理論Ｔの最初に現れる、一つ以上の関係式を、Ｔの明示公理と呼ぶ。
明示公理に現れる文字を、Ｔにおける定数という．
２゜Ｔのシェーマとは、次のような特性を持つ．
a) シェーマの一つＳを適用して得られる結果は、Ｔの関係式である．
b) ＴがＴの対象式、xを文字とする。ＲがシェーマＳの適用によって得られるＴの関係式ならば、
(Ｔ|x)ＲもＳの適用により得られる。
Ｔのシェーマによって得られる全ての関係式を、Ｔの非明示公理と呼ぶ。
２．証明
理論の公理とシェーマが与えられれば、シェーマを公理に次々と適用することで、
さらには三段論法の適用により証明が実行され、定理が得られる（形式論理の出力仕様）。
それが証明である。ただし実際には、証明に必要な関係式や対象式を、
証明の前に構成しておくのが普通だ。そこで次のようになる。
理論Ｔにおける証明の全文とは、次のものからなる。
1゜必要な関係式や対象式に関する補助的な構成手続き．
2゜証明．すなわち、Ｒを関係式として、次のいずれかの条件を満たす記号列があること．
a) ＲはＴの明示公理．
b) ＲはＴのシェーマから得られる．
c) Ｒより前に、関係式ＳとＳ⇒Ｒがある．
理論Ｔにおける定理とは、Ｔの証明の中に現れる関係式のことである。
証明と定理の導入により、「定理を証明する」という行為に関する、
形式的で一般的な規則を与えることが可能になる。以下では、それらを推論法則と呼び、
Ｃnで番号付けして示す（Tipsまたはパターン）。
本章の目的は、この推論法則を、必要最小限の範囲で得ることである。
なお推論法則にも、いわゆる［証明］を付けるが、
この［証明］は、上で述べたような通常の数学的証明ではないことを注意する。
それは、具体的に書かれた有限個の記号からなる記号列の列から得られる推論結果を、総括して書いた、
省略記述と考えるのが正しい。
この［証明］は原則として、総括することにより、途中の経過を省略して書いたものとみなすことができる。
従って、全ての記号を省略しないで書き並べれば自明と考えられる。
それがこれらの［証明］の根拠である。その意味で、太字記号で［証明］と記して、
通常の数学的［証明］とは区別する。
Ｃ1（三段論法）
ＡとＡ⇒Ｂを理論Ｔの定理とする。ＢはＴの定理。
［証明］
ＡとＡ⇒ＢがＴの定理であれば、2゜a)，b)，c)のどれかを満たす証明Ｐ1とＰ2が存在し、
Ｐ1はＡを、Ｐ2はＡ⇒Ｂを含む。従って、
Ｐ1，Ｐ2，Ｂ
をつくれば、これは2゜c) を満たす証明になる。よって、ＢはＴの定理。［証明終］
３．理論における代入
一つの文字は対象を表すのだった。
従って理論全体において、そこで使用される文字xを全て同時に対象式Ｔで置き換えても、
理論の意味は変わらない。ただし、文字xが定数である場合とそうでない場合とでは、少し差がある。
「概要」でも述べたように、この項と次項とは、実用プログラムのレベルで言えば、
混成言語プログラムの方法と、Sub Routineの本質について述べたものに過ぎない。
Ｔを一つの理論とする。Ａ1，Ａ2，･･･，Ａnをその明示公理全体、
xを文字、ＴをＴの対象式とする。記号およびシェーマはＴと同じで、明示公理が、
(Ｔ|x)Ａ1，(Ｔ|x)Ａ2，･･･，(Ｔ|x)Ａnである理論を(Ｔ|x)Ｔで表す。
Ｃ2
Ａを理論Ｔの定理、ＴをＴの対象式、xを文字とする。(Ｔ|x)Ａは(Ｔ|x)Ｔの定理。
［証明］
(1) ＡがＴの明示公理であれば、(Ｔ|x)Ａは(Ｔ|x)Ｔの明示公理で定理。
(2) ＡがＴのシェーマによって得られる定理であれば、(Ｔ|x)Ａは、同じＴのシェーマによって得られる、
(Ｔ|x)Ｔの定理。
(3) ＴにおいてＡより前に関係式ＢとＢ⇒Ａがあるなら、(Ｔ|x)Ｔおいて、
(Ｔ|x)Ｂと(Ｔ|x)(Ｂ⇒Ａ)、すなわち、(Ｔ|x)Ｂ⇒(Ｔ|x)Ａをつくれる。従って、
(Ｔ|x)Ａは(Ｔ|x)Ｔの定理。［証明終］
Ｃ3
Ａを理論Ｔの定理、ＴをＴの対象式、xをＴの定数でない文字とする。(Ｔ|x)ＡはＴの定理。
［証明］
Ｃ2の［証明］(2)と(3)は、Ｔと(Ｔ|x)Ｔの違いに関わらない。従って(1)のみ考慮すれば良い。
その場合、xはＴの定数でない文字なので、(Ｔ|x)ＡはＡに一致し、Ｔの定理になる。［証明終］
４．理論の比較
理論Ｔのすべての記号が理論Ｔ'の記号であり、Ｔのすべての明示公理がＴ'の定理であり、
ＴのすべてのシェーマがＴ'のシェーマであるとき、Ｔ'はＴより強いと言われる。
実用プログラムの世界では、このような概念はあまり使われない。しかし実用言語の言語開発の側面では、
これと良く似た概念がある。それが低級言語，高級言語である。
Macro AssemblerはAssemblerよりも高級で（強く）、
CはMacro Assemblerよりももっと高級（もっと強い）といった分類である。
Ｃ4
理論Ｔ'がＴより強ければ、Ｔの全ての定理は、Ｔ'の定理である。
［証明］
(1) ＡがＴの明示公理なら、それはＴ'の定理である。
(2) ＡがＴのシェーマから得られる定理なら、Ｔ'の同じシェーマからＡが得られ、それはＴ'の定理である。
(3) Ｔにおいて、Ａより前に関係式ＢとＢ⇒Ａがあるなら、Ｔ'においても関係式ＢとＢ⇒Ａをつくれる。
従って、ＢをＴ'の定理にできる。［証明終］
二つの理論Ｔ'とＴは、おのおのが他方より強いとき、同値であるという。
このとき、Ｔの定理はＴ'の定理であり、Ｔ'の定理はＴの定理である。
実用Applicationに限れば、VBとVCは今やほぼ同値と言える。
したがって一方でやれる事は、もう一方でもほぼ必ずやれる。
Ｃ5
Ｔを理論、Ａ1，Ａ2，･･･，Ａnをその明示公理全体、a1，a2，･･･，akをその定数全体、
Ｔ1，Ｔ2，･･･，ＴkをＴの対象式とする。
(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ａi，i＝1〜ｎが、理論Ｔ'の定理であり、
Ｔのすべての記号はＴ'の記号であり、ＴのすべてのシェーマはＴ'のシェーマとする。
ＡがＴの定理なら、(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)ＡはＴ'の定理。
［証明］
明示公理(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ａiを持つ理論を、(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ｔとする。
さらに、
(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ｔは、Ｔと同じ記号とシェーマを持つ。
Ｔ'はＴと同じ記号とシェーマを持つから、それは(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ｔの記号とシェーマであり、
しかもＴの明示公理Ａiから得られる(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ａiは、理論Ｔ'の定理である。
従って、Ｔ'は(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)Ｔより強い。
よってＣ4より、Ｔの定理(Ｔ1|a1)(Ｔ2|a2)･･･(Ｔk|ak)ＡはＴ'の定理。［証明終］
§３．論理的な理論
この節以降では、それぞれの個別理論に固有のシェーマ（計算規則または組み込み関数）を具体的に与え、
アルゴリズムに当たるその運用を展開して行く事になる。
しかしアルゴリズムを「書く」ためには、何らかの言語を一つ選択し、
その言語の語彙を用いてアルゴリズムを書く必要がある。
プログラミングの世界では、その行為をコーディングと言う。
もし、選択できる言語が存在しないなら、言語自体を［定義］しながらコーディングを進めるしかない。
§1.と2.で行った作業は、言語の語彙を［定義］した事にあたる。明らかに語彙も、形式的なものだった。
ただしここで使っている［定義］の意味は、§1.1で述べた「記号列の省略記法」という意味での定義よりも、
明らかに広くて非形式的なものである。例えば語彙の導入において、
結果として現れた語彙自体は形式的なものだったが、その導入に使われた言葉は、
非形式的な説明である。そのようなものを、ここでは、［定義］と書くことにした。
これは、あるものを説明する事とほぼ同義である。
いずれにしろここでの状況は、言語を作りつつ進む場合に当たる。
数学的記述の形式化は始めたばかりで、あらかじめ用意された、形式論理記述用言語があるわけではない。
以後の作業を進めるにあたっても、広い意味での形式的プログラミング言語の［定義］は、
引き続き必要になるが、形式的定義を行った際には、原則的にはいつでも、
Well-difined性の「証明」が必要である。
形式的定義は、既存の理論と矛盾しないことをチェックすべきだ。
形式的記号の導入は、意味に縛られずに自由に行えるからである。
しかし現段階において、形式化された既存の理論というのものは存在しない。
製作中だからだ。あるのは、ただ現実に行える事、行っている事の意味や判断だけである。
例えば、Ｒ(x)を文字xを含む関係式だとする。可能な全てのxに対してＲ(x)をテストし、
Ｒ(x)が全て真だった時には、その意味として、
(∀x)Ｒ
を用いるが、同時に、
〜(∃x)(〜Ｒ)
という判断を下す。そして、任意のxに対してＲ(x)が成り立つ事や、
任意のxに対して〜Ｒ(x)が成り立たない事などを確認していなくても、
(∀x)Ｒ ⇔ 〜(∃x)(〜Ｒ)
という論理的判断を恒真関係として受け入れ、これを形式的なアルゴリズムの一つとする。
同様に、Ａ(x)を満たす全てのxに対してＢ(x)をテストし、Ｂ(x)が全て真ならば、その意味として、
Ａ(x) ⇒ Ｂ(x)
を用いるが、任意のxでＡ(x)が必ず成り立つとは限らない。それでも、
Ａ ⇒ Ｂ
という論理的判断を受け入れ、恒真関係として採用する。
何を言いたいかというと、論理アルゴリズムを書くための言語のWell-difined性の「証明」は、
現段階では現実に行える事、行っている事の意味や判断に基づくしかないという事である。
ところで、このWell-difined性の「証明」は明らかに、§1.2でいちおう形式的に［定義］した
証明］よりもさらに形式化されていない説明になるのは明らかだろう。
そのような意味で、以後の各節，各項には、必要に応じてWell-difined性の説明を設ける。
上の例でもう一つ言いたいのは、論理は現実に行っている事に対する、一種の省略記述だという事実である。
例えば、(∀x)Ｒが成り立つと仮定したならば、全てのxに対してＲ(x)をテストせずに、
〜(∃x)(〜Ｒ)は成り立つと判断する。これによって全てテストを省略できるので、
明らかに推論の効率は上がる。これが論理の実際的な価値である（省力化）。
だからこそ恒真関係のみを受け入れ、証明を要しない遍手続きを探す。
１．公理
以下のS1〜S4のシェーマが非明示公理を与える全ての理論Ｔを、論理的な理論と呼ぶ。
Ａ，Ｂ，ＣはＴの関係式とする。
S1 (ＡouＡ)⇒Ａは、Ｔの公理．
S2 Ａ⇒(ＡouＢ)は、Ｔの公理．
S3 (ＡouＢ)⇒(ＢouＡ)は、Ｔの公理．
S4 (Ａ⇒Ｂ)⇒((ＣouＡ)⇒(ＣouＢ))は、Ｔの公理．
以下Ｔは、ある一つの論理的な理論を表すものとし、しばしば「Ｔの」という言い回しを省略する。
また、文脈上で自明ならば、関係式，対象式などの説明も省略する。
§2.2より、理論Ｔにおける証明の全文とは、次のようなものだった。
1゜必要な関係式や対象式に関する補助的な構成手続き．
2゜証明．すなわち、Ｒを関係式として、次のいずれかの条件を満たす記号列があること．
a) ＲはＴの明示公理．
b) ＲはＴのシェーマから得られる．
c) Ｒより前に、関係式ＳとＳ⇒Ｒがある．
ここまでで明らかなように、論理的な理論は明示公理を持っても持たなくても良い。
状況を簡単化するために、明示公理を持たない理論で考える。つまり上記a)の適用は、とりあえずない。
そうすると最初にあるのは、シェーマのみである。シェーマは公理を導く。
例えば、「S1 (ＡouＡ)⇒Ａは、Ｔの公理」は、(ＡouＡ)⇒ＡがＴの非明示公理である事を言っている。
よって上記b)より、(ＡouＡ)⇒Ａは定理である。つまりシェーマは実質的に、理論Ｔの明示公理であり、
明らかな恒真関係である。
このような事情から、以後の説明では、S1〜S4を一種の明示公理とみなす。
つうじょうの手順では、理論Ｔの明示公理にシェーマを適用し、いくつかの補助的定理を導いた後に、
c)三段論法が登場し、関係式Ｓ⇒Ｒから、前提Ｓと結論Ｒを切り離し、結論Ｒを一人立ちさせる。
次の例にはほとんど利用価値がないが、説明のために導入する。
Ａ ⇒ ＡouＢ，(Ａ ⇒ ＡouＢ) ⇒ (ＣouＡ ⇒ ＣouＡouＢ)，ＣouＡ ⇒ ＣouＡouＢ
(1) (2) (3)
(1)：Ａ ⇒ ＡouＢ は、S2より「明示公理」とみなせる。それにシェーマS4を適用し、
「定理」(2)を得る。定理(1)，(2)に三段論法c)を適用し、
(3)：ＣouＡ ⇒ ＣouＡouＢ が「定理」である事がわかり、
以後の同様なタイプの推論では、「定理」ＣouＡ ⇒ ＣouＡouＢ を、
自由にその前提として用いて良い事になる。典型的な理論は、このような推論の連鎖からなる。
この例からもわかるように、推論に現れる関係式は常に恒真関係である
。何故なら推論は、形式的普遍手続きでなければならないからだ。
特にふつうに言うところの理論の公理は、恒真関係である事を強制された関係式であると言える。
よって、このような理論構成で三段論法に現れる関係式は、つねに全て恒真関係である。
恒真関係とは、次のようなものだ。文字（対象）xを含んだ関係式Ａ(x)の外延集合をaで表す。
xで表される対象全体の外延集合をＸとする。Ｘには全ての物が含まれると、ここでは素朴に考える。
Ａ(x)が恒真関係であるとは、a＝Ｘである事だ。何故ならそうでないとすれば、
Ａは特定のxでしか成り立たない事になり、任意のケースでは成り立たないからだ。
この事をここでは、普遍的に真という言葉で表す。特にＡが文字xを含んでいないならば、
Ａが任意の対象xに無関係という意味で（成り立つなら）、恒真関係とみなせる。
次に三段論法は、Ｃ1によれば、
ＡとＡ⇒Ｂを理論Ｔの定理とする．ＢはＴの定理．
というものだった。
ここで少なくとも、Ａ(x)とＡ(x)⇒Ｂ(x)は恒真関係でなければならない。
Ａ(x)については、現実との比較テストが行われて普遍的に真である事が確認されたか、
公理としてそうである事が強制されたか、それともS1〜S4にように、
自明な恒真関係とみなせるかのどれかである。
しかしＡ(x)⇒Ｂ(x)については、たとえＡ(x)とＢ(x)が普遍的に真であっても、
どういう場合にＡ(x)⇒Ｂ(x)を恒真関係と認めるべきかはわかっていない。
つまり三段論法を認めるためには、Ａ⇒ＢをWell-difinedする事が必要だ。
要するにここでは、§1.2で 〜ＡouＢ の事だと定義された、⇒ のWell-difined性を説明したいのである。
Ａ(x)とＢ(x)の外延集合をa，bとしたとき、Ａ(x)⇒Ｂ(x)が任意のxで成り立つためには、
a⊂bが必要なのは明らかである。たとえxが現実にはＡ(x)を満たさないとしても、
そう仮定した場合に（x∈aと仮定した場合に）つねに、Ａ(x)⇒Ｂ(x)が成り立つために、
a⊂bは必要である。aやbの補集合をここでは、a'やb'で表す。そうすると、
a'∪b＝Ｘ ⇔ a⊂b
であるのがわかる。a'∪b＝Ｘとは、〜ＡouＢが普遍的に真という事である。
逆に、〜ＡouＢが普遍的に真であれば、上記関係が成り立つ事も言える。この事実をもって、
Ａ⇒Ｂ を、〜ＡouＢ で定義する．
ことになる。
さらに、公理の完全性，無矛盾性，独立性の問題があるが、ここでは問わない。
ここで言う公理とは、実質的に論理的理論の明示公理とみなせるS1〜S4の事だが、
つうじょうの推論のタイプ（Tipsおよびパターン）は、S1〜S4を過不足なく用いる事によって、
いずれも導けるのだとだけ、ここでは言うに止める。
最後に、普遍的に真である事を以後、「命題理論の意味で定理」と言う事にする。
純粋な命題理論は、公理S1〜S4しか持っておらず、しかもこれらはシェーマであるから、§1.1.2゜より、
a) シェーマの一つＳを適用して得られる結果は、Ｔの関係式である．
b) ＴがＴの対象式、xを文字とする。ＲがシェーマＳの適用によって得られるＴの関係式ならば、
(Ｔ|x)ＲもＳの適用により得られる。
という特性を持つものになる。従ってS1〜S4のみを明示公理とし、S1〜S4をシェーマとする命題理論の
定理は全て、この特性を持つ。命題理論の定理は常に普遍的に真なのだ。
その中には、たまたま文字xを含まないが故に普遍的に真になる関係式Ａもあり得るが、
最初からＡが文字xを含めない事と、これは本質的に違う。この違いは、
後述する「限定作用素を持つ理論」において、重要な違いをもたらす。
２．基本的結論
ここでは三段論法によって導かれる、典型的な推論パターンを［証明］し、以後の議論への準備とする。
Ｃ6
Ａ⇒Ｂ，Ｂ⇒Ｃが定理なら、Ａ⇒Ｃは定理。
［証明］
S4でＣを〜Ｃに置き換えたものを考えれば、
(Ａ⇒Ｂ)⇒((〜ＣouＡ)⇒(〜ＣouＢ))
となる。これは、
(Ａ⇒Ｂ)⇒((Ｃ⇒Ａ)⇒(Ｃ⇒Ｂ))
と同じ。従って、Ｃ⇒ＡとＡ⇒Ｂが定理なら、Ｃ⇒Ｂが定理になる。これは、Ａ⇒Ｂ，Ｂ⇒Ｃが定理なら、
Ａ⇒Ｃが定理になると同じこと。［証明終］
Ｃ7
Ｂ⇒(ＡouＢ)は定理。
［証明］
S2より、
Ｂ⇒(ＢouＡ)
であり、S3より、
(ＢouＡ)⇒(ＡouＢ)
である。従って、Ｃ6より、
Ｂ⇒(ＡouＢ)
は定理。［証明終］
Ｃ8
Ａ⇒Ａは定理。
［証明］
S2より、
Ａ⇒(ＡouＡ)
であり、S1より、
(ＡouＡ)⇒Ａ
である。従って、Ｃ6より、Ａ⇒Ａ は定理。［証明終］
Ｃ9
Ｂが定理なら、Ａ⇒Ｂは定理。
［証明］
S7より、
Ｂ⇒(〜ＡouＢ)
である。これは、
Ｂ⇒(Ａ⇒Ｂ)
と同じ。Ｂが定理だから、Ａ⇒Ｂは定理。［証明終］
Ｃ9は一見利用価値がないように見えるが、意味はすぐわかる。
Ｂが正しいなら、どんな前提を立てても（前提とは無関係に）Ｂは正しいという当然の結果である。
しかも利用価値もある。
（まだ［証明］していないが）対偶をとると、〜Ｂ⇒〜Ａとなる。
ここでＡは任意であったから、〜Ａも任意である。
Ｂは真だったから、〜Ｂは偽。従って、間違った前提からはどんな結論でも出せる事になる。
前提とは仮定だから、真であるＢに対して〜Ｂを仮定した、
追加仮定を行った系では、Ｂと〜Ｂは両方とも真である。このような理論は矛盾していると言われ、
上で述べた事情から任意の関係式が真となる。この状況を上手く利用したのが、
後述する帰謬法（背理法）である。
間違った前提からはどんな結論でも出せる、の対偶を再び取ると、
特定の結論しか出せない時には（結論が前提に束縛される時には）前提は間違っていない
、という意味になる。この事は、理論の無矛盾性の証明に結びつきそうだが、
このノートの方針は数学基礎論と関わらないなので、これ以上深追いしない（自分には出来ないし）。
もっと現実的な見方も出来る。特定の結論しか出せない時には前提は間違っていない、
は論理的な理論の反証可能性を保証するように見える。Ｃ9はきっと、まともな理論が持たざる得ない、
まともさから来るお釣りのような性質だと思う。
Ｃ10
Ａou(〜Ａ)は定理。
［証明］
Ｃ8より、
Ａ⇒Ａ
は定理。これは
〜ＡouＡ
と同じ。S3より、
(〜ＡouＡ)⇒(Ａou(〜Ａ))
である。従って、
Ａou(〜Ａ)
は定理。［証明終］
Ｃ11
Ａ⇒(〜〜Ａ)は定理。
［証明］
Ｃ10より、〜Ａou(〜〜Ａ)は定理。これは、
Ａ⇒(〜〜Ａ)
と同じ。［証明終］
Ｃ12
(Ａ⇒Ｂ)⇒((〜Ｂ)⇒(〜Ａ))は定理。
［証明］
Ｃ11とS4とS3から、
Ｂ⇒(〜〜Ｂ)
(Ｂ⇒(〜〜Ｂ))⇒((〜ＡouＢ)⇒(〜Ａou(〜〜Ｂ)))
(〜Ａou(〜〜Ｂ))⇒(〜〜Ｂou(〜Ａ))
である。従って、Ｃ6より、
(〜ＡouＢ)⇒(〜〜Ｂou(〜Ａ))
が定理になる。これは、
(Ａ⇒Ｂ)⇒((〜Ｂ)⇒(〜Ａ))
と同じ。［証明終］
Ｃ13
Ａ⇒Ｂが定理なら、(Ｂ⇒Ｃ)⇒(Ａ⇒Ｃ)は定理。
［証明］
Ｃ12，S4，S3より、
(Ａ⇒Ｂ)⇒((〜Ｂ)⇒(〜Ａ))
((〜Ｂ)⇒(〜Ａ))⇒((Ｃou(〜Ｂ))⇒(Ｃou(〜Ａ)))
(〜ＢouＣ)⇒(Ｃou(〜Ｂ)
(Ｃou(〜Ａ)⇒(〜ＡouＣ)
である。Ａ⇒Ｂが定理だから、
(〜ＢouＣ)⇒(Ｃou(〜Ｂ)
((Ｃou(〜Ｂ))⇒(Ｃou(〜Ａ)))
(Ｃou(〜Ａ)⇒(〜ＡouＣ)
が得られる。従って、Ｃ6より、
(〜ＢouＣ)⇒(〜ＡouＣ)
が言える。これは、
(Ｂ⇒Ｃ)⇒(Ａ⇒Ｃ)
と同じもの。［証明終］
以後、Ｃ6（とＣ1）は、引用することなく使用する。
３．証明の方法
2.で示された全ての推論法則を用いたとしても、実際には非常に遠回りで、
何度も同じ［証明］パターンを繰り返す必要に迫られる。
以下はさらなるショートカットの導入である。これらがないと実際上、
証明は不可能なくらい手がかかるものになる。以下に述べる「証明の方法」
は標準的なものである。いずれも最初の「補助仮定の方法」を基礎にしている。
3.1 補助仮定の方法
Ｃ14（演繹法則）
Ａを理論Ｔの関係式、Ｔの公理にＡを追加して得られる理論を、
Ｔ'とする。ＢがＴ'の定理なら、Ａ⇒ＢはＴの定理。
［証明］
まずＢがＴ'の公理なら、それはＴの明示公理であるか、Ａそのものか、
シェーマの適用によって得られたものである。Ｔの明示公理ならばそれはＴの定理だから、
Ｃ9よりＡ⇒Ｂが成り立つ。ＢがＡなら、Ｃ8よりＴでＡ⇒Ａが成り立つ。
Ｂがシェーマの適用によって得られたものならば、それは定理だから、
やはりＣ9よりＴでＡ⇒Ｂが成り立つ。残る場合は、ＢがＴ'における三段論法によって得られた場合である。
ＢがＴ'において、三段論法によって得られたとすれば、Ｔ'にＢを含む証明Ｐnがあり、
Ｐnの中で、Ｂより前に関係式ＳとＳ⇒Ｂが存在する。ＳとＳ⇒Ｂは、証明Ｐnの中に現れる関係式だから、
Ｔ'の定理である。従ってそれらは、Ｔの明示公理であるか、Ａであるか、
シェーマの適用によって得られたか、Ｔ'における三段論法で得られたものになる。
Ｔの明示公理，Ａ，シェーマの適用の場合はいずれも、ＳとＳ⇒ＢはＴの定理であり、
ＢもＴの定理になる。よって、Ａ⇒ＢはＴの定理。
そこで、ＳとＳ⇒ＢがＴ'における三段論法で得られたものとする。ただし証明Ｐnは、
ＳとＳ⇒Ｂの証明を含まないとする。そうすると、証明Ｐnより前に、
ＳとＳ⇒Ｂを含む証明Ｐn-1が存在しなければならない。帰納的に遡ることによって、
あるｍ≦ｎが存在し、証明Ｐ1，Ｐ2，･･･，Ｐmに含まれる全ての定理は、Ｔの明示公理であるか、
シェーマの適用によって得られたか、Ｔのにおける三段論法によって得られた定理であるか、
Ａということになる。Ａである場合を除いて、それらの定理は全てＴの定理である。
Ｐ1，Ｐ2，･･･，Ｐmの定理がＡでないときは、それはＴの定理であるから、
そこから三段論法の系列によって帰納的に得られたＢは、Ｔの定理であり、Ａ⇒Ｂが成り立つ。
そこでＰ1，Ｐ2，･･･，Ｐmの定理がＡである場合を考える。
例えばＡがＰ1に含まれ、ＳがＰ2に含まれ、Ｓ⇒Ｂ1がＰ3に含まれるとする。
ただし、1，2，3≦ｍである。このとき、Ａ⇒ＳとＡ⇒(Ｓ⇒Ｂ1)は明らかにＴの定理であり、
ここからＡ⇒Ｂ1がＴの定理として得られると仮定する。帰納的に逆をたどれば、
Ａ⇒ＳとＡ⇒(Ｓ⇒Ｂ)がＴの定理であれば、Ａ⇒ＢはＴの定理である。これを示す。
以上の結論として以下では、定理と言えばＴの定理になる。
Ｃ13より、
(Ａ⇒Ｓ)⇒((Ｓ⇒Ｂ)⇒(Ａ⇒Ｂ))
が成り立つ。Ａ⇒Ｓは定理であるから、
(Ｓ⇒Ｂ)⇒(Ａ⇒Ｂ)
は定理である。さらに、Ａ⇒(Ｓ⇒Ｂ)も定理なのだから、
Ａ⇒(Ａ⇒Ｂ)
が定理である。これは、
〜Ａou(Ａ⇒Ｂ)
と同じものである。従って、
(〜Ａou(Ａ⇒Ｂ))⇒((Ａ⇒Ｂ)ou(〜Ａ))
より、
(Ａ⇒Ｂ)ou(〜Ａ)
は定理。
次にS2より、
〜Ａ⇒(〜ＡouＢ)
は定理。これは、
〜Ａ⇒(Ａ⇒Ｂ)
と同じものである。これにS4を適用すれば、
(〜Ａ⇒(Ａ⇒Ｂ))⇒(((Ａ⇒Ｂ)ou(〜Ａ))⇒((Ａ⇒Ｂ)ou(Ａ⇒Ｂ)))
が得られる。従って、〜Ａ⇒(Ａ⇒Ｂ)が定理であるから、
((Ａ⇒Ｂ)ou(〜Ａ))⇒((Ａ⇒Ｂ)ou(Ａ⇒Ｂ))
も定理。また、(Ａ⇒Ｂ)ou(〜Ａ)も定理だから、
(Ａ⇒Ｂ)ou(Ａ⇒Ｂ)
が定理。最後にS1を適用すれば、
Ａ⇒Ｂ
が、Ｔの定理になる。［証明終］
3.2 帰謬法
理論Ｔにおいて、関係式Ａと〜Ａが同時に定理となる場合、Ｔは矛盾していると言われる。
Ｃ15
Ａを理論Ｔの関係式、Ｔの公理に〜Ａを追加して得られる理論を、Ｔ'とする。Ｔ'が矛盾すれば、
ＡはＴの定理。
［証明］
理論Ｔ'が矛盾すれば、Ｔ'の任意の関係式ＣはＴ'の定理であることを示す。
理論Ｔ'が矛盾するとは、〜ＢとＢが、同時にＴ'の定理となることである。従って、S2より、
〜Ｂ⇒(〜ＢouＣ)
が成り立つ。〜ＢはＴ'の定理だから、
〜ＢouＣ
がＴ'の定理で、これは、
Ｂ⇒Ｃ
と同じ。ここでＢもＴ'の定理だから、
Ｃ
がＴ'の定理になる。
従って、Ａを理論Ｔの関係式として、
Ｔの公理に〜Ａを追加して得られる理論Ｔ'が矛盾すれば、ＡはＴ'の定理である。
よって、Ｔにおいて、
〜Ａ⇒Ａ
が定理（補助仮定の方法）。これにS4を適用すれば、
(〜Ａ⇒Ａ)⇒((Ａou(〜Ａ))⇒(ＡouＡ))
が得られる。〜Ａ⇒ＡはＴの定理だから、
(Ａou(〜Ａ))⇒(ＡouＡ)
がＴの定理。Ｃ10より、Ａou(〜Ａ)はＴの定理で、
ＡouＡ
はＴの定理である。これにS1を適用すれば、
(ＡouＡ)⇒Ａ
なので、
Ａ
がＴの定理になる。［証明終］
帰謬法の応用として、次の2つの推論法則を示す。
Ｃ16
〜〜Ａ⇒Ａは定理。
［証明］
〜〜Ａを追加した理論Ｔ'とする（補助仮定の追加）。
さらに〜Ａを追加した理論をＴ"とする（帰謬法の仮定の追加）。
このときＴ"において、〜Ａと〜〜Ａは定理となるから矛盾。従ってＴ'でＡは定理で、
〜〜Ａ⇒Ａ
は、最初の理論の定理。［証明終］
17
((〜Ｂ)⇒(〜Ａ))⇒(Ａ⇒Ｂ)は定理。
［証明］
(〜Ｂ)⇒(〜Ａ)を追加した理論をＴ'，さらにＡを追加した理論をＴ"，
その上で〜Ｂを追加した理論をＴ'''とする。
Ｔ'''において、(〜Ｂ)⇒(〜Ａ)は定理だから、〜Ｂが定理なら〜Ａが定理になる。
ところがＡもＴ'''の定理なので、これは矛盾。従って、
Ｂ
はＴ"の定理で、
Ａ⇒Ｂ
はＴ'の定理になる。よって、
((〜Ｂ)⇒(〜Ａ))⇒(Ａ⇒Ｂ)
は、最初の理論の定理である。［証明終］
3.3 場合分けの方法
Ｃ18
Ａ，Ｂ，Ｃを理論Ｔの関係式とする。ＡouＢ，Ａ⇒Ｃ，Ｂ⇒ＣがＴの定理なら、ＣはＴの定理。
［証明］
S4，S3およびS1より、以下が得られる。
(Ｂ⇒Ｃ)⇒((ＡouＢ)⇒(ＡouＣ))
(ＡouＣ)⇒(ＣouＡ)
(Ａ⇒Ｃ)⇒((ＣouＡ)⇒(ＣouＣ))
(ＣouＣ)⇒Ｃ
ここで、Ａ⇒Ｃ，Ｂ⇒ＣがＴの定理だから、
(ＡouＢ)⇒(ＡouＣ)
(ＡouＣ)⇒(ＣouＡ)
(ＣouＡ)⇒(ＣouＣ)
(ＣouＣ)⇒Ｃ
は、いずれもＴの定理になる。ＡouＢもＴの定理だから、
ＡouＣ
(ＡouＣ)⇒(ＣouＡ)
(ＣouＡ)⇒(ＣouＣ)
(ＣouＣ)⇒Ｃ
が得られる。三段論法を繰り返し適用すれば、ＣはＴの定理。［証明終］
3.4 補助定数の方法
Ｃ19
xを文字、ＡおよびＢを理論Ｔの関係式、Ｔ'をある理論とし、以下の条件を満たすとする。
1゜xはＴの定数でなく、Ｂはxを含まない．
2゜(Ｔ|x)ＡがＴの定理となる、Ｔの対象式Ｔがある．
3゜理論Ｔ'は、Ｔの公理にＡを追加して得られる．
このとき、ＢがＴ'の定理なら、ＢはＴの定理。
［証明］
補助仮定の方法より、Ａ⇒ＢはＴの定理。このときxはＴの定数でないので、
Ｃ3より、(Ｔ|x)(Ａ⇒Ｂ)もＴの定理になる。Ｂは文字を含まないなので、
これは(Ｔ|x)Ａ⇒Ｂと同じで、しかも、(Ｔ|x)ＡがＴの定理となる、Ｔの対象式Ｔがある。
従って、ＢはＴの定理である。
［証明終］
この段階まで来ると、推論はかなり自由に行えるようになる。まず良く使われる関係式 、
・ Ａ⇒〜〜Ａ と 〜〜Ａ⇒Ａ（二重否定律，排中律）
・ (Ａ⇒Ｂ)⇒(〜Ｂ⇒〜Ａ) と (〜Ｂ⇒〜Ａ)⇒(Ａ⇒Ｂ)（対偶）
は［証明］され、推論のアウトラインを定める、
・ 補助仮定の方法
・ 帰謬法（背理法）
が導入された。また、
・ 補助定数の方法
により、ある性質を持つ対象を適宜導入する事も可能だ
（補助仮定の方法と組み合わせると、これはSub RoutineのLocal変数になる）。最後に、
・ 場合分けの方法
は、基本的な論理演算ＡouＢを、個々の要素関係式Ａ，Ｂに分解して考えても良い事を許す。
これに二重否定律を加えると、ＡやＢが否定〜を伴っていても、同様に分解できる事がわかる。
任意の関係式は、〜とouで連結された関係式で出来ているから、
それらを要素関係式に分解し、他の推論法則も利用して、
目的に沿って組み立て直す事が出来るようになる。特にS2からは、
Ａ，Ｂ ⇒ ＡouＢ という関係式は常に正しい。
次項では、もう一つの基本論理演算ＡetＢ（Ａ AND Ｂ）を定義する。
従って次項では、ＡetＢの定義の他に、
・ ＡetＢをＡ，Ｂに分解する方法、およびその逆
・ 分解のための、〜，ou，etに関する分配則
が必要になる。ＡetＢは意味から言って、〜とouから定義できるのは明らかだろう。
４．論理積
ＡetＢを、〜((〜Ａ)ou(〜Ｂ))で定義する。
Ｃ20
Ａ，Ｂを定理とする。ＡetＢは定理。
［証明］
〜(ＡetＢ)を仮定する。これは〜〜((〜Ａ)ou(〜Ｂ))のことで、Ｃ16より、
〜〜((〜Ａ)ou(〜Ｂ))⇒((〜Ａ)ou(〜Ｂ))
が成り立つ。従って、
(〜Ａ)ou(〜Ｂ)
は定理だが、これは、
Ａ⇒(〜Ｂ)
と同じ。Ａが定理なので、〜Ｂが定理。
ところがＢも定理だから、これは矛盾。
よって、Ａ，Ｂを定理なら、ＡetＢは定理でなければならない。［証明終］
Ｃ21
(ＡetＢ)⇒Ａと(ＡetＢ)⇒Ｂは定理。
［証明］
〜Ａ⇒((〜Ａ)ou(〜Ｂ))
は定理。Ｃ12より、
(〜Ａ⇒((〜Ａ)ou(〜Ｂ)))⇒(〜((〜Ａ)ou(〜Ｂ))⇒(〜〜Ａ))
も定理で、Ｃ16より、
〜((〜Ａ)ou(〜Ｂ))⇒(〜〜Ａ)，〜〜Ａ⇒Ａ
が定理になるが、これは、
ＡetＢ⇒(〜〜Ａ)，〜〜Ａ⇒Ａ
と同じ。従って、
ＡetＢ⇒Ａ
が定理になる。同様に、
〜Ｂ⇒((〜Ｂ)ou(〜Ａ))，((〜Ｂ)ou(〜Ａ))⇒((〜Ａ)ou(〜Ｂ))
〜Ｂ⇒((〜Ａ)ou(〜Ｂ))，(〜Ｂ⇒((〜Ａ)ou(〜Ｂ)))⇒(〜((〜Ａ)ou(〜Ｂ)))⇒(〜〜Ｂ))
〜((〜Ａ)ou(〜Ｂ))⇒(〜〜Ｂ)，〜〜Ｂ⇒Ｂ
〜((〜Ａ)ou(〜Ｂ))⇒Ｂ
が得られるが、最後の式は、
ＡetＢ⇒Ｂ
と同じである。ただし、上の は三段論法の仮定を、下の は三段論法の結論を表す。
［証明終］
５．同値
Ａ⇔Ｂを、(Ａ⇒Ｂ)et(Ｂ⇒Ａ)で定義する。
Ｃ22
Ａ⇔Ｂが定理なら、Ｂ⇔Ａは定理。Ａ⇔ＢとＢ⇔Ｃが定理なら、Ａ⇔Ｃは定理。
［証明］
Ａ⇔Ｂは、(Ａ⇒Ｂ)et(Ｂ⇒Ａ)と同じである。従ってＣ21より、
((Ａ⇒Ｂ)et(Ｂ⇒Ａ))⇒(Ｂ⇒Ａ)
((Ａ⇒Ｂ)et(Ｂ⇒Ａ))⇒(Ａ⇒Ｂ)
は定理。Ａ⇔Ｂ、すなわち(Ａ⇒Ｂ)et(Ｂ⇒Ａ)が定理だから、
Ｂ⇒Ａ，Ａ⇒Ｂ
は定理。よってＣ20より、
(Ｂ⇒Ａ)et(Ａ⇒Ｂ)
は定理。これは、
Ｂ⇔Ａ
と同じ。
次にＡ⇔ＢとＢ⇔Ｃが定理なら、Ｃ21より、
Ａ⇒Ｂ，Ｂ⇒Ｃ
は定理なので、
Ａ⇒Ｃ
は定理。同様に、
Ｃ⇒Ｂ，Ｂ⇒Ａ
が定理で、
Ｃ⇒Ａ
も定理。Ｃ20より、
(Ａ⇒Ｃ)et(Ｃ⇒Ａ)
が定理になる。これは、
Ａ⇔Ｃ
と同じ。［証明終］
以下のＣ23〜Ｃ25は、［証明］を省略している。これらについては、
今まで得られた結果を「証明の方法」も含めて全面的に活用すれば、いずれも導ける。
Ｃ23
Ａ⇔Ｂが定理とする。以下は定理。
(〜Ａ)⇔(〜Ｂ)
(Ａ⇒Ｃ)⇔(Ｂ⇒Ｃ)，(Ｃ⇒Ａ)⇔(Ｃ⇒Ｂ)
(ＡetＣ)⇔(ＢetＣ)，(ＡouＣ)⇔(ＢouＣ)
［証明］
Ｃ1〜Ｃ22を使用すれば、示せる。詳細は、Appendixに譲る。［証明終］
Ｃ24
次は定理。
〜〜Ａ⇔Ａ，(Ａ⇒Ｂ)⇔((〜Ｂ)⇒(〜Ａ))
ＡetＡ⇔Ａ，ＡetＢ⇔ＢetＡ
(Ａet(ＢetＣ))⇔((ＡetＢ)etＣ)
(ＡouＢ)⇔〜((〜Ａ)et(〜Ｂ))
(ＡouＡ)⇔Ａ，(ＡouＢ)⇔(ＢouＡ)
(Ａou(ＢouＣ))⇔((ＡouＢ)ouＣ)
(Ａet(ＢouＣ))⇔((ＡetＢ)ou(ＡetＣ))
(Ａou(ＢetＣ))⇔((ＡouＢ)et(ＡouＣ))
(Ａet(〜Ｂ))⇔(〜(Ａ⇒Ｂ))，(ＡouＢ)⇔((〜Ａ)⇒Ｂ)
［証明］
Ｃ1〜Ｃ23を使用すれば、示せる。詳細は、Appendixに譲る。［証明終］
Ｃ25
Ａを定理とすれば、以下は定理。
(ＡetＢ)⇔Ｂ
〜Ａを定理とすれば、以下は定理。
(ＡouＢ)⇔Ｂ
［証明］
Ｃ1〜Ｃ24を使用すれば、示せる。詳細は、Appendixに譲る。
［証明終］
Ａ⇒Ａは定理である。従ってＣ20より、
(Ａ⇒Ａ)et(Ａ⇒Ａ)は定理。これは、Ａ⇔Ａと同じである。すなわち、Ａ⇔Ａは定理である。
ここで、記号列Ａが定義により、記号列Ｂで表せるとする。
定義とは省略記法のことであるから、Ａ⇔Ｂは定理Ａ⇔Ａを、省略記法を用いて表したものとみなせる。
このことからＡ⇔Ｂも、便宜上定理とみなす。この方針に従えば、例えば、
(〜ＡouＢ)⇔(Ａ⇒Ｂ)
(Ｔ|x)(〜Ａ)⇔(〜(Ｔ|x)Ａ)
などは定理である。そこでＣ24とetの定義により、
〜(ＡouＢ)⇔((〜Ａ)et(〜Ｂ))
(ＡetＢ)⇔((〜Ａ)ou(〜Ｂ))
は定理であるから、ouとetは否定によって互いに移る事ができる。
すなわちＡetＢについての関係式を得たあとに、Ａ，Ｂを〜Ａ，〜Ｂに置き換えて対偶をとれば、
対応するＡouＢについての関係式が得られる。一方についての関係式があるなら、
他方についても同様であり、両者の全体は全く同等である。
