Simple example of an explicit Henkin sentence?

Question

I came across the concept of explicit Henkin sentences in a discussion of Gödel sentences, but I'm unable to find a concrete example of an explicit Henkin sentence

Answer 1

First, some background. Recall that the Goedel sentence asserts its own unprovability. We could also ask about sentences which assert their own provability, a much weirder situation. While Kreisel showed that the situation is more complicated for "pathological" provability predicates, Lob's theorem famously states that (among other things) every sentence expressing its own provability in a "reasonable" way is in fact provable! And such sentences are called Henkin sentences.

So a Henkin sentence asserts its own provability. An explicit Henkin sentence goes one step further: it tells you how it is proved.

The formal definition of an explicit Henkin sentence is as follows: an explicit Henkin sentence is one of the form "$t$ is a proof of me," where $t$ is some closed primitive recursive term.

For example, the following is an explicit Henkin sentence:

$0$ is the Goedel number of a proof of this sentence.

This is false, and easily disprovable, since $0$ isn't the Goedel number of any proof. So explicit Henkin sentences are meaningfully different from Henkin sentences.

OK, what about true (indeed, provable) explicit Henkin sentences? It's not at all clear that these exist, but it turns out that they do; and this was proved by Solovay. The proof is short, but uses a standard diagonal lemma approach, and such arguments provide very very messy example sentences (although they do provide examples when appropriately unwound - they are constructive, just not efficiently so). So if you ask, "What's a simple example of a true explicit Henkin sentence?", then Solovay's proof does not provide a satisfying answer, and indeed I'm not aware of any simple example.