The Double-Negation Translation says that a classically equivalent proposition does hold in intuitionistic logic.

I think it doesn't. However, I suspect it doesn't allow to achieve self-trust in AI. I don't really understand intuitionistic logic, but if we only admit constructive proofs then Lucy won't be able to reason in full generality about Lucy2's reasoning, will she? Won't the step "Lucy2 took action A so there exists a proof that A is a good idea" fail since it doesn't constructively show the proof Lucy2 would find? It feels like intuitionistic logic overcomes the problem of "a proof that a proof exists" in a "degenerate" way, namely, since every proof is constructive "a proof that a proof exists" has to display an actual proof.