not not Pは「not Pの証明が存在するならば⊥の証明が存在する」という意味であって、そこから「Pの証明が存在する」は出てこない