証明.

定義から明らかである。

証明.

こちらも定義から明らかである。

証明.

⊨󱁀1Σ1 から ⊨󱁀nΣn が全て成り立っていると仮定する。 証明は、 ⊢K[Σ1,⋯,Σn]A の導出に関する帰納法で行う。 なお、 記号を簡単にするため、 以降 󰔃K:=K[Σ1,⋯,Σn] と 󰔃󱁀:=󱁀1∩⋯∩󱁀n と書く。

⊢󰔃KA が公理であるとき。 このときは、 さらに 4 つの場合に分けられる。 A が命題論理的恒真であるときは、 命題 2.3 によって ⊨󰔃󱁀A が成り立つ。 A が K に属するときは、 命題 2.5 から ⊨󰔃󱁀A が成り立つ。 A が Dual⬦ に属するときも、 命題 2.6 から ⊨󰔃󱁀A が成り立つ。 最後に A が 󰔃K で追加された公理 Σi(1≤i≤n) であったときは、 最初の仮定から ⊨󱁀iA が成り立っているので、 󱁀i⊇󰔃󱁀 と命題 9.2 によって ⊨󰔃󱁀A も成り立つ。

⊢󰔃KA が推論規則 MP の帰結であるとき。 すなわち、 ⊢󰔃KX と ⊢󰔃KX⇀A からこれが導かれているとき。 帰納法の仮定から ⊨󰔃󱁀X と ⊨󰔃󱁀X⇀A が成り立つが、 命題 2.4 を使うことでこれらから ⊨󰔃󱁀A が導かれる。

⊢󰔃KA が推論規則 RN の帰結であるとき。 すなわち、 A≡◻X と書けて ⊢󰔃KX からこれが導かれているとき。 帰納法の仮定から ⊨󰔃󱁀X が成り立つが、 命題 2.7 を使うことで ⊨󰔃󱁀◻X すなわち ⊨󰔃󱁀A が導かれる。

これで全ての場合が尽くされたので、 定理の主張が示された。

証明.

全て定理 9.3 の特別な場合である。 追加されているスキーマが恒真となるモデルのクラスについては、 命題 3.8 を参照すれば良い。

なお、 最後の K[T,5] については少しコメントが必要かもしれない。 定理 9.3 によって K[T,5] が反射的かつ Euclid 的なモデル全体に対して健全であることはすぐに分かるが、 実は反射的かつ Euclid 的な関係とは同値関係のことである。 このことは直接確かめることもできるが、 命題 8.5 によって K[T,5] が K[T,B,4] と同型であることを踏まえるとすぐに分かる。 K[T,B,4] に対応するのは反射的かつ対称かつ推移的なモデル全体であるが、 反射的かつ対称かつ推移的な関係とはまさに同値関係である。

証明.

公理の追加で得られるあらゆる体系が上記の 15 種類の体系に帰結させられることは、 命題 8.5 から分かる。 また、 それらの間の包含関係も、 命題 8.1, 命題 8.2, 命題 8.3, 命題 8.4 を適宜使うことですぐに分かる。 これの具体的な議論は省略する。 したがって、 後は上記の 15 種類の体系が互いに同型でないことを示せば良い。 これも、 代表的なところだけ証明して、 残りは省略する。

モデル 󰒤:=(W,∼,P) を、 相異なる元 α,β をとって、 W := {α,β} ∼ := {(α,α),(β,β),(α,β)} Pn := {α}(n∈󱀍) で定めると、 この 󰒤 は反射的かつ推移的であり、 すなわち 󰒤∈Refl∩Tran である。 一方、 ⊭α󰒤p0⇀◻⬦p0 かつ ⊭α󰒤⬦p0⇀◻⬦p0 であることも容易に確かめられる。 ここに出てきた式はそれぞれ B と 5 に属するから、 これにより ⊭Refl∩TranB と ⊭Refl∩Tran5 が示されたことになる。 したがって、 定理 9.3 の対偶と命題 9.1 により、 󱁑⊆K[T,4] を満たす理論 󱁑 に対して、 ⊬󱁑B と ⊬󱁑5 が成り立つ。 これより、 󱁒⊇K[B] もしくは 󱁒⊇K[5] を満たす理論 󱁒 に対して、 󱁑 では B と 5 がどちらも証明できないのに対して 󱁒 では B と 5 のどちらかは証明できるので、 󱁑≠󱁒 である。 このことからは例えば、 K[T]≠K[T,B], K[T,4]≠K[T,5], K[D]≠K[D,B], K≠K[5] などが分かる。