$$ \newcommand{\tsf}[1]{{\sf{#1}}} \newcommand{\lb}{\left<} \newcommand{\rb}{\right>} \newcommand{\pair}[1]{\lb #1 \rb} \newcommand{\BB}{\mathbb{B}} \newcommand{\RR}{\mathbb{R}} \newcommand{\Pow}{\tsf{Pow}} \newcommand{\List}{\tsf{List}} \newcommand{\TwoPow}[1]{2^{#1}} \renewcommand{\implies}{⇒} \newcommand{\pto}{\to_{\text{?}}} \newcommand{{\not\vdash}}{{\not\vdash}} $$

High-level proof of Gödel's Second Incompleteness Theorem

Sort ArithForm₁ - Formulas of the language of arithmetic with one free variable.
Sort ArithSent
Sentences of the language of arithmetic (i.e. formulas with no free variables).
Sort ℕLiteral
The set of (closed) number terms $0, s(0), s(s(0)),\ldots$ (not all the closed terms of the language of arithmetic).

$\bot$ : ArithSent - ¬(0=0), or negation of any sentence provable from the axioms of PA
$\vdash_{\text{PA}}$ : ArithSent → 𝔹 - The given sentence is provable from the axioms of PA.
Defn ${\not\vdash}_{\text{PA}}$ : ArithSent → 𝔹 - ${\not\vdash}_{\text{PA}}$ x ⇔ ¬($\vdash_{\text{PA}}$ x) - The given sentence is not provable from the axioms of PA.
$\stackrel{\cdot}{¬}$ : ArithSent → ArithSent
Arithmetic sentence obtained by negating the given arithmetic sentence.
$\stackrel{\cdot}{⇒}, \stackrel{\cdot}{⇔}$ : ArithSent × ArithSent → ArithSent
Arithmetic sentence obtained by joining the two given arithmetic sentence with the implication connective (resp. iff connective).
Pr : ArithForm₁
Formula with one free variable that defines (in the standard model of arithmetic) the relation "is the code of a sentence that is provable from the axioms of PA".
subst : ArithForm₁ × ℕLiteral → ArithSent
Substitution of a number term for the free variable in a formula with exactly one free variable.
# : ArithSent → ℕLiteral - The code of the given arithmetic sentence.
Defn P : ArithSent → ArithSent - P(ψ) := subst(Pr, #(ψ))

Axiom 4: ∃φ. $\vdash_{\text{PA}}$ (φ $\stackrel{\cdot}{⇔}$ $\stackrel{\cdot}{¬}$${}$P(φ))
Gödel's fixed-point lemma; φ is an ArithSent that asserts (truthfully) that its own code is not the code of a PA-provable sentence.
Let $φ_{\text{liar}}$ : ArithSent be a witness for the previous sentence.
Axiom 5: (${\not\vdash}_{\text{PA}}$ $\bot$) ⇒ (${\not\vdash}_{\text{PA}}$ $φ_{\text{liar}}$)
Gödel's first incompleteness theorem; if PA is consistent then it does not prove the liar sentence.
Axiom 6: $\vdash_{\text{PA}}$ ($\stackrel{\cdot}{¬}$${}$P($\bot$) $\stackrel{\cdot}{⇒}$ $\stackrel{\cdot}{¬}$${}$P($φ_{\text{liar}}$)) - PA internally proves Gödel's first incompleteness theorem

$\tsf{Theorem}$: (${\not\vdash}_{\text{PA}}$ $\bot$) ⇒ (${\not\vdash}_{\text{PA}}$ $\stackrel{\cdot}{¬}$${}$P($\bot$))
If PA is consistent then it does not prove (an arithmetization of) the statement of its consistency.
Assume ${\not\vdash}_{\text{PA}}$ $\bot$
Lemma 1: ${\not\vdash}_{\text{PA}}$ $φ_{\text{liar}}$ From previous assumption and Gödel's first incompleteness theorem.
Lemma 2: ${\not\vdash}_{\text{PA}}$ $\stackrel{\cdot}{¬}$${}$P($\bot$)
Assume PA is consistent. $\vdash_{\text{PA}}$ $\stackrel{\cdot}{¬}$${}$P($\bot$) - PA is consistent.
Lemma 3: $\vdash_{\text{PA}}$ $\stackrel{\cdot}{¬}$${}$P($φ_{\text{liar}}$) from previous assumption, Axiom 6, and property of $\vdash_{\text{PA}}$.
Lemma 4: $\vdash_{\text{PA}}$ $φ_{\text{liar}}$ by property of $\vdash_{\text{PA}}$ and Axiom 5.
Lemma 5: false - previous line contradicts earlier assumption of ${\not\vdash}_{\text{PA}}$ $\bot$.
Lemma 6: ${\not\vdash}_{\text{PA}}$ $\stackrel{\cdot}{¬}$${}$P($\bot$) since we just derived a contradiction from the assumption $\vdash_{\text{PA}}$ $\stackrel{\cdot}{¬}$${}$P($\bot$).