Logic has proposed and clarified various forms of circularity.
Among them one may recall: non-well-founded sets, self-application and
recursive definitions of functions and types, impredicative definitions.
They may be understood in a unified manner, as "mathematical closure properties"
of suitable domains of interpretation. In Type Theory, an analysis
of universal second-order (impredicative) propositions may be developped
in terms of "prototype proofs and generic arguments", as a fall out of
the Genericity Theorem for Girard's system F (papers downloadable from