>>713
>Qは=付きで定義されていて=の公理は無限じゃないの？
>Qが有限公理化されているってのは言い過ぎなような気が
>Qをさらに=無しで考え直したQ’で有限公理化されたものがあるのかな

横レスですが
https://ja.wikipedia.org/wiki/%E3%83%AD%E3%83%93%E3%83%B3%E3%82%BD%E3%83%B3%E7%AE%97%E8%A1%93
ロビンソン算術
超数学
Qの状況は非常に複雑である。QはPAよりも弱い有限公理化可能な一階の理論と考えられ、それらの公理は存在量化をただひとつ持ち、PAが不完全であるのと同様にゲーデルの不完全性定理の意味で不完全であり、本質的に決定不能である。ロビンソンは(Robinson (1950))において、任意の計算可能関数が表現可能ならしめるPAの公理が何であるかを考えることにより、Qの公理(Q1)–(Q7)を導き出した。PAの帰納法の公理図式は上記(Q3)の証明にのみ必要であり、表現可能性の証明の他の部分には全く必要がない。それゆえ任意の計算可能関数はQにおいて表現可能である(Mendelson (1997): Th 3.33, Rautenberg (2010): 246})。

＜en.wikipediaより＞
https://en.wikipedia.org/wiki/Robinson_arithmetic
Robinson arithmetic
Q is a finitely axiomatized first-order theory that is considerably weaker than Peano arithmetic (PA), and whose axioms contain only one existential quantifier. Yet like PA it is incomplete and incompletable in the sense of Gödel's incompleteness theorems, and essentially undecidable. Robinson (1950) derived the Q axioms (1)–(7) above by noting just what PA axioms are required [4] to prove that every computable function is representable in PA.[5] The only use this proof makes of the PA axiom schema of induction is to prove a statement that is axiom (3) above, and so, all computable functions are representable in Q.[6][7][8] The conclusion of Gödel's second incompleteness theorem also holds for Q: no consistent recursively axiomatized extension of Q can prove its own consistency, even if we additionally restrict Gödel numbers of proofs to a definable cut.[9][10][11]