[FOM] Structural set theory for proof assistants

Timothy Y. Chow tchow at math.princeton.edu
Sat May 4 22:26:32 EDT 2019

Josh Chen wrote:

> Have structural set theories been considered as foundations for formal 
> *computer* mathematics before? Maybe some people who know the details of 
> these foundations, and have perhaps tried to work out some mathematics 
> in them, could comment on the prospects of such an undertaking? Even the 
> more recent developments in set-theoretic systems seem to mostly use 
> ZF(C), and I would like to know if this is a historical/cultural 
> accident, or if there is some deeper obstruction.

I don't keep up with all the latest developments, but I have not heard of 
anyone specifically using ETCS (or something like it) as the basis for a 
proof assistant.  But if indeed it hasn't been done, I doubt that there is 
any deep obstruction.  In fact, since ETCS has both type-theoretic and 
set-theoretic aspects, perhaps it can take advantage of the best of both 
worlds.  See also:



More information about the FOM mailing list