Exercise:
Show that if $F$ is a closed formula and if $$\mathcal{P} \vdash \exists v_0\; Drv[ \underline{\#F},v_0]\Rightarrow F,$$ then $$\mathbb{P}\vdash F.$$
Solution:
Suppose that $$\mathcal{P} \vdash \exists v_0\; Drv[ \underline{\#F},v_0]\Rightarrow F,$$ then by taking the contrapositive, $$\mathcal{P} \vdash \lnot F \Rightarrow \lnot \exists v_0\; Drv[ \underline{\#F},v_0],$$ equivalently, $$\mathcal{P}\cup \{\lnot F\} \vdash \lnot \exists v_0\; Drv[ \underline{\#F},v_0].$$ But $\lnot \exists v_0\; Drv[ \underline{\#F},v_0]$ means that $F$ is not derivable in $\mathcal{P}$, in other words, that $\mathcal{P}\cup \lnot F$ is a consistent theory. So we have $$\mathcal{P}\cup \{\lnot F\} \vdash Con(\mathcal{P}\cup \{\lnot F\},$$ which implies, according to Gödel's second incompleteness theorem, that $\mathcal{P}\cup \{\lnot F\}$ is not a consistent theory; hence $\mathcal{P}\vdash F$.
I don't understand why suddenly we have $$\mathcal{P}\cup \{\lnot F\} \vdash Con(\mathcal{P}\cup \{\lnot F\}.$$ Could you help? Thanks in advance!
The point is that "$\neg\exists v_0 Drv[\underline{\# F}, v_0]$" is equivalent to "$Con(\mathcal{P}\cup\{\neg F\})$:" intuitively, $\mathcal{P}$ fails to prove $F$ iff $\mathcal{P}\cup\{\neg F\}$ is consistent.
This equivalence is provable in a very weak system, e.g. $\mathcal{P}$ itself.
A bit more precisely, we're combining the sequent $$\mathcal{P}\cup\{\neg F\}\vdash \neg\exists v_0 Drv[\underline{\# F}, v_0]$$ which we've gotten from the argument so far and the sequent $$\mathcal{P}\vdash \neg\exists v_0 Drv[\underline{\#F}, v_0]\leftrightarrow Con(\mathcal{P}\cup\{\neg F\})$$ which holds in general.