存在導入 (∃I), 存在除去 (∃E)

存在導入は、ある具体的な項について述語が成立することから、そのような要素が存在するという命題を得る規則である。証拠となる項を追跡できるため、構成的な読み方ができる。

仕組みと確認

具体的な証人と、その証人に必要な前提を記録する。検索結果やデータベースの存在判定でも、判定だけでなく対象の識別子と取得時点を残す。

限界と注意点

証人がスコープ外の変数に依存していないか確認する。存在を示す証拠が後から無効になる場合は、時間や整合性の条件も仕様化する。