今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合、その変数や中身の式を証明することができません。そこで多くの場合には全称量化子 ∀を外してその中身にアクセスできるようにすることが証明の第一歩となります。 全称量化子 ∀がゴールの論理式に登場している場合、introタクティクを使うとその変数がラベル付きで導入されて、以降の証明で使えるようになります。 例えば前回見たcalcモードの説明の記事では偶関数…
