As far as I know, there is no published attempt at a "circular" foundations of mathematics though I'ave seen it noted by many category theorists and logicians without in-depth analysis, e.g Notes on predicate logic. The current and past attempts at foundations of math seem to be about choosing the right axiomatic schema and universes in which math can be formalized. Notable examples include set theory-ZFC, homotopy type theory/Univalent foundations-HoTT and $\infty$-categories.

I will try to explain what I mean by circular foundations. By the syntax-semantics duality, every theory corresponds to the internal logic of some category which acts as the model. The category itself has a definition which serves as the metatheory, with a new model, it's metamodel. This process seems to be an infinite regress which may converge on itself forming a loop of meta-theories. This means that any foundations of math based on axiom schemas should be subject to such circularity or at least regression. A circular foundation seems to have 'uncommon' consequences, which by stating them I hope will help give a deeper understanding into the question:

- No axiom is irrelevant, because it is math itself which decides what theory will be the background of another theory.
- Math maybe quasi-empirical, because by being 'self-delimiting' it is independent of mathematicians whose work then should be only to observe it unfold. That is, self-reference may imply the objective reality of math.

Have such claims been considered in-depth ?

**Edit :** This is my attempt to have a precise formulation of "circularity"(I may be wrong)

Let $\mathfrak C$$_H$ and $\mathfrak C$$^H$ be the kleisli and eilenberg-moore categories on some monad * H* respectively. Then the syntax-semantics duality is between a term algebra $\mathfrak C$$_H$ and its model $\mathfrak C$$^H$. I propose that a syntax-semantics duality is a lifting of the corresponding meta-syntax-semantics duality between the metatheory and metamodel with this forming an algebraic square as defined here. Then by monadic decomposition, iterated lifting should converge forming an 'infinite regress' of metatheories. I interpret the two different possibilities of Kleisli lifting and Eilenberg-moore lifting as the concept of "meta" and its dual.

syntax. This is quite finitary, and the metatheory for this is surely rather weak. $\endgroup$7more comments