10

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.)

Timothy Chow
  • 78,129
  • 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. – Hanul Jeon Dec 29 '22 at 16:37
  • 3
    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: https://mathoverflow.net/questions/380539/are-we-sure-the-calculus-of-inductive-constructions-and-zfc-plus-countably-many/418133#418133 – François G. Dorais Dec 29 '22 at 16:46
  • 2
    Perhaps a short reminder of what a "Feferman universe" is, would be in order? – Sam Sanders Dec 29 '22 at 19:41
  • 1
    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. – Timothy Chow Dec 29 '22 at 22:30
  • 1
    @Tymothy Chow Maybe you should also mention the 2004 paper of Feferman Typical Ambiguity: Trying to Have Your Cake and Eat it too. There he describes $ZFC/U_{<\omega}$ which seems more advanced than 1969 $ZFC/s$. – Victor Makarov Aug 28 '23 at 17:09

0 Answers0