0
$\begingroup$

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.

$\endgroup$
12
  • 4
    $\begingroup$ If I'm not mistaken we can define truth in a theory using the meta-theory but not within the theory itself in (for example) ZFC, so if this theory->internal category->ambient category viewed as a model->definition of ambient category used as a theory->internal category->... tower converges to a theory (meaning it stabilizes up to equivalence or something), we would be able to define truth within the resulting theory and get a paradox, right? $\endgroup$
    – Alec Rhea
    Feb 10, 2021 at 15:25
  • 1
    $\begingroup$ I think a set theory like Quine's NF that admits a universal set should be included on your list of notable examples. $\endgroup$
    – Rob Arthan
    Feb 10, 2021 at 23:06
  • 4
    $\begingroup$ For people with a more formalist leaning, ultimately mathematics comes down to rules for manipulation of syntax. This is quite finitary, and the metatheory for this is surely rather weak. $\endgroup$
    – David Roberts
    Feb 11, 2021 at 2:09
  • 1
    $\begingroup$ In general, when studying logic, I think one usually conceptually separates the metatheory from the logical systems being studied as much as possible, precisely because, as Alec Rhea points out, paradoxes lurk when we do otherwise. But things like the reflection principle in ZFC can allow one to buck this trend to a certain extent (note that there are also other "reflection principles" which can be even more powerful). So I think I would appreciate a more precise and focused form of this question. $\endgroup$
    – Tim Campion
    Feb 11, 2021 at 14:03
  • 6
    $\begingroup$ By the way, "i.e." = "id est" = "in other words", what you're looking for is "e.g." = "exempli gratia" = "for example". $\endgroup$
    – Asaf Karagila
    Feb 11, 2021 at 18:11

2 Answers 2

4
$\begingroup$

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

$\endgroup$
4
  • 3
    $\begingroup$ For your first paragraph, I think you conflate non-founded set theory (which allows circular objects like Quine atoms) and that the OP asked. $\endgroup$
    – Hanul Jeon
    Feb 10, 2021 at 23:20
  • $\begingroup$ (Typo: I mean non-well-founded set theory, not just non-founded set theory. I add it as a new comment since I cannot edit it now.) $\endgroup$
    – Hanul Jeon
    Feb 10, 2021 at 23:30
  • $\begingroup$ I agree this is not exactly an answer to the question as asked. It’s a little long for a comment, and I thought the final paragraph addressed this a bit. The question itself is a bit vague and my answer does address the title question, so. To each their own I suppose. $\endgroup$
    – Ryan
    Feb 11, 2021 at 0:50
  • 2
    $\begingroup$ I was thinking of mentioning this book yesterday, but wasn't sure how relevant it might be, since my impression is that the book deals with circularity at the theory level whereas the question asks about circularity at the meta-theory level. However, the book is rather speculative and wide ranging, so maybe something in it could be relevant, but I don't know much about any of this. I got a copy of this book a year or two after it appeared, having read somewhere that monotone closure operators are discussed some, an occasional interest of mine. $\endgroup$ Feb 11, 2021 at 16:02
2
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ I think there might be a way to get around the family of diagonalization lemmas, if one views them as formalizable structure as well (say anti-reflection principle), they are just part of the tower which can be considered as (anti) (co) reflection principle. This way they are interpreted into a structure that models all their effects. $\endgroup$
    – Kori Peter
    Feb 18, 2021 at 15:10
  • 2
    $\begingroup$ @KoriPeter I suggest you try to formalize these notions yourself and see what you can come up with, it could be interesting. Also just a heads up that this question is one vote away from being closed as too vague/opinion based, so editing to add clarity or accepting an answer are likely going to be necessary to avoid your question being closed. $\endgroup$
    – Alec Rhea
    Feb 18, 2021 at 20:05
  • $\begingroup$ Sure, am still learning lots of things including how to ask questions the right way. I meant to question current philosophy on foundations so yea I should do it with pure facts not philosophy. Thanks for the eye-opener! $\endgroup$
    – Kori Peter
    Feb 20, 2021 at 14:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.