A heuristic but very nice outline is given in Contents of Gentzen's consistency proof of PA

I wonder, does such a proof that PA is consistent (using ZFC) guarantees that there will never be a statement $\phi$ (stated in PA) such that it is impossible for $\phi$ and $\neg \phi$ to be theorems in PA?

@ManuelAraújo I appreciate for your explanation for strict $2$-category in your paper! Now I'm worried.. I thought the problem would go away once we prove the essential uniqueness for strict $2$-cats. However, you had to prove it for strict $3$-cats (in the same paper), and Riehl-Veriy had to prove it for $qCat_\infty$ (mathoverflow.net/questions/231867/uniqueness-of-infty-adjoints). Who had prove this for general $(\infty,n)$-cats, or at least for the cobordism categories $Cob_n$? Any reference? Or is it something that is accepted by folklore without a careful proof?

@ManuelAraújo I would love to have a reference or a complete proof for this! In particular, in for a strict category, the space of the triples $(g,u,c)$ should be a single point, right? I couldn't prove this even for the most classical case, i.e. when $f$ is a functor between two categories.

This is very useful in TFT because a priori adjoint functors are hard to compute explicitly. And passing to $Prof$ makes it easier. The problem is, in the end, how do we pass back to $Func$?

I finally understood this answer, after seeing very similar things in Bartlett et al's Modular categories as representations of the 3-dimensional bordism 2-category, section 2. There, they work for categories enriched over Vect. So I'd say the trick here is by viewing $F: C \to D$ as a profunctor $F^{formal}: C \nrightarrow D$ in $Prof$, whose right adjoint is simply $G^{formal}: D \nrightarrow C$. And the desired $G$ exists iff $G^{formal}$ is co-representable.

It took me a while to understand this answer, and wow it's good! (1) I wonder, is $U^G: C^{T^G} \to C$ also initial among functors to $C$ that admit left adjoints? (I know what 'monadic' means here, but I don't feel natural to consider the initial object among monadic functors to $C$; partly because I don't understand why we should consider only the monadic ones.) (2) (How) Does your answer fit into Mike Shulman's?

This has been inspiring me over the past few days. Some older papers are difficult to find. A modern account is given in sec 1.3 of Lux and Pahlings' Representations of Groups. There, two basic variants were given. The meataxe based on Norton's irreducibility criterion only works for finite fields. A workaround is the Holt-Rees algorithm. However, one step of the later requires factorizing single-variable polynomials over the field, which no definite algorithm solves. Over the integer ring $Z$, check Parker's paper on The Integral Meataxe.

The link to Max Neunhoffer's note from @TimDokchitser is broken. I suppose this link brings to a similar document math.rwth-aachen.de/homes/Max.Neunhoeffer/Publications/pdf/…

Thanks for pointing out that I need "algebraic closeness"; edited. And I appreciate your results on $k[G]$-modules. Are there general techniques? Or it is so elusive that we must focus on special case?