Suppose for the sake of contradiction that such a formula ϕ exists. By the diagonal lemma applied to ¬ϕ, there is some sentence ψ such that, provably, ¬ϕ(┌ψ┐)↔ψ. By the soundness of our theory, in fact ¬ϕ(┌ψ┐)↔ψ. But by the property for ϕ we also have ϕ(┌ψ┐)↔ψ, which means ¬ϕ(┌ψ┐)↔ϕ(┌ψ┐), a contradiction.
This seems to be the “semantic” version of the theorem, where the property for ϕ is stated outside the system. There is also a “syntactic” version where the property for ϕ is stated within the system.
My solution for #12:
Suppose for the sake of contradiction that such a formula ϕ exists. By the diagonal lemma applied to ¬ϕ, there is some sentence ψ such that, provably, ¬ϕ(┌ψ┐)↔ψ. By the soundness of our theory, in fact ¬ϕ(┌ψ┐)↔ψ. But by the property for ϕ we also have ϕ(┌ψ┐)↔ψ, which means ¬ϕ(┌ψ┐)↔ϕ(┌ψ┐), a contradiction.
This seems to be the “semantic” version of the theorem, where the property for ϕ is stated outside the system. There is also a “syntactic” version where the property for ϕ is stated within the system.