Set-theoretical foundations of Mathematics with only bounded quantifiers
$begingroup$
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?
set-theory lo.logic mathematical-philosophy
$endgroup$
add a comment |
$begingroup$
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?
set-theory lo.logic mathematical-philosophy
$endgroup$
1
$begingroup$
There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write.
$endgroup$
– Monroe Eskew
Apr 8 at 5:27
2
$begingroup$
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$.
$endgroup$
– Andrej Bauer
Apr 8 at 9:04
1
$begingroup$
I think one keyword for this question might be predicative.
$endgroup$
– Pedro Sánchez Terraf
Apr 8 at 9:47
2
$begingroup$
@AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification.
$endgroup$
– Monroe Eskew
Apr 8 at 11:45
1
$begingroup$
I just couldn't help myself.
$endgroup$
– Andrej Bauer
Apr 8 at 13:40
add a comment |
$begingroup$
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?
set-theory lo.logic mathematical-philosophy
$endgroup$
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?
set-theory lo.logic mathematical-philosophy
set-theory lo.logic mathematical-philosophy
asked Apr 7 at 16:40
shuhaloshuhalo
1,6791531
1,6791531
1
$begingroup$
There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write.
$endgroup$
– Monroe Eskew
Apr 8 at 5:27
2
$begingroup$
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$.
$endgroup$
– Andrej Bauer
Apr 8 at 9:04
1
$begingroup$
I think one keyword for this question might be predicative.
$endgroup$
– Pedro Sánchez Terraf
Apr 8 at 9:47
2
$begingroup$
@AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification.
$endgroup$
– Monroe Eskew
Apr 8 at 11:45
1
$begingroup$
I just couldn't help myself.
$endgroup$
– Andrej Bauer
Apr 8 at 13:40
add a comment |
1
$begingroup$
There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write.
$endgroup$
– Monroe Eskew
Apr 8 at 5:27
2
$begingroup$
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$.
$endgroup$
– Andrej Bauer
Apr 8 at 9:04
1
$begingroup$
I think one keyword for this question might be predicative.
$endgroup$
– Pedro Sánchez Terraf
Apr 8 at 9:47
2
$begingroup$
@AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification.
$endgroup$
– Monroe Eskew
Apr 8 at 11:45
1
$begingroup$
I just couldn't help myself.
$endgroup$
– Andrej Bauer
Apr 8 at 13:40
1
1
$begingroup$
There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write.
$endgroup$
– Monroe Eskew
Apr 8 at 5:27
$begingroup$
There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write.
$endgroup$
– Monroe Eskew
Apr 8 at 5:27
2
2
$begingroup$
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$.
$endgroup$
– Andrej Bauer
Apr 8 at 9:04
$begingroup$
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$.
$endgroup$
– Andrej Bauer
Apr 8 at 9:04
1
1
$begingroup$
I think one keyword for this question might be predicative.
$endgroup$
– Pedro Sánchez Terraf
Apr 8 at 9:47
$begingroup$
I think one keyword for this question might be predicative.
$endgroup$
– Pedro Sánchez Terraf
Apr 8 at 9:47
2
2
$begingroup$
@AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification.
$endgroup$
– Monroe Eskew
Apr 8 at 11:45
$begingroup$
@AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification.
$endgroup$
– Monroe Eskew
Apr 8 at 11:45
1
1
$begingroup$
I just couldn't help myself.
$endgroup$
– Andrej Bauer
Apr 8 at 13:40
$begingroup$
I just couldn't help myself.
$endgroup$
– Andrej Bauer
Apr 8 at 13:40
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
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.
$endgroup$
5
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
1
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
1
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
add a comment |
$begingroup$
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.
$endgroup$
1
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
1
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
3
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
1
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
2
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
|
show 11 more comments
Your Answer
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "504"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f327414%2fset-theoretical-foundations-of-mathematics-with-only-bounded-quantifiers%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
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.
$endgroup$
5
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
1
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
1
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
add a comment |
$begingroup$
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.
$endgroup$
5
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
1
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
1
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
add a comment |
$begingroup$
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.
$endgroup$
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.
edited Apr 8 at 13:45
answered Apr 7 at 21:08
Ali EnayatAli Enayat
10.6k13468
10.6k13468
5
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
1
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
1
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
add a comment |
5
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
1
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
1
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
5
5
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
$begingroup$
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?
$endgroup$
– Andreas Blass
Apr 8 at 1:15
1
1
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
$begingroup$
@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".
$endgroup$
– Ali Enayat
Apr 8 at 9:38
1
1
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
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.
$endgroup$
– Emil Jeřábek
Apr 8 at 14:30
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
$begingroup$
If I remember right, there is a good treatment of Mac Lane’s ZBQC in the book by John Bell.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:55
add a comment |
$begingroup$
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.
$endgroup$
1
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
1
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
3
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
1
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
2
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
|
show 11 more comments
$begingroup$
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.
$endgroup$
1
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
1
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
3
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
1
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
2
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
|
show 11 more comments
$begingroup$
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.
$endgroup$
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.
answered Apr 8 at 9:20
Andrej BauerAndrej Bauer
31.2k480171
31.2k480171
1
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
1
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
3
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
1
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
2
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
|
show 11 more comments
1
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
1
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
3
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
1
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
2
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
1
1
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
$begingroup$
@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.)
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 11:41
1
1
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
$begingroup$
@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?
$endgroup$
– Andrej Bauer
Apr 8 at 14:06
3
3
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
$begingroup$
@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.
$endgroup$
– Andrej Bauer
Apr 8 at 17:41
1
1
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
$begingroup$
@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.
$endgroup$
– Peter LeFanu Lumsdaine
Apr 8 at 18:51
2
2
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
$begingroup$
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.
$endgroup$
– Andrej Bauer
Apr 8 at 23:08
|
show 11 more comments
Thanks for contributing an answer to MathOverflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f327414%2fset-theoretical-foundations-of-mathematics-with-only-bounded-quantifiers%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
$begingroup$
There is no logical difference between the above two expressions. Bounded quantification is simply defined as the kind of implication you write.
$endgroup$
– Monroe Eskew
Apr 8 at 5:27
2
$begingroup$
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$.
$endgroup$
– Andrej Bauer
Apr 8 at 9:04
1
$begingroup$
I think one keyword for this question might be predicative.
$endgroup$
– Pedro Sánchez Terraf
Apr 8 at 9:47
2
$begingroup$
@AndrejBauer you miss the point. (S)he didn’t give an example of true unbounded quantification.
$endgroup$
– Monroe Eskew
Apr 8 at 11:45
1
$begingroup$
I just couldn't help myself.
$endgroup$
– Andrej Bauer
Apr 8 at 13:40