>>608

つづき

https://ja.wikipedia.org/wiki/%E5%85%AC%E7%90%86%E5%9E%8B
公理型
（公理図式から転送）
ナビゲーションに移動検索に移動
公理型（英：axiom schema、英複数形：axiom schemata）とは、数理論理学における用語で、公理を一般化した概念である。

有限公理化
型変数に代入されうる部分論理式や項の個数が可算無限だとすれば、ある公理型は可算無限個の公理の集合を表すことになる。
この集合は通常は再帰的に定義できる。公理型を用いずに公理化できる理論は「有限公理化」可能であると言う。
有限公理化可能な理論は、たとえそれらが推論を行う上で実用性に劣っていても、超数学的なエレガントさの上では幾分か優位であると看做される。

公理型の例
公理型の実例としてよく知られているものを二つ挙げる。

帰納型：ペアノ算術の一部であり自然数の算術である。
置換の公理型（英語版）：集合論の標準的なZFC公理系による公理化の一部。
これらの型は除去できないことが証明されている（最初の証明はリチャード・モンタギューによる）。従ってペアノ算術とZFCは有限公理化できない。このことは数学の様々な公理的理論や、哲学、言語学その他についても当てはまる。

有限公理化可能な理論
ZFCで証明できる定理は全てフォン・ノイマン＝ベルナイス＝ゲーデル集合論（英語版）(NBG)でも証明できるが、大変驚くべきことに、後者は有限公理化されている。新基礎集合論(NF)は有限公理化可能だが、その場合はエレガントさが幾分か失われる。

つづく