計数定量化

計数量指定子は、 「プロパティX を満たす要素が少なくともk個存在する」という形式の量指定子を表す数学用語です。等式を伴う一階述語論理では、計数量指定子は通常の量指定子で定義できるため、このコンテキストでは表記上の省略形です。ただし、数え上げを伴う 2 変数論理など、数式内の変数の数を制限する論理のコンテキストでは興味深いものです。また、「無限に存在する」という一般化された計数量指定子は、一階述語論理の有限の数の式を使用して表現することはできません。

計数量指定子は、通常の量指定子を使用して再帰的に定義できます。

が「ちょうど が存在する」と表すとします。すると ${\displaystyle \exists ^{=k}}$${\displaystyle k}$

${\displaystyle {\begin{aligned}\exists ^{=0}xPx&\leftrightarrow \neg \exists xPx\\\exists ^{=k+1}xPx&\leftrightarrow \exists x(Px\land \exists ^{=k}y(y\neq x\land Py))\end{aligned}}}$

を「少なくとも が存在する」と表すと、 ${\displaystyle \exists ^{\geq k}}$${\displaystyle k}$

${\displaystyle {\begin{aligned}\exists ^{\geq 0}xPx&\leftrightarrow \top \\\exists ^{\geq k+1}xPx&\leftrightarrow \exists x(Px\land \exists ^{\geq k}y(y\neq x\land Py))\end{aligned}}}$

• ユニークさの定量化
• リンドストローム量指定子

• Erich Graedel、Martin Otto、Eric Rosen。「カウント付き 2 変数ロジックは決定可能」。第 12 回 IEEE コンピュータ サイエンス ロジック シンポジウム LICS `97 の議事録、Warschau。1997 年。Postscript ファイルOCLC  282402933