10
$\begingroup$

This question was prompted by a discussion from another MO question about the consistency of ZFC. 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 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?

(Maybe this question belongs on the proof assistants StackExchange, but that site seems to be more of a help desk for existing proof assistants than a forum for broader mathematical questions like this one.)

Improve this question
$\endgroup$
5
  • $\begingroup$ I am not an expert on type theory, but I know that universes in Martin-Löf Type Theory (MLTT) are given with finitely many (introduction and elimination) rules, and adding (a form of) extensionality with LEM to MLTT results in a theory whose strength is more or less similar to that of ZFC. That seems to mean Feferman's idea would not work under type-theoretic setups. $\endgroup$
    – Hanul Jeon
    Commented Dec 29, 2022 at 16:37
  • 3
    $\begingroup$ I monitor proof assistants on a regular basis. Enough people there are willing and able to answer theoretical questions, there's just too few people asking. Anyway, the Feferman trick already plays a role there but at the next level up, as I tried to explain here: mathoverflow.net/questions/380539/… $\endgroup$
    – François G. Dorais
    Commented Dec 29, 2022 at 16:46
  • 2
    $\begingroup$ Perhaps a short reminder of what a "Feferman universe" is, would be in order? $\endgroup$
    – Sam Sanders
    Commented Dec 29, 2022 at 19:41
  • 1
    $\begingroup$ Feferman's original paper is Set-theoretical foundations of category theory but I haven't found a non-paywalled link. Mike Shulman's paper Set theory for category theory contains a readable summary; see pages 24-25 in particular. $\endgroup$
    – Timothy Chow
    Commented Dec 29, 2022 at 22:30
  • 1
    $\begingroup$ @Tymothy Chow Maybe you should also mention the 2004 paper of Feferman <a href="math.stanford.edu/~feferman/papers/Ambiguity.pdf"> Typical Ambiguity: Trying to Have Your Cake and Eat it too</a>. There he describes $ZFC/U_{<\omega}$ which seems more advanced than 1969 $ZFC/s$. $\endgroup$
    – Victor Makarov
    Commented Aug 28, 2023 at 17:09

0

Reset to default

You must log in to answer this question.