Gödel's incompleteness theorems

To which of these theories does the first incompleteness theorem (Rosser's form) apply, assuming each is consistent? Choose all that apply.

Code a string $s_1 s_2 \cdots s_k$ by $2^{c(s_1)} 3^{c(s_2)} 5^{c(s_3)} \cdots$, with symbol codes $c(0) = 1$, $c(=) = 5$ and $c(S) = 3$. What is the Gödel number of the string $S0 = 0$?

In Gödel's form of the first theorem, part (a) shows $T \nvdash G_T$ and part (b) shows $T \nvdash \neg G_T$. Which hypothesis does part (b) need beyond those of part (a)?

Assume $\mathsf{PA}$ is consistent, and let $T' = \mathsf{PA} + G$ where $G$ is the Gödel sentence of $\mathsf{PA}$. Which statements are true? Choose all that apply.

Löb's theorem: if $T \vdash \mathrm{Prov}_T(\ulcorner\varphi\urcorner) \to \varphi$, then $T \vdash \varphi$ (for $T \supseteq \mathsf{PA}$ recursively axiomatised). Apply it with $\varphi$ the sentence $0 = S0$. What do you obtain?

In the Lean file, which statement correctly formalises the abstract form of Tarski's theorem for a diagonalisable system S (with hcompl and hdiag as hypotheses)?

The Lean theorem halting_incompleteness has hypotheses hre : REPred Provable, hc : Computable nonHalt and sound. Which hypothesis expresses that the theory is recursively axiomatised?

Write encode(codes), which sends a list of positive symbol codes $[c_1, \dots, c_k]$ to $2^{c_1} 3^{c_2} \cdots p_k^{c_k}$, and decode(n), which recovers the list (and [] from 1). Why is decode(encode(xs)) == xs guaranteed?