|
公理図式公理図式（英：axiom schema、英複数形：axiom schemata）とは、数理論理学における用語で、公理を一般化した概念である。公理型とも訳される。 定義公理図式とは、ある一群の（多くの場合には無限個の）類似の「形式」（schema）を持った公理を、メタ変数を含む単一の論理式で表現したものをいう。より正確にいえば、項を表すメタ変数記号と、論理式を表すメタ変数記号とを含むような拡大言語を考えたときに、その拡大言語に於ける論理式として記述された公理が公理図式である。メタ変数記号に代入される項や論理式に何かしらの条件（自由変数の出現に関する条件等）を付ける場合もある。具体的な公理はそれらのメタ変数に項や論理式を代入することによって得られる。 有限公理化メタ変数に代入されうる部分論理式や項が可算無限通りあるとすれば、その公理図式は可算無限個の公理の集合を表すことになる。この集合は、メタ変数に代入される論理式や項に付された条件が再帰的に判定可能である限り、再帰的に定義できる。公理図式を用いずとも有限個の公理のみで公理化できる理論は「有限公理化」可能であると言う。有限公理化可能な理論は、たとえそれらが推論を行う上で実用性に劣っていても、超数学的によい性質を持つ場合がある。 公理図式の例公理図式の実例としてよく知られているものを二つ挙げる。 これらの図式は除去できないことが証明されている（最初の証明はリチャード・モンタギューによる）。従ってペアノ算術とZFCは有限公理化できない。このことは数学の様々な公理的理論や、哲学、言語学その他についても当てはまる。 有限公理化可能な理論ZFCで証明できる定理は全てフォン・ノイマン＝ベルナイス＝ゲーデル集合論(NBG)でも証明できるが、大変驚くべきことに、後者は有限公理化されている。新基礎集合論(NF)は有限公理化可能だが、その場合はエレガントさが幾分か失われる。 高階論理において一階述語論理におけるメタ変数は、二階述語論理においては通常は除去できる。何故なら、メタ変数は何らかの理論中に現れる要素間で成り立つ性質や関係そのものを代入可能な変数として位置付けられることが多いからである。上で挙げた帰納法 と置換 の図式は正にそうした例に当る。高階述語論理では量化変数を用いてあらゆる性質や関係を渡るような記述ができる。 参考文献
脚注 |
