# Set-theoretical foundations of Mathematics with only bounded quantifiers

It seems that outside of researchers in Mathematical Logic, mathematicians use almost exclusively bounded quantifiers instead of unbounded quantifiers. In fact, I haven't observed any other practice from the very first day on when I was a student.

For example, a logician would write

$$\forall a : ( a \in \mathbb R ) \rightarrow ( a^2 \geq 0 )$$

whereas most working analysists and algebraists write

$$\forall a \in \mathbb R : a^2 \geq 0$$

On the other hand, most mathematicians I know accept the idea that all of mathematics can be built up from set-theoretical foundations alone (starting the natural numbers).

So there seems to be a set of assumptions, almost universally agreed upon, which most working mathematicians assume implicitly for their practice. These assumptions start with set theory but apparently exclude unbounded quantifiers. In fact, unless you attend a class in formal logic you might never encounter unbounded quantifiers.

It seems that most mathematicians use a subset of human language enhanced with a subset of mathematical language (avoiding universal quantifiers) as their working language.

Question: Have there been attempts at precisely identifying this mathematical sublanguage and the rules that it governs?

• There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write. Apr 8, 2019 at 5:27
• There is no logical difference between the above two expressions. Unbounded quantification is simply defined as quantification bounded by the class of all sets $V$. Apr 8, 2019 at 9:04
• I think one keyword for this question might be predicative. Apr 8, 2019 at 9:47
• @AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification. Apr 8, 2019 at 11:45
• I just couldn't help myself. Apr 8, 2019 at 13:40

The most ambitious (and well-argued) attempt at formulating a set-theoretical foundation of the type you are proposing using bounded quantification has been suggested by non other than Saunders Mac Lane in the last chapter of his book Mathematics, Form and Function.

Mac Lane dubbed his system ZBQC, which can be described as a weakening of Zermelo set theory in which the scheme of separation is limited to formulae with bounded quantification. Curiously, at the level of consistency strength, ZBQC is the only known lower bound to the consistency strength of Quine's system NF; moreover, it is known that that the urelement-version, NFU, of NF (in which the axiom of infinity is included) is equiconsistent with ZBQC.

On the other hand, Adrian Mathias has critically-and-forcefully responded to Mac Lane's thesis to found mathematics on ZBQC; see here for an article of his addressed to philosophers and general mathematicians, together with a response from Mac Lane; and here for an article addressed to logicians.

• I"m not sure what "(weak) upper bound" means, but I'd understand "ZBQC is an upper bound to the consistency strength of NF" to mean that Con(ZBQC) implies Con(NF). Did you mean the converse of that? Apr 8, 2019 at 1:15
• @AndreasBlass I will change the wording to make it more clear, I put the parenthetical "weak" to distinguish it from "strict", and as you suspected, "upper bound" should have been "lower bound". Apr 8, 2019 at 9:38
• The conclusion of Randall Holmes’s purported proof of consistency of NF (arxiv.org/abs/1503.01406) suggests that it has the consistency strength of ZBQC, so the lower bound may actually be tight. Apr 8, 2019 at 14:30
• If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell. Apr 8, 2019 at 18:55
• Does bounded ZFC (i.e. with both separation and replacement limited to bounded formula) prove consistency of ZC (with unbounded separation but no replacement)? Sep 7, 2021 at 17:04

Most mathematics can be done in logical systems which are far weaker than Zermelo-Fraenkel set theory. For example, something like structural set theory will suffice for a great deal of ordinary mathematics.

It's not exactly true that mathematicians never use unbounded quantification. For example, in category theory universal properties quantify over all objects of a category. When the category in question is large this amounts to unbounded quantification. In a sense, such quantification is "harmless" because it is "on the outside", i.e., it is of the form $$\forall X . \phi(X)$$ where $$\phi$$ itself contains no further unbounded quantifiers. In many cases we can replace such a statement with a schema $$\phi(X)$$ where $$X$$ is a schematic symbol (that is, instead of having a single formula $$\forall X . \phi(X)$$ we have many separate formulas $$\phi(X)$$, one for each $$X$$).

Occasionally one sees mathematical statements which do contain inner unbounded quantifiers, but those are not common. One example I can think of is the following. The notion of epimorphism in a category requires quantification over all objects: a morphism $$f : A \to B$$ is epi when for all all $$C$$ (unbounded quantifier!) and $$g, h : B \to C$$, if $$g \circ f = h \circ f$$ then $$g = h$$. Often in concrete example we can characterize epis equivalently with some statement that only contains bounded quantifiers (e.g., in the category of sets a map is epi if, and only if it is surjective), but if we make general statements about epis in large categories, large quantification will be required.

• @Pedro: Yes; a standard statement like “If a category C has all products and equalisers, then it has all limits.” (Though again the most-unbounded quantifier is on the outside.) Apr 8, 2019 at 11:41
• @MonroeEskew: I am not sure I get your point. Those are just more examples of the "easy" unbounded quantifier $\forall$ on the outside, like universal properties in category theory. The inner $\exists$ can easily be made bounded. Can you think of statements where the inner quantifiers cannot be made bounded easily? Apr 8, 2019 at 14:06
• @MonroeEskew: let us not confuse a particular first-order set-theoretic language based on $\in$-relation with mathematical practice. It is quite natural to have a langauge in which the powerset (and other basic set-theoretic operations) are primitive function symbols. So yes, we need to fix a language, but let us fix something that looks like mathematical practice. Apr 8, 2019 at 17:41
• @Monroe: The point that these examples are $\Pi_1$ is important, but I read it with a very different informal interpretation than you do: I see such examples as illustrating that the informal concept the Lévy hierarchy formalises is not really quite “unbounded quantification”, but something more like “higher-order quantification”. And it’s worth appreciating that ZFC and its choice of language is not the only foundational system; there are systems where products genuinely require unbounded quantification, and systems where power-objects do not. Apr 8, 2019 at 18:51
• I apologize, I've been stuck at home with a fever which seems to be getting the better of me. But please, do try to understand other people's points of view, even if they're not just set theory. Apr 8, 2019 at 23:08