How relevant this is to "an abstract framework, maybe a certain kind of formal language with some extra structure" in the OP, I am not quite sure, and I am only beginning to read Halbach's works, yet I think they are general enough to properly belong to this thread, and they weren't yet mentioned. Very very roughly, what I gather from Halbach's work on this topic so far is that (my interpretation)
the 'say' in the old idea of formulae which 'say' about themselves they are not provable is not an idea which is synthetic a priori (like e.g. the idea of necessity), rather is an idea consisting of many sub-ideas. (For example, by filtering according to where the relevant formulae are placed in the arithmetical hierarchy.)
Philosophically, the approach to self-reference I am pointing to here could be called an 'analytic' approach to self-reference, as opposed to the 'synthetic' approach of Lawvere. (Both 'analytic' and 'synthetic' to be taken in their neutral technical sense, i.e. breaking a concept into parts in the former, combining the concept with other concepts in the latter.)
Some references on Halbach's work:
so new that it hasn't yet appeared: Volker Halbach has announced a book (with Graham Leigh) whose draft has the title Syntax and Circularity: A Study in Self-Reference and Paradox.
so new that it lies after the answers given so far:
Volker Halbach, Albert Visser: Self-reference in arithmetic I. Vol. 7(4), 2014 , pp. 671-691
Volker Halbach, Albert Visser: Self-reference in arithmetic II. Vol. 7(4), 2014 , pp. 692-712
- a relevant lecture of Halbach's with a very general title, containing explanations on the work of Halbach and Visser:
