空中戦 // \( \forall x \)や\( \exists y\)などの量限定子がついた変数を全て除去出来れば、自由変数だけからなる式が出来ます。これを同値変形で求めることができれば、量限定子除去した結果の自由変数の式は元の式が成立するための（必要十分）条件となり…