公理図式

公理図式の概要

公理図式（英：axiom schema）は、数理論理学の分野で使用される概念であり、公理を一般化した形式として位置づけられています。具体的には、無限個の類似の公理を、メタ変数を使用して一つの論理式として表現する方法を指します。このメタ変数は、特定の項や論理式を代入することが可能で、それによって具体的な公理が生成されます。

定義と構造

公理図式は、特定の形式を持つ無限公理の集合を、メタ変数が含まれる単一の論理式として表現するものです。メタ変数記号は項を、また別のメタ変数記号は論理式を表し、これらを用いて拡張された言語での論理式として定義されます。また、メタ変数に代入される要素に条件を付与することもあり、自由変数の出現に関するルールなどが適用されることがあります。これにより、特定の条件に従った具体的な公理が導出されるのです。

公理図式の有限公理化

もし、メタ変数に代入可能な部分論理式や項が可算無限通り存在する場合、その公理図式は可算無限の公理の集合を表しています。この集合は、代入される論理式や項に付随する条件が再帰的に判定できる場合に再帰的に定義できます。このように、有限個の公理で理論が成立する場合、その理論は「有限公理化可能」と呼ばれます。たとえ実用性が低くとも、有限公理化可能な理論は超数学的な意義を持つとされます。

公理図式の実例

よく知られている公理図式の例としては、以下の2つが挙げられます。

1. 帰納法図式：ペアノ算術における自然数の算術に関するもので、帰納的な性質の形成を可能にします。
2. 置換公理図式：集合論の標準的なZFC公理系において用いられる、公理の一部です。

これらの公理図式は除去不可能であることが証明されており、ペアノ算術やZFCは有限公理化できないことが示されています。このことは数学の多くの公理的理論、哲学、そして言語学にも影響を及ぼします。

有限公理化可能な理論

ZFCで証明できる全ての定理は、フォン・ノイマン＝ベルナイス＝ゲーデル集合論（NBG）でも証明可能ですが、NBGは驚くべきことに有限公理化されています。また、新基礎集合論（NF）も有限公理化可能ですが、その場合は美しさが失われることがあります。

高階論理における公理図式

一階述語論理では適用できるメタ変数が、通常は二階述語論理においては除去されることが多いです。これは、メタ変数が理論内の要素間の性質や関係を代入可能な変数として作用するためです。例として挙げた帰納法と置換の図式もこのカテゴリーに属します。高階述語論理では、量化変数を使用してより幅広い性質や関係性を表現することが可能となります。

参考文献

• - Schema （英語） - スタンフォード哲学百科事典「John Corcoran」の項目
• - Corcoran, J. 2006. Schemata: the Concept of Schema in the History of Logic. Bulletin of Symbolic Logic 12: 219-40.
• - Mendelson, Elliot, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
• - Potter, Michael, 2004. Set Theory and its Philosophy. Oxford Univ. Press.

もう一度検索