全称導入 (∀I), 全称除去 (∀E)

全称導入は、任意に選んだ個体について、特別な仮定に依存せず命題を証明できたとき、全称命題へ一般化する規則である。

仕組みと確認

選んだ個体が任意であること、未解消の仮定がその個体を特別扱いしていないことを確認する。汎用関数やプロパティベーステストでも、入力の一般性を壊す条件を明示する。

限界と注意点

特定の例で成立した結果を全称へ拡張してはいけない。量化子のスコープと自由変数の条件を厳密に確認する。