>>722 補足
>>Qが有限公理化されているってのは言い過ぎなような気が

ここの 有限公理化は
下記の ツェルメロ＝フレンケル集合論 公理図式
『この公理図式は、実際には無限個の公理を含意する』
および
フォン・ノイマン＝ベルナイス＝ゲーデル集合論 NBG
『NBGは有限公理化できる一方、ZFCやMKではできない』
と関係している

集合の濃度の”無限”とは 話は別

https://ja.wikipedia.org/wiki/%E3%83%84%E3%82%A7%E3%83%AB%E3%83%A1%E3%83%AD%EF%BC%9D%E3%83%95%E3%83%AC%E3%83%B3%E3%82%B1%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
ツェルメロ＝フレンケル集合論
公理
分出公理図式および置換公理図式は、（閉論理式としての）公理ではなく、ある論理式に対して一つの公理が対応する公理図式であることに注意を要する。この公理図式は、実際には無限個の公理を含意する。

https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A9%E3%83%B3%E3%83%BB%E3%83%8E%E3%82%A4%E3%83%9E%E3%83%B3%EF%BC%9D%E3%83%99%E3%83%AB%E3%83%8A%E3%82%A4%E3%82%B9%EF%BC%9D%E3%82%B2%E3%83%BC%E3%83%87%E3%83%AB%E9%9B%86%E5%90%88%E8%AB%96
フォン・ノイマン＝ベルナイス＝ゲーデル集合論
数学基礎論において、フォン・ノイマン＝ベルナイス＝ゲーデル集合論 (NBG) とはツェルメロ＝フレンケル集合論＋選択公理 (ZFC)の保存拡大である公理的集合論である。NBGでは、量化子の範囲を集合に限定した論理式によって定義される集合の集まりとして、クラスの概念を導入する。NBGは、すべての集合というクラスやすべての順序数というクラスといった、集合よりも大きいクラスを定義できる。モース＝ケリー集合論 (MK) は量化子の範囲がクラスである論理式によるクラスの定義を許容する。NBGは有限公理化できる一方、ZFCやMKではできない。