閉包と推論システム

論理 半形式証明スクリプト

推論システムの公理化の有名なものはアクツェル〈Aczel | アクゼル〉のもので、

  • Aczel, Peter (1977). “An Introduction to Inductive Definitions”. In: Handbook of Mathematical Logic. Ed. by Jon Barwise. Vol. 90. Studies in Logic and the Foundations of Mathematics. Elsevier, pp. 739 –782.

だったらしい。次の修士論文に詳しい。

ムーア閉包〈Moore closure〉については：

あるいは：

伴意システムのセットアップと公理は：

セットアップ：

  • $`E\subseteq \mathrm{Sen}(\Sigma)`$
  • $`\vdash_\Sigma `$ は、$`\mathrm{Pow}(\mathrm{Sen}(\Sigma)), \mathrm{Sen}(\Sigma)`$ の関係

公理：

  1. $`E \vdash_\Sigma \rho \text{ when }\rho\in E`$
  2. $`\text{If }E \vdash_\Sigma \gamma \text{ for each }\gamma\in \Gamma \text{ and }\Gamma \vdash_\Sigma \rho \text{ then }E \vdash_\Sigma \rho`$
  3. $`\text{For each signature morphism }\varphi \,\colon\ \Sigma \rightarrow \Sigma'\\ \text{ if } \vdash_\Sigma \rho \text{ then }\mathrm{Sen}(\varphi)(E) \vdash_{\Sigma'} \mathrm{Sen}(\varphi)(\rho)`$
まとめ

アクツェル推論系〈inference system〉の定義は アクツェル推論系と不動点とアリーナ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編 にある。

アクツェルのオリジナル インスティチューション用語
判断 文
演繹ルール 伴意関係の生成系
前提集合 -
結論 -
ワンステップ演繹演算子 -
帰納的演繹演算子 閉包演繹演算子

閉包演繹演算子の公理：

  1. [単調性] A⊆B ⇒ Cl(A)⊆Cl(B)
  2. [増大性] A⊆Cl(A)
  3. [モナド性] Cl(Cl(A))⊆Cl(A)

閉包演算子からの伴意関係：

  • A |- a :⇔ a∈Cl(A)
参考文献