>>168ですけど、

任意の論理式ψについて、¬¬ψが直観主義論理において証明不可能ならば、古典論理においても
妥当式ではないと言えるのでしょうか?

((A→B)→A)→A は証明できないとしても、¬¬(((A→B)→A)→A)は
証明できますよね？

あと、A→¬¬Aは最小論理で証明できるので、ψが直観主義論理で
証明できるなら、¬¬ψも直観主義論理で証明できるのでしょうか?
(少なくとも、¬¬(A→A)は、証明できますよね・・・)

ならば、

結合記号¬→のみで表される命題Pが妥当式ならば、
¬¬Pは、結合記号¬→⊥の導入と除去だけで、
証明図を示せるのでしょうか?