8
$\begingroup$

I asked this question on MathOverflow a few months ago, but received no answers.

There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them, it may be unsettling that Mizar assumes infinitely many inaccessibles, and that Lean's dependent type theory makes a similar tacit assumption. Basically, this is because they appeal to Grothendieck universes.

Now, there is an alternative: Feferman's universes. (For a brief explanation of Feferman's universes, see pages 24–25 of Mike Shulman's paper, Set theory for category theory.) Feferman's universes achieve most of what a "practicing mathematician" wants from Grothendieck's universes, but has the advantage of being conservative over ZFC. So here's my question:

Suppose we wanted a proof assistant to avoid going beyond the consistency strength of ZFC, while retaining essentially all the functionality of something like Mizar or Lean. Could this be done using the Feferman-universe idea? How difficult would this be to implement and what would be the tradeoffs?

I see that there is a somewhat related question here on the Proof Assistants Stack Exchange, Alternatives to universe levels, but as of this writing, that question has no answers either.

Improve this question
$\endgroup$
14
  • $\begingroup$ I don’t know about Fereman’s universes, but you might want to look into the consistency strength of Isabelle/ZF and Metamath/set.mm (although I think the later uses universes). Also, if you just want a foundations commonly used in proof assistants but not stonger than ZFC, then IIRC Isabelle/HOL and HOL-Light both have a lower consistency strength than ZFC, but are very capable and practical theorem provers. $\endgroup$
    – Jason Rute
    Commented Jun 25, 2023 at 22:15
  • $\begingroup$ Can you explain the motivation for your question? What would be gained from having such a proof assistant? $\endgroup$
    – Andrej Bauer
    Commented Jun 26, 2023 at 23:10
  • $\begingroup$ @AndrejBauer I'm looking ahead to a future in which I hope more "working mathematicians" will use proof assistants, either directly (by coding up their own results) or indirectly (trusting proof assistants to vouchsafe the correctness of mathematical arguments). My anecdotal impression is that the use of universes, in one form or another, is becoming increasingly common in areas such as homotopy theory, algebraic geometry, and related areas. If and when these arguments are formalized, what will the implementation look like? $\endgroup$
    – Timothy Chow
    Commented Jun 27, 2023 at 1:09
  • 1
    $\begingroup$ Feferman's trick won't work because the Feferman universe $V_\theta$ doesn't know that it's a model of ZFC. In fact, Feferman's compactness argument gives a non-standard model where $V \models \lnot(V_\theta \models \text{ZFC})$. $\endgroup$
    – François G. Dorais
    Commented Jun 27, 2023 at 1:10
  • $\begingroup$ (continued) I'm guessing that, as things stand now, the formalizations will go beyond ZFC, because that is the most straightforward way to proceed. But the drawback is that some mathematicians will be unhappy with proofs that go beyond ZFC. I'm wondering if Feferman universes will allow informal arguments that use universes to be formalized more easily in a way that stays inside ZFC. $\endgroup$
    – Timothy Chow
    Commented Jun 27, 2023 at 1:12

1 Answer 1

Reset to default
4
$\begingroup$

The concrete suggestion you make, namely to use ZFC/S, is quite difficult to appraise. The only way to answer it is to actually try formalizing mathematics in it. One possibility is for you (or your students) to do it. Perhaps the fastest way to achieve something is to take Isabelle/ZF and modify it to support ZFC/S. Good luck!

However, I think the question should be read in a wider sense: what should be used by people who want to stay low on consistency strength? I am aware of two possibilities:

  • In Isabelle land:

    • Isabelle FOL and ZF ought to have the power of ZF, precisely.

    • Isabelle/HOL has a huge library of formalized proofs based on classical higher-order logic. The consistency strength of HOL is quite low, and certainly below ZFC ($V_{\omega + \omega}$ models it).

  • You can use Metamath, see the Metamath Proof Explorer which contains over 23000 proofs based on ZFC.

There is a second sense to the question: must we reach for high consistency strength in order to use universes in practice?

I suspect, but cannot confirm, that in practice most uses of universes are "administrative" in the sense that they just serve as an organizing mechanism (a bit like having second-order logic without comprehension, or classes over ZFC), and not to boost the deductive power of the proof assistant. This leads to the question: are there formulations of type theory with universes which are "tame"?

Improve this answer
$\endgroup$
7
  • $\begingroup$ I think Metamath (the set.mm library) uses universes, at least according to Wikipedia: en.m.wikipedia.org/wiki/Tarski-Grothendieck_set_theory $\endgroup$
    – Jason Rute
    Commented Jun 28, 2023 at 16:31
  • $\begingroup$ They do introduce the Tarski-Grothendieck axiom, but I am not sure whether it gets used anywhere. For instance, the category of categories is parametrized by a universe, so it does not rely on there being any universes. $\endgroup$
    – Andrej Bauer
    Commented Jun 28, 2023 at 17:28
  • $\begingroup$ Here is where it is introduced. I don’t know if it is used much. It is easy check check for each theorem which axioms are used. $\endgroup$
    – Jason Rute
    Commented Jun 28, 2023 at 18:18
  • $\begingroup$ Actually, I just clicked through all the downstream dependencies, and there are only a handful of logical theorems. So maybe the library is basically only ZFC? $\endgroup$
    – Jason Rute
    Commented Jun 28, 2023 at 18:25
  • $\begingroup$ Thanks for this answer. Regarding the "administrative" use of universes, that is precisely the issue that prompted this question. If you have not already done so, I recommend reading Peter Scholze's answer to an MO question, which I linked to in my question. It is long but it explains why he thinks that Feferman universes are more suitable than Grothendieck universes if one is concerned about consistency strength. $\endgroup$
    – Timothy Chow
    Commented Jun 29, 2023 at 0:13

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.