I have read Kunen's Theorem III.7.13 ($V=L$ implies diamond principle at $\omega_1$) before, but today found that I don't really understand it. The proof roughly goes like this.
For limit ordinals $\alpha$, define
$P(\alpha,A,C)\Leftrightarrow A,C\subseteq\alpha\ \land\ C\text{ is club in }\alpha\ \land \lnot\exists\xi\in C[A\cap\xi=A_\xi]$
Inductively for limit $\alpha<\omega_1$, let $(A_\alpha,C_\alpha)$ be the $<_L$-least pair such that $P(\alpha,A,C)$; if there is no such pair or $\alpha$ is not a limit, let $A_\alpha=C_\alpha=\emptyset$. Suppose $(A_\alpha\mid\alpha<\omega_1)$ is not a $\Diamond$ sequence, then take a countable $M\prec L_{\omega_2}=H(\omega_2)$ and also its transitive collapse. Since the definition of $(A_\alpha\mid\alpha<\omega_1)$ is absolute for any transitive model of $ZF-P+V=L$, one can somehow obtain a contradiction.
Why is the sequence absolute? Of course $<_L$ is absolute and $P(\alpha,A,C)$ is absolute, but I don't see why that is true for $\exists A\exists C\ P(\alpha,A,C)$.
I know Kunen proves $\Diamond^+$ right after this but haven't looked at that one.
I also want to learn how other people understand this proof. At first I thought it to be some sort of "greedy algorithm", but if that were the case one would take the least $A\subseteq\omega_1$ that hadn't been guessed, not $A\subseteq\alpha$. Of course then there's no hope to use absoluteness so it doesn't work.
Best Answer
The idea is very close to forcing. How would you add a generic diamond sequence? You will approximate it by initial segments.
How would you do it over $L$? You approximate it using the $<_L$ order.
The key point is that given a countable model, $M$, of $\sf ZF-P$, we can diagonalise over the sets that it knows to produce a counterexample. If you prefer, think about this as just avoiding all the countably many countable sets that are in the model. Easy, I know.
Now, since every subset of $\omega_1$, including the diamond sequence itself (which formally is a subset of $\omega_1\times\omega_1$), appears in $L_{\omega_2}$, if the definition didn't work, this would be already true in $L_{\omega_2}$, and we have a definable $<_L$-minimal counterexample. Say $(A,C)$ where $A$ is a set and $C$ is a club.
Take $M\prec L_{\omega_2}$, then by definability our sequence, as well our counterexample, are all in $M$. Letting $L_\gamma$ be the transitive collapse of $M$ and letting $\delta$ be the ordinal $\omega_1$ is mapped to, namely, $\delta=\omega_1^{L_\gamma}$, we get that $(A\cap\delta,C\cap\delta)$ is exactly the image of $(A,C)$ under the isomorphism, and that the image of the sequence $(A_\alpha\mid\alpha<\omega_1)$ is just its truncation to $\delta$.
This means that in $L_\gamma$, this is the $<_L$-minimal counterexample, and therefore in $L_{\omega_2}$ this is also the $<_L$-minimal counterexample for that stage, which meant that we took that $A\cap\delta$ to be $A_\delta$. And that is a contradiction.
As I mention above, it is much easier to understand this claim if you understand forcing. This is quite literally "constructing the generic using $<_L$-minimal counterexamples". And if you really understand forcing, there is a method to force $\sf PFA$ and other forcing axioms by "least rank counterexample" that kind of operates on the same principle (since it replaces adding a Laver diamond sequence as a first step).