高階述語論理

提供: miniwiki
移動先:案内検索

高階述語論理(こうかいじゅつごろんり、: Higher-order logic)は、一階述語論理と様々な意味で対比される用語である。

例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。

その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語(higher-order predicate)とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である(ここで n > 1)。同じことは高階関数(higher-order function)にも言える。

高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は(帰納的に公理化された)健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。

高階述語論理の例として、アロンゾ・チャーチSimple Theory of Types や Calculus of Constructions (CoC) がある。

関連項目

参考文献

  • Andrews, P.B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers, available from Springer.
  • Church, Alonzo, 1940, "A Formulation of the Simple Theory of Types," Journal of Symbolic Logic 5: 56-68.
  • Henkin, Leon, 1950, "Completeness in the Theory of Types," Journal of Symbolic Logic 15: 81-91.
  • Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press.
  • Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
  • Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press.

外部リンク

テンプレート:Logic