Has there been any serious attempt at a "circular" foundation of mathematics?

Question

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:

1. No axiom is irrelevant, because it is math itself which decides what theory will be the background of another theory.
2. 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.

Answer 1

This is not exactly an answer, but the name I think of here is Jon Barwise. He has a book with Moss, called Vicious Circles, which uses non-well founded set theory (following Peter Aczel) not only to discuss foundations but serious applications to things like computer science and fixed point theorems.

Maybe more relevant to the foundational questions would be his book Admissible Sets and Structures, which starts off by developing a weak (non-well founded, but in a different way) set theory called "Kripke-Platek" as a tool to study definability and infinitary logics.

A final comment: this answer doesn't directly talk about homotopy type theory or univalence. Much of Barwise's work involves applying non-well founded ideas to understand second-order set theory. Once you remember the 'point' of set theory is to write all these different kinds of mathematics within the same first-order theory, the fact that second-order set theory is a thing might be kind of.... hrm. My point is, you can insist on categorical terminology, but already at the 'set level' so to speak, this question is pretty interesting.

Best

Answer 2

As you say the question is nebulous as it stands, so I'm going to attempt a formalization of what you're talking about to make it precise.

We proceed by recursion, so the metatheory we're carrying this whole process out in should be strong enough to support recursion of the appropriate length. It's not clear to me how you intended to proceed at limit steps, as the process you describe is between successor stages of the recursion, but here is one possibility.

For a theory $T$, let $C(T)$ denote the category whose internal logic corresponds to $T$ through syntax-semantics duality, and $Th(C(T))$ the definition of this ambient category viewed as a theory. We then define

$$T_0=\text{your favorite theory},$$ $$T_{\alpha+1}=Th(C(T_\alpha)),$$ $$T_\lambda=Th(\coprod_{\alpha<\lambda}C(T_\alpha)),$$

Note that truth in $T_\alpha$ is definable in $T_{\alpha+1}$. Assume that there exists some ordinal $\alpha$ such that $$C(T_\beta)\simeq C(T_\alpha)$$ for all $\beta\geq\alpha$. Then the internal logics of all these categories will be 'the same', so anything definable in the corresponding theories will be definable in $T_\alpha$. In particular $T_\alpha$ can define truth within itself and thusly must not be strong enough to define arithmetic, or we get a paradox via Tarski.

As mentioned at the outset this is just one possibility for formalizing what you're talking about, and this one can only be used on base theories $T_0$ weaker than Peano arithmetic, and the existence of such an $\alpha$ is simply assumed here. I can't see how you would get around the issue with definability of truth at the moment, but there are people more knowledgable on these subjects here who might see something more clever. From the comments, it looks like Tim Campion might have something cooler in mind if you can offer a more precise formulation of the question.