[FOM] Inconsistency of Inaccessibility

[Andrej Bauer]

On Tue, Oct 25, 2011 at 3:09 PM,  <MartDowd at aol.com> wrote:
> Existence of inaccessible cardinals seems consistent.  They have appeared in
> logic, in settings such as Grothendieck universes, monster sets, etc.  Most
> mathematicians would probably agree that consistency holds.

You may add to the list the fact that in type theory universes, which
are the type-theoretic analogue of inaccessible cardinals, are
routinely used and not considered problematic at all. In fact, proof
assistants such as Coq use type universes, so at least some computer
scientists can be counted as consumers of inaccessible cardinals. That
is putting a lot of trust into inaccessibles, as some of these tools
are used to verify safety of large systems (think Paris metro).

With kind regards,

Andrej