既存導出を組み合わせて新しい導出作ることにより証明を行う。このとき、実際の導出が何であるかは問題にならない。なので、シーケント〈導出のプロファイル〉を書くだけで導出を書いたことになる。これより、導出とシーケントが混同、あるいは同一視される。
A∧B → A はプロファイルだが、次の命題を考える。
- [射影命題] ∀A, B.∃f.( f:A∧B → A ) in (a category C)
これが真だとして、スコーレム関数 ψ を考える。
- (A, B) |→ ( (ψ[A, B] : A∧B → A) in (a category C) )
これは ψ:Obj(C)×Obj(C) → Mor(C) という関数を定義する。射のインデックス付き族になる。
今は 射＝導出 だから、導出のインデックス付き族になり、それを推論規則と呼ぶ。時系列で書くと：
- 射影命題のような、インデックス付き存在命題が与えられる。セマンティックな命題、メタ命題。
- インデックス付き存在命題のスコーレム関数を考える。
- そのスコーレム関数は、インデックス付き導出である。
- インデックス付き導出を“規則”と呼ぶ。
ここで注意すべきは、スコーレム関数さえあればよいこと。ψがほんとの射影である必要はない。ψを具体的に与えるとき典型的・簡単なのは射影だが、“規則”の実体が射影である必要性がない。
ここにギャップがある。仕組み上は射影である必要がないが、たいていはスコーレム関数の具体的な実現として射影を想定している。
次の概念のあいだの相互関係をよく理解すべきだ。
- インデックス付き存在命題〈indexed existential proposition〉
- スコーレム関数〈選択関数 | セクション〉
- スコーレム関数と同義のインデックス付き族
- 構成的・具体的に与えられたスコーレム関数
- スコーレム関数のプロファイル〈シーケント〉
- 規則とかパターンとか呼ばれるモノ
