I've drawn out my understanding of these below, in the hope that some thoughts that may be helpful. (Fwiw tracking in this level of detail is not yet easy for me! But I think I have made a good attempt.)

I think the basic thing to say is that self-reference is (generally) not a provided primitive! So anything anyone does that looks like self-reference is actually a construction that has to ground out in a finite and fully-unrolled sentence.

Here are my full thoughts though, others will hopefully correct me if anything I'm saying is misleading:

• As you've sketched, you can prove that for any and any (like "Santa exists"), , meaning: if there exists any claim that both implies and is implied by , then must be true and so is .
• That does mean that if you are working in a logical framework that lets you construct a sentence with this property, you would be in trouble!
• In almost-python, the "proof" looks like:
  def go[F, R](up: F -> (F -> R), down: (F -> R) -> F) -> R:
half: F -> R = lambda f: up(f)(f)
return half(down(half))
• (You may recognize this as a Y-combinator-y construction! If you invent some type F that's equal to F -> R , you can then pass in the identity function lambda f: f for up and down. Then go will build the resulting "R" by *checks notes* looping forever and never actually returning anything. Anyway.)
• But why can't you generally say , i.e. "I define to be "? One handle is that you don't actually start having a thing named "" to refer to until after you've defined it. Generally theories aren't in the business of letting you build graphs with loops, a sentence has to stand on its own feet when fully unrolled in order to obtain truth grounding.
• We could see the definition as being code or syntactic sugar that tries to describe a fully unrolled sentence. We often talk about sentences this way because it's easier to name things with let bindings and graphs. And that's confusing in exactly this case! But the difference is that this one loops when you go to unroll it, and doesn't actually name a valid finite sentence.
• There are ways you can get (working) self-reference within this constraint. One way is that you can think of as a property you would like to obtain at a fixed point, and define a series of increasingly-complicated/increasingly-deep sentences , and ask if there is a limiting value that reaches as gets arbitrarily high. In this case the kind of self-reference is akin to the flipping back-and-forth T=>F=>T=>F... if you set R to something false, so there's no fixed point to be had here.
• A different way you can build in self-reference (of sorts) is using quining. Quining lets you refer to the source code of inside itself, and can be made to work even in rather weak theories (via Godel numbering schemes). The source code on its own is not a "claim" though, so if wants to make a claim about its own source code you need something like an evaluator, where "" means the (encoded) source code for a sentence .
• (I'm weakest on this part, someone may correct me:) Tarski's undefinability of truth result says that consistent logical systems must not contain a general evaluator that corresponds to models of "truth" in the system, in a particular sense:
  • Looking on from outside the system, we pick a "model" that is some way to assign true/false to every sentence that is consistent with what the system can prove to be true and false. Call this our truth function .
  • There can be no general defined within the system that successfully claims for every sentence that "the sentence is true according to our outer model"; i.e. there is no satisfying for every that .
  • This means our model of the truth value of the sentence cannot always line up with our model of the truth value of the sentence , which we take to mean that no inner can define within-the-theory our outer .
• The reason Tarski's result holds is exactly that it lets you build the self-reference chain. Because can refer to its own source code via quining, you can pick an function that turns a sentence into a truth-claim then build . Tarski is forcing both our model and our inner to make a choice of true or false on everything, including on loopy content like this. And from either choice we derive a contradiction because this new quine-y would be equivalent to a loopy (and we can choose to get ).
• This doesn't rule out an that can work on source code that doesn't loop, or otherwise does something approximating but not fully reaching "outer truth".
• For instance a common use of is provability. You can describe the inference rules of a theory within itself, and this lets you perfectly-well construct sentences like "there exists a proof of the sentence within theory ".
• This means you can build sentences like , which says "this sentence is not provable in theory ". If you are using a concrete theory like PA or ZF then you can build a sentence which says "there are no proofs of me in PA/ZF", and the theory won't be able to prove this true or false on pain of loopy problems! But the theory can escape this by simply saying "I abstain from this one, you can't prove it either way".
• This means there are partial models of truth that can say "true/false/abstain" with an exactly-matching on the inside (that could also allowed to abstain, or could be allowed to return whatever it likes when we abstain on the outside). And provability is an example of this, where "abstain" on the outside means "we can't prove it true or false".
• As maybe a callback to , you aren't going to be able to define in a fully recursive fashion, because you would be referencing "" within the definition before it has been fully defined, which you can't do with these fully-unrolled sentences. But you can define an that refers to , which you could use to assign truth to everything that halts in some finite number of steps (like "is there some depth after which no longer abstains").
• (Relatedly you can write things like "there exists some length of proof where each of the steps is valid and concludes ", and that's how you get the provability one.)

I hope that's helpful!