導出とシーケントを混同する理由 - (新) 檜山正幸のキマイラ飼育記 メモ編 に関連して。
信頼できる目録があるとする。目録に登録されていることが、存在を保証するならば、
- 登録は存在命題に匹敵する。
演繹システムのシステム指標／ライブラリ指標は、信頼できる目録だから、指標に登録されていると、それはセマンティック背景圏の対象・射・オペレータ・2-射などの存在命題になる。存在命題（インデックス付き存在命題）に対するスコーレム関数は、インデックス付き族となる。
インデックス付き族を“規則”と呼んでいるのだろう。インデックスを具体化することが規則の具体化。規則の具体化は、全称命題の具体化ではあるが、メタ全称命題（インデックス付き存在命題は全称命題）の具体化に対応する。
演繹システムにおいては、次が同じ効果を持つ。
- インデックス付き導出族の登録
- メタなインデックス付き存在命題（全体はメタな全称命題）
- スコーレム関数として与えられる“規則”
- 構成的・具体的な関数として与えられる“規則”
登録が、メタなインデックス付き存在命題を主張することと同じであることが見過ごされやすい。また、スコーレム関数があれば十分だが、構成的・具体的に与えられることが多い。
