論理

いずれは形式集合論の方で行っている証明をそのままCoqで検証していくつもりなのですが、コンピューターソフト上で証明を行うとなると、いくら自明な恒真式でも証明を省略するわけにはいきません。そこで最初は、具体的な定理の証明のときに使いそうな恒真式などを証明していきたいと思います。