有限公理化可能
Def
理論$ Tが高々有限個の公理によって定義されるとき，$ Tは有限公理化可能という．
remark: 有限個の公理図式ではない．
Memo
Robinson算術$ \sf Qは一般に8個ぐらいの公理によって定義されるため，有限公理化可能である．
#Robinson算術の有限公理化可能性
一方，一般にPeano算術$ \sf PAやTarski-Mostowski-Robinson算術$ \sf Rは公理図式によって特徴づけられるため，有限公理化可能ではない．すなわち無限個の公理を持つ．
Prop
有限公理化可能な理論$ Tについて，$ Tの全ての公理を$ \landで結んだ論理式$ \bigwedge Tは明らかに文である．
この事実を用いて1階述語論理の決定不能性を示すこともできる．
一方，有限公理化可能でない理論についてはそのような論理式を考えることは一般に出来ない．もし考えると無限の長さの論理式となり，一般に無限の長さの論理式は許容されないためでる．