> Showing it’s not provable, on the other hand, is more difficult. He did this with a proof by contradiction: He began with the assumption that he could prove his theorem in ZFC, and then constructed from it a system of objects in which ZFC holds. Which means that if his theorem holds true, then ZFC is consistent—and, transitively, that ZFC has proven its own consistency. But by Gödel’s incompleteness theorem, that cannot possibly be the case. And so, the theorem cannot be proven in ZFC. He’s working to extend the theory to other types of symmetries, other definitions of “maximal,” and other types of objects.
So he encoded some statements about ZFC into these statements about sets of rationals. Wasn't Gödel was able to do better already, encoding statements about ZFC into basic arithmetic/number theory? I guess I just don't understand what the big breakthrough is supposed to be, even though I'm interested in alternate axiom systems (e.g. the whole homotopy type theory / univalent foundations business). Is the idea that he's come up with some new natural statements about symmetries of sets that turn out to demonstrate incompleteness? That would be an innovation, but the above description makes it sounds like it's more about finding symmetry statements that correspond to ZFC.