- 205 名前：１３２人目の素数さん mailto:sage [2012/04/15(日) 20:31:49.29 ]
- >>168ですけど、
任意の論理式ψについて、¬¬ψが直観主義論理において証明不可能ならば、古典論理においても
妥当式ではないと言えるのでしょうか?
((A→B)→A)→A は証明できないとしても、¬¬(((A→B)→A)→A)は
証明できますよね？
あと、A→¬¬Aは最小論理で証明できるので、ψが直観主義論理で
証明できるなら、¬¬ψも直観主義論理で証明できるのでしょうか?
(少なくとも、¬¬(A→A)は、証明できますよね・・・)
ならば、
結合記号¬→のみで表される命題Pが妥当式ならば、
¬¬Pは、結合記号¬→⊥の導入と除去だけで、
証明図を示せるのでしょうか?
