Let $I$ be the statement "there is an inaccessible cardinal".
I'm aware of two proofs of "If $ZFC\vdash I$ then $ZFC$ is inconsistent".
One proof uses the Second Incompleteness Theorem, which I understand.
The other proof goes something like:
1) Suppose $ZFC\vdash I$.
2) Then we have $ZFC\vdash ^{\backprime\backprime} V_\kappa\models ZFC ^{\prime\prime}$ where $\kappa$ is the least inaccessible cardinal.
3) Then by absoluteness results, we have $ZFC\vdash ^{\backprime\backprime}V_\kappa\models\neg I ^{\prime\prime}$.
4) Thus we have a model of $ZFC+\neg I$
And this is where this version of the proof ends in all sources I've come across.
I was wondering how the rest of the proof should go to get that $ZFC$ really is inconsistent.
My idea was it is essential to use the fact:
(*) If $ZFC\vdash\varphi$ then $ZFC\vdash ^{\backprime\backprime}ZFC\vdash\varphi ^{\prime\prime}$ for any sentence $\varphi$.
Then to finish:
5) Since we've assumed $ZFC\vdash I$, then we have $ZFC\vdash ^{\backprime\backprime}ZFC\vdash I ^{\prime\prime}$ by (*).
6) And since $ZFC\vdash ^{\backprime\backprime}V_\kappa\models ZFC^{\prime\prime}$, then we have $ZFC\vdash ^{\backprime\backprime}V_\kappa\models I ^{\prime\prime}$ by using 5).
7) By 3), we have $ZFC\vdash ^{\backprime\backprime}V_\kappa\nvDash I ^{\prime\prime}$.
8) So since $ZFC\vdash ^{\backprime\backprime}V_\kappa\models I ^{\prime\prime}$ and $ZFC\vdash ^{\backprime\backprime}V_\kappa\nvDash I ^{\prime\prime}$, then $ZFC$ is inconsistent.
Is this the way the proof is typically finished or is it somehow not necessary to appeal to (*)?
Any help is appreciated, thanks.
You could run the argument schematically. For instance, using induction in the metatheory you could show that (1) when $\phi$ is an axiom of ZFC, ZFC proves "if $V_\kappa$ is an inaccessible rank, then $V_\kappa\vDash \phi$"; and (2) when $\psi$ is a consequence of $\phi$, ZFC proves "if $M\vDash \phi$, then $M\vDash \psi$".