全称導入

所謂一般化ってやつじゃないなと。
全称記号∀除去は別名「普遍汎化」とも呼ぶようです。

普遍汎化

定義

もし

$\displaystyle \vdash P(x)$が導出されていれば、

$\displaystyle \vdash \forall x\,P(x)$を導出してよい、という意味である。

Wikipedia

Wikipediaだと分かりにくいのでWIISでも確認しました。少し分かったのうな分からないような。

$c^{2}\geq 0\ \models \ \forall x\in \mathbb{R} :x^{2}\geq 0$

WIIS

0以上のcの二乗は実数かつ二乗すると0以上を満たす。cという代数的な表現を実数の要素xという表現に変更してもよいとする推理規則なのかなと。

全称除去は逆に具体的な数を代数的に表現できますよってことで。