「公理型」の版間の差分

削除された内容 追加された内容
m ボット: 言語間リンク 6 件をウィキデータ上の (d:Q792536 に転記)
m 節分割を追加
1行目:
'''公理型'''(英:'''axiom schema'''、英複数形:axiom schemata)とは、[[数理論理学]]における用語で、[[公理]]を一般化した概念である。
 
==概要==
任意の公理型は何らかの[[公理系]]における[[整論理式]]であり、そこには一つ以上の型変数が現れる。これらの変数はメタ[[言語学]]的な構成物であり、所与の体系における[[一階述語論理#形成規則|項]]や[[一階述語論理|部分論理式]]に相当し、一定の条件を満たすことが要請される場合やされない場合がある。一定の条件とは、例えば特定の変数が[[自由変項]]であることや、またはそうした特定の変数が部分論理式や項に現れないことなどである。
 
==有限公理化==
型変数に代入されうる部分論理式や項の個数が[[可算]]無限だとすれば、ある公理型は可算無限個の公理の集合を表すことになる。この集合は通常は[[再帰]]的に定義できる。公理型を用いずに公理化できる理論は「有限公理化」可能であると言う。有限公理化可能な理論は、たとえそれらが推論を行う上で実用性に劣っていても、超数学的なエレガントさの上では幾分か優位であると看做される。
 
==公理型の例==
公理型の実例としてよく知られているものを二つ挙げる。
* [[帰納]]型:[[ペアノ算術]]の一部であり[[自然数]]の算術である。
* [[{{仮リンク|置換の公理型]]([[:|en:|Axiom schema of replacement|en]])}}:[[集合論]]の標準的な[[公理的集合論#ZFC|ZFC公理系]]による公理化の一部。
これらの型は除去できないことが証明されている(最初の証明は[[リチャード・モンタギュー]]による)。従ってペアノ算術とZFCは有限公理化できない。このことは数学の様々な公理的理論や、哲学、言語学その他についても当てはまる。
 
==有限公理化可能な理論==
ZFCで証明できる定理は全て[[{{仮リンク|フォンノイマンベルナイスゲーデル集合論]]|en|Von Neumann–Bernays–Gödel set theory}}(NBG)でも証明できるが、大変驚くべきことに、後者は有限公理化されている。[[新基礎集合論]](NF)は有限公理化可能だが、その場合はエレガントさが幾分か失われる。
 
==高階論理において==
[[一階述語論理]]における型変数は、二階述語論理においては通常は除去できる。何故なら、型変数は何らかの理論中に現れる要素間で成り立つ性質や[[二項関係|関係]]そのものを代入可能な変数として位置付けられることが多いからである。上で挙げた''帰納法'' と''置換'' の型は正にそうした例に当る。高階述語論理では[[量化]]変数を用いてあらゆる性質や関係を渡るような記述ができる。