公理型（英：axiom schema、英複数形：axiom schemata）とは、数理論理学における用語で、公理を一般化した概念である。任意の公理型は何らかの公理系における整論理式であり、そこには一つ以上の型変数が現れる。これらの変数はメタ言語学的な構成物であり、所与の体系における項や部分論理式に相当し、一定の条件を満たすことが要請される場合やされない場合がある。一定の条件とは、例えば特定の変数が自由変項であることや、またはそうした特定の変数が部分論理式や項に現れないことなどである。型変数に代入されうる部分論理式や項の個数が可算無限だとすれば、ある公理型は可算無限個の公理の集合を表すことになる。この集合は通常は再帰的に定義できる。公理型を用いずに公理化できる理論は「有限公理化」可能であると言う。有限公理化可能な理論は、たとえそれらが推論を行う上で実用性に劣っていても、超数学的なエレガントさの上では幾分か優位であると看做される。公理型の実例としてよく知られているものを二つ挙げる。これらの型は除去できないことが証明されている（最初の証明はリチャード・モンタギューによる）。従ってペアノ算術とZFCは有限公理化できない。このことは数学の様々な公理的理論や、哲学、言語学その他についても当てはまる。ZFCで証明できる定理は全て(NBG)でも証明できるが、大変驚くべきことに、後者は有限公理化されている。新基礎集合論(NF)は有限公理化可能だが、その場合はエレガントさが幾分か失われる。一階述語論理における型変数は、二階述語論理においては通常は除去できる。何故なら、型変数は何らかの理論中に現れる要素間で成り立つ性質や関係そのものを代入可能な変数として位置付けられることが多いからである。上で挙げた"帰納法" と"置換" の型は正にそうした例に当る。高階述語論理では量化変数を用いてあらゆる性質や関係を渡るような記述ができる。

出典:wikipedia