I will talk about the strange apparent gap between the actual working Mathematics and its foundations as provided by Zermelo-Fraenkel Set Theory. This slide lists my talk's sections. I will, of course, only summarize the points, but I will repeat at the last slide the above link where you can see more details.
Cantor reduced all that variety of objects to just one type - sets, all their relations to just one - membership, and all assumptions about them to one family of Cantor Axioms: For each property it postulates a set of those sets that satisfy it.
The euphoria that followed was short-lived: Bertrand Russell killed it by formalizing the Barber Paradox. It is based on the self-referential aspect of set theory properties that use quantifiers over sets. All properties define sets, so quantifiers in properties really include properties themselves in their domain.
Zermelo and Fraenkel proposed a remedy based on Cantor's concept of cardinality. They restricted Cantor's Axioms to preserving cardinality bounds, and allowed only a single tool - Power Set axiom to increase them. This sounds a bit ad-hoc as a foundation for the mathematics as a whole. Yet, so far it has prevented the appearance of any contradictions.
The focus on cardinality seems a bit foreign to mathematics. Have you seen many (or for that matter, any) math papers that looked at distinctions between uncountable cardinalities ? Those are almost never looked at in math papers. Besides, all consistent axiom systems have countable models. Cardinalities feel like an artifact, designed to hide some self-referential aspects.
And there is something exotic for mathematics in the Power Set axiom. Usual mathematics sets have special types: countable, compact, open, occasionally Borel, rarely projective, etc. Generic subsets from Power Set classes, with no other descriptions, find little use in mathematics
[ Admittedly, the sets provided by rarely used axiom of Choice may pose an issue here. But even they can be, with some stretch, looked at as internally specified - by adding to the language a notation for (named, treated as canonical, but not described) injection of reals into ordinals. Bourbaki books used a similar trick with tau symbol. ]
Zermelo-Fraenkel's ad-hoc cardinality-based restrictions diffused fatal consistency problems of Cantor's Axioms. But they left intact their self-referential root. Seems just an example of uncoiling a vicious circle into a vicious spiral. The result was a Babel Tower of cardinalities, types, and other hierarchies finding little relevance in mathematics.
And the generality of this height of hierarchies is illusory. Expanding Set Theory with more formula types, axioms, etc. has no natural limit. Benefits are few and eventual consistency loss inevitable. (There is more to this, but no room for that in this talk.)
This does concern the Logicians. A popular topic in Logic is to isolate math segments where more ingenious proofs can replace the use of Power Set Axiom and its uncountable sets. But such assault on the unity of Mathematics raises many hackles. And mathematicians are aghast at losing simplicity and elegance of their proofs.
Now, some radicals always questioned the need and validity of using any infinite objects in mathematics at all. But these ideas gained little sympathy. Infinities are neat. Zero is a great simplifying approximation for negligible quantities. And so is infinity for their inverses. The transparency they add to many considerations allow powerful insights into methods that otherwise would be obscured by irrelevant complications. And handling (often ambiguous) termination points of finite objects is awkward.
Besides, look at infinitely tailed reals versus finitely long rationals on a segment. The segment of reals is compact. In that it has more similarities with finite domains than the same segment of rationals.
The really useful math properties go to very limited heights. Yet, provisions for open-ended hierarchies are motivated by the perceived need to handle objects that are not defined by readily envisioned properties. Indeed, mathematics needs to handle objects that are not defined by any mathematical properties at all. For instance, random sequences.
But there is no reason for such externals to bring any self-referential issues. Those issues come from math properties over variables whose domains include objects defined by properties themselves. This need not be the case with variables covering only external objects, unrelated to math properties. Externals may be chaotic, but not really tricky.
Keeping a clear distinction between external and internal objects allows to face challenges of each type separately without confusions of fighting on two fronts. Of course, mathematics would deal with objects that mix both types: classes defined by properties that refer to external objects as parameters. But only these parameters, not the properties themselves, would be subject to quantifiers.
Such a mix adds no extra self-referential aspects to math properties. But to see how these mixed objects can avoid saddling mathematics with messy irrelevant hierarchies, we need to get more technical.
Parameters may have not only infinite size (like, say, the number $\pi$), but also infinite complexity. Could not that infinite complexity be a backdoor for formula-related self-referentials ?
It is redundant for formulas to use in their parameters information from formulas themselves. This would not increase their expressive power. Besides, how could external parameters acquire infinite uncomputable information about formula-defined classes ? Yet, seeing no need or no realistic mechanisms for such occurrences is not the same as ruling them out.
Here the Algorithmic Information theory comes to the rescue. It provides a family of axioms postulating independence of external parameters (that is, values of variables) from formula-defined classes. This postulate has a number of other interesting applications, too.
It is justified by Independence Conservation Inequalities. They state that no algorithmic or random processes, or any of their combinations, can increase the amount of algorithmic information their inputs have about any specific sequence, such as one defined by a formula. This, for any formula-defined object, justifies a postulate that physically realizable sequences, even having potentially infinite complexity, hold only finite (small really) information about that object.
This powerful postulate opens a way to reduce any set theory sentence to one with only integer quantifiers. All with seemingly no need to change almost anything in mathematical papers, only to reinterpret some formalities.
A bit-sequence is random under uniform distribution if no prefixes of it have complexity significantly smaller than their length. Their largest difference is called Deficiency of Randomness, or Rarity. If it is finite, the sequence is called random.
Two random sequences are independent if their combination is random, too. By Gacs-Kucera theorem, any sequence can be algorithmically generated from a random one. Sequences that may not be random are still independent, if generated separately from the respective sides of an independent random pair. The minimal Rarity of such a pair is the degree of Dependence, or the Amount of Mutual Information in the generated pair.
It would be redundant anyway for formulas to duplicate formula-related information in their external parameters. But the "physical meaning" of the Postulate is justified by the Independence Conservation Inequalities mentioned earlier.
Note that there are sequences that are both generatable (thus legitimate externals) and definable by formulas. But the Postulate requires them to be computable, otherwise they would have infinite information about themselves.
What does all this give us? Many sets, for instance linear spaces, would then be interpreted as classes, specified by formulas with parameters. The formula defines the membership relation on the transitive closure of the class. It is expressed as a relation between parameters that specify the classes in that closure. The parameters are externals -- hereditary countable sets, respecting the Independence Postulate. Quantifiers bind only parameters, not formulas.
Papers may have families of theorems parameterized by formulas. Such are used now for the so called Large Categories that are not Zermelo-Fraenkel sets. They are also used for families of axioms, like Induction axioms. We may treat such families as meta-mathematical statements. Alternatively, one may allow variables for formulas but not quantifiers on them, except for an implicit universal quantifier over all free variables in a sentence.
But the reverse does not follow from the Independence Postulate. So, it needs support from more axioms. One is the Primal Chaos axiom. It says "Each sequence reduces to even-indexed digits of some random sequence." For classes (that is, in classical set theory) this axiom is the famous Gacs-Kucera theorem. I did hope that adding this theorem as an axiom is all we need. But we will soon see some complications here.
Note, by the way, that a random sequence respects the Independence Postulate if and only if it is GENERIC, meaning that it is outside of all arithmetic classes of measure zero. So, for outsiders to Complexity Theory, random sequences may be more intuitive to so handle. (And all sequences reduce to random ones.)
A countable model has a reduction basis: that is, a chain of sequences each computable from the next one, and all sequences in the model computable from them. By the axioms discussed, each of them reduces to a generic sequence (and can be taken Turing equivalent to them).
We can represent such basis as a set of trims of a combined sequence gamma. Trims are obtained by dropping a fraction of its digits, say, those indexed by a given power of 2: dropping every second digit, or every fourth, eighth, etc.
Call such models internal if gamma is generic itself. They respect a family of axioms that do eliminate all non-integer quantifiers. These axioms, for almost every sequence gamma, assert equivalence of each closed formula to its modification that replaces all second order variables by algorithms computing those sequences from trims of that gamma.
The obstacle comes from strange objects -- Recursively One-Way Functions. They were discovered by George Barmpalias, Peter Gacs, and Xiaoyan Zhang. Such functions are computable, preserve probability distribution, but have zero chance to be inverted, meaning to find an input that generates a given random output. So, existence of sequences with a given property does not immediately follow from their positive measure conditioned on a given output reducing to them. For now, minimizing axioms to a more elegant and intuitive set is still an open problem.
Some proposals, such as Reverse Mathematics, replace the Power Set axiom in some segments of mathematics with more elaborate proofs. But this breaks the unity of mathematics which is a high price to pay. I blame the problems on the blurred distinction between internal objects, defined by mathematical properties, and external ones in the domain of the variables.
Allowing quantifiers to bind mathematical properties, even indirectly through sets they define, does extend the reach of Set Theory. But such extensions have no natural limit. Climbing ever higher in that direction finds little relevance to mainstream mathematics.
Now, my way to handle these issues.
I advocate separating in mathematical objects their aspects defined by formulas from aspects brought by external parameters. This allows the exclusion of formula-related information from parameters that are "bindable" by quantifiers.
Complexity theory allows us to formalize that, justify the validity for "external data", and use that for a great simplification of foundations.
This drastic simplification seems to have little effect on typical math papers, it only reinterprets some their formalities. But what is left out are "logics" sets, related to infinite hierarchies of formulas, such as "The set of all true sentences of Arithmetic". Those should be a subject of math foundations. And theories cannot include their own foundations.
The Independence Postulate has other powerful applications. They are unrelated to set theory, so I will only briefly mention a couple.
Many paradoxes in application of Probability Theory led Kolmogorov and Martin-Lof to introduce the concept of Randomness. The Independence Postulate clarifies its use: Namely: Any set of sequences has measure zero if and only if all its random sequences have infinite information about some common sequence.
The Independence Postulate also removes a subtle loophole in Goedel's Theorem. Goedel believed that informal arguments allow to circumvent that theorem. I quote him: "It is not at all excluded by the negative results mentioned earlier that nevertheless every clearly posed mathematical yes-or-no question is solvable in this way. For it is just this becoming evident of more and more new axioms on the basis of the meaning of the primitive notions that a machine cannot imitate."
But this hope of Godel's is quite impossible ! If a predicate extends the "proven/refuted" partial predicate of Peano Arithmetic to all statements of some length, then it has information about halting problem at least close to that length. Such information cannot be generated by any methods, not only by formal ones.
Many objects treated now as sets would be reinterpreted as classes, specified by formulas with parameters. (I guess people would still call them sets, but only informally.) The formula defines the membership relation on the transitive closure of the class. It is expressed as a relation between parameters that specify the classes in that closure.
What is formally called sets are the parameters representing the externals. They respect axioms that are modified from the classical system. ( The slide freely uses arithmetic concepts, assuming their expression in terms of membership is known. I did not attempt to find the most elegant expression. )
Quantifiers bind only parameters, not formulas. But some families of axioms may be parameterized by variable formulas, similarly to the Induction axioms in Peano Arithmetic. This may be viewed as extending to formula~variables the implicit universal quantifier on all free variables in a sentence.
So~parameterized will be the Foundation and Extensionality axioms, because they must apply to classes, not just sets.
Replacement axiom is restricted to only computable mappings. Its opposite, the Independence Postulate, is added. The Power Set, too, is replaced with its opposite: "All sets are countable." (Subsets would now form a class, not a set.) The Primal Chaos axiom is added. It is an open question if something stronger than it is needed. (At worst, it could be the family of Internal Models axioms.)
It is also an open issue of what to do with the axiom of Choice, It may be simply dropped. An alternative is adding to the language a postulated (thus, only named, not described) class that injectively maps reals into countable v.Neumann ordinals. This would also imply the Continuum Hypothesis. Thank you very much! And while this was very brief, the slide gives links for a more detailed account.