2025/12/29 8:10
**「量化子除去を使った屠殺競技の問題」**
RSS: https://news.ycombinator.com/rss
要約▶
Japanese Translation:
以下は、すべての重要ポイントを保持し、不適切な推測や曖昧な表現を排除した簡潔版です。
Summary（要約）
この記事では、Sage が QEPCAD の量化消去エンジンと連携して、数学競技に登場する多項式不等式を解決または検証できることを示しています。Tarski–Seidenberg 定理（任意の論理式が多項式等号・不等号、ブール演算子、および量化子から構成されている場合、それは量化子のない式と同値である）を思い出させます。
具体例でこのことを示します：
-
2次判別式
[ \exists x.; a,x^2 + b,x + c = 0 ;\Longleftrightarrow; b^2-4ac \ge 0. ] -
混合量化子
[ \forall x,\exists y.;(x>0 \rightarrow a,x + b,y + xy > c) ;\Longleftrightarrow; b \ge 0 ,\vee, (c+ab < 0). ] -
Math Stack Exchange の不等式
(a,b\ge 0) で (a^4+b^4=17) とするとき、次を証明する
[ 15(a+b)\ge 17 + 14\sqrt{2ab}. ] 記事はこれを多項式不等式に書き換え、Sage に渡し、等号が成立するのは ((a,b)=(1,2)) または ((2,1)) のみであることを示しています。 -
逆数の積
(x,y,z>0) ならば証明すべき
[ (x+\tfrac1x)(y+\tfrac1y)(z+\tfrac1z) \ge (x+\tfrac1y)(y+\tfrac1z)(z+\tfrac1x). ] 分母をクリアした後、Sage は不等式を確認し、無限に多くの点で鋭いこと（sharp）を見つけます。
Sage は
sage -i qepcad本文
2021年12月22日
- タグ:
sage、featured
MSEで「簡単な」質問を見たときに、必ず「コンピュータがやってくれる！」と言いたくなることがあります。研究数学者なら、コンピュータが解ける問題に時間を費やすべきではありませんが、まだテクニックを学んでいる段階（あるいはMSEの多くの場合で宿題を解いている段階）では、そのコメントはあまり役立ちません。私は通常、回答しないようにしています。この衝動は、競技数学でよく見られる人為的な不等式に対して特に強く出ますが、今日はその衝動を抑えきれない質問を目にしました！MSEには適切ではないと感じましたが、幸いにも自分のブログがあるので好きなことを書けます :P
本日は「量化子除去」を使ってこれらの問題に一撃で対処する方法を見てみましょう！
この記事は短くまとめます。要点はモデル理論からの強力な定理です：
タルスキー–サイデンバーグ定理
変数ベクトル (\overline{x}) に関して
(p(\overline{x}) = 0,; p(\overline{x}) < 0)（(p \in \mathbb{R}[\overline{x}])）という形の式で、
論理結合子 (\lor,,\land,,\lnot,,\to) と量化子 (\exists,,\forall) で組み合わせたものは、
その式と論理的に等価な「量化子のない」式が存在します。
例。
[
\exists x.; ax^2 + bx + c = 0
]
（量化子を含む）という式は、(b^{2}-4ac \ge 0) と等価です。
もう少し複雑な例：
[ \forall x,\exists y;\bigl(x>0 \to ax+by+xy>c\bigr) \quad\Longleftrightarrow\quad b \ge 0 ;\lor; c + ab < 0 . ]
したがって、上記の式がある実数 (a,b,c) に対して真であるかどうかを判定するには、この量化子のない式に代入し、単純にチェックすればよいのです！
これらの量化子のない表現はどのように見つけたか？
Sage！ Sage は多くの既存ソフトウェアパッケージとインタフェースを持っています。私たちにとって関連するインタフェースは QEPCAD で、実際に量化子除去を行います。
始めるには、Sage がアクセスできる形で QEPCAD をインストールしてください。まだインストールしていない場合は
sage -i qepcad
を実行します。
以下では、「より複雑な例」から量化子を除去する手順を示します。とても簡単です！
競技数学の問題
1. 本投稿をきっかけにした問題
(a,b \ge 0) で (a^4 + b^4 = 17)。
次を証明せよ：
[ 15(a+b) \ge 17 + 14\sqrt{2ab}. ]
これは多項式としては与えられていませんが、次のように書き換えることができます：
[ (15(a+b)-17)^2 ;\ge; 14^2 \cdot 2ab . ]
この形で QEPCAD を通じて Sage に量化子を除去させます。
また、等号が成り立つのは ((a,b)=(1,2)) および ((2,1)) のみであるという仮説も Sage で確認できます。
2. 別の例
正の実数 (x,y,z) が与えられたとき、次を示せ
[ \Bigl(x+\frac{1}{x}\Bigr) \Bigl(y+\frac{1}{y}\Bigr) \Bigl(z+\frac{1}{z}\Bigr) ;\ge; \Bigl(x+\frac{1}{y}\Bigr) \Bigl(y+\frac{1}{z}\Bigr) \Bigl(z+\frac{1}{x}\Bigr). ]
この不等式はそのままでは多項式不等式でないため、両辺に (xyz) を掛けて多項式形に変換します。すると QEPCAD に入力できます。
Sage は不等式が無限多数の点で鋭い（等号が成り立つ）ことを示しています。すべて列挙する代わりに、解集合の幾何学的記述を求めます。（実際には (x=y) が決定因子となります。自分で導き出せるか試してみてください。）
練習問題
-
具体的な練習 – 好きなユークリッド幾何学の定理を座標系に書き直し、Sage に真偽判定させてみましょう！
例： ポトレイムの定理。 -
このツールを使って助かった経験があれば教えてください。実際の応用事例を聞かせていただけると嬉しいです！
-
Sage や類似プログラムで自動的に問題を解く驚きの用途があれば、ぜひ共有してください。
ではまた次回！ ^_^