On: Kurt Gödel and the Mechanization of Mathematics

[bjornsing]

What does that mean though?

Does it only mean that ZFC is consistent when subsumed within a strongly-typed higher order theory, or does it mean that ZFC by itself is consistent?

[ProfHewitt → bjornsing]

The strongly-typed higher-order theory Ordinals is consistent because it has a unique up to isomorphism model by a unique isomorphism. Consequently, ZFC is consistent because it is a special case of the theory Ordinals.

[petters → bjornsing]

That ZFC by itself is consistent, i.e. you can't find a contradiction.