109

Clearly I first need to formally define what I mean by "junk" theorem. In the usual construction of natural numbers in set theory, a side-effect of that construction is that we get such theorems as $2\in 3$, $4\subset 33$, $5 \cap 17 = 5$ and $1\in (1,3)$ but $3\notin (1,3)$ (as ordered pairs, in the usual presentation).

Formally: Given an axiomatic theory T, and a model of the theory M in set theory, a true sentence $S$ in the language of set theory is a junk theorem if it does not express a true sentence in T.

Would it be correct to say that structural set theory is an attempt to get rid of such junk theorems?

EDIT: as was pointed out $5 \cap 17 = 5$ could be correctly interpreted in lattice theory as not being a junk theorem. The issue I have is that (from a computer science perspective) this is not modular: one is confusing the concrete implementation (in terms of sets) with the abstract signature of the ADT (of lattices). Mathematics is otherwise highly modular (that's what Functors, for example, capture really well), why not set theory too?

Jacques Carette
  • 11,669
  • 3
    I'm afraid that your definition of a junk theorem is somewhat imprecise since it doesn't address what the language of the theory $T$ is and how it is interpreted in the language of set theory. For one thing there are surely lots of theorems we would like to categorize as "junk" which are not even expressible in the language of $T$. Another issue is that a sentence like $5 \cap 17 = 5$ need not be junk depending on how you interpret your theory in set theory. For example if $T$ is the theory of lattices, then you can interpret $\omega$ (the set of finite von Neumann ordinals)... – Karol Szumiło Mar 10 '12 at 15:22
  • ...as a model of T in such a way that $5 \cap 17 = 5$ means exactly "the meet of $5$ and $17$ is $5$" which doesn't sound like junk to me. – Karol Szumiło Mar 10 '12 at 15:24
  • I purposefully under-specified the language of the theory $T$, and its interpretation - any such stringent specification would invite an answer along the lines of "oh, don't use that encoding, use this one instead", which would miss the point of the question. However, your comment on lattice theory is well taken, and I will try to adapt my question accordingly. – Jacques Carette Mar 10 '12 at 15:40
  • 4
    I find that link to nLab somewhat troubling. Of course that the fact $3\in 7$ is not used in mathematics, but the fact that for ordinals $\alpha,\beta$ we define that $\alpha<\beta$ if and only if $\alpha\in\beta$ is actually useful because it allows us to define the ordinals internally, and without the need for second order, or external characterizations such as "the third place in a natural numbers object". – Asaf Karagila Mar 10 '12 at 16:26
  • 1
    I am not sure I have understood the question; but have you looked at: AN ELEMENTARY THEORY OF THE CATEGORY OF SETS F. William Lawvere – Bruce Westbury Mar 10 '12 at 16:31
  • 66
    I believe the (nowadays) usual set-theoretic coding of ordered pairs is Kuratowski's ${{x},{x,y}}$. So 1 would not be a member of (1,3), but it would be a member of (0,3), which is probably worse junk. – Andreas Blass Mar 10 '12 at 16:41
  • 46
    Some time ago, the question was raised (perhaps by Peter Freyd), on the categories discussion list, whether a finite simple group could be a zero of the Riemann zeta function. I believe someone checked that, with the usual set-theoretic codings of such entities, the answer is negative. Whew! – Andreas Blass Mar 10 '12 at 16:44
  • @Andreas: With the usual coding, eh? I hope someone out there is sitting to verify with all possible coding, otherwise... we'll never know! :-) – Asaf Karagila Mar 10 '12 at 16:51
  • 3
    I brought up this problem on the FOM mailing list as an undergrad: http://cs.nyu.edu/pipermail/fom/2008-January/012571.html – Steven Gubkin Mar 10 '12 at 17:00
  • 25
    Isn't the set theory you are looking for type theory? Why do you want sets, or global membership? – Andrej Bauer Mar 10 '12 at 18:12
  • 2
    @Andreas: good points, $1\in (0,3)$ does seem even worse. And the 'question' of whether a group could be a zero is exactly the kind of 'junk' that shouldn't be there. – Jacques Carette Mar 10 '12 at 19:04
  • 2
    @Andrej: I do use type theory for my actual work, all the time. I am a convert. The point of my question was to get a better understanding of set theory and its use in mathematical practice. In particular, why does it seem acceptable to have such "junk" theorems at all. – Jacques Carette Mar 10 '12 at 19:09
  • 47
    But mathematical practice uses type theory, not set theory! It is not acceptable to have junk theorems. Mathematicians want variables to have types, either explicitly ("In this paper we assume that $G$ is a simple group...") or by convention ($f$ is a function, $k$ is an integer, etc). What would happen if a student wrote on a math exam "If $1 \in (x,y)$ then $x = 0$ or $y = 0$"? They would say the statement makes no sense and would refuse to judge its truth value. These are clear indications that we have a type theory. – Andrej Bauer Mar 11 '12 at 06:18
  • 8
    @Andrej, "junk" is a mater of perspective and taste, and no mathematical practice does not use formal type theory, nor does it use formal set theory. – Not Mike Mar 11 '12 at 06:35
  • 1
    Dear Jacques: A detail: In Bourbaki's theory you don't have $2\in3$. (You do have other junk theorems.) I'm mentioning that because some of the mathematicians using (at least implicitly) Bourbaki's theory are usually regarded as important ones, like Serre or Grothendieck. – Pierre-Yves Gaillard Mar 11 '12 at 10:27
  • 3
    Todd Trimble gave a quick and dirty setup for ETCS starting from first-order logic equipped with a natural deduction-style proof calculus over at the nLab: http://ncatlab.org/nlab/show/fully+formal+ETCS If instead you prefer to think of things in terms of a Hilbert-style proof calculus, you can very easily translate this into Bourbaki's notion of a "mathematical theory". – Harry Gindi Mar 11 '12 at 13:09
  • 5
    @Andrej: I agree that, in practice, mathematicians implicitly use types to 'rule out' many sentences being worthy of consideration. But until I see type theory taught as a foundational course, and elementary textbooks eschew sets, I will not believe that set theory is not still the 'foundations'. In a PL sense, mathematicians seem to use dynamic types rather than static types (since 'set' is their only type). – Jacques Carette Mar 11 '12 at 13:42
  • 15
    Both some pro-junk and some anti-junk commenters are implicitly using the term ‘set theory’ to mean only material set theory, that is set theory based on a global membership relation. But the OP and other commenters are also talking about structural set theory. What's important is that mathematicians can keep on talking about sets like we always do but still purge the junk statements from our formal language. A structural set theory, while arguably a type theory and certainly quite similar to a type theory, is still a set theory because it is a theory of sets. – Toby Bartels Mar 11 '12 at 16:18
  • 3
    @Toby: seems like your various comments could easily amount to an answer, perhaps it would be worth doing so? – Jacques Carette Mar 11 '12 at 20:48
  • This is relevant to this entire discussion: http://www.youtube.com/watch?v=l2O7YpENesw – Not Mike Mar 12 '12 at 21:39
  • i think the construction of formal theories has a price, the price is that you will get a lot of prepositions (not theorems) that would be natural and simple, but that is part of life, you will meet a lot of them all the time. –  Mar 10 '12 at 19:38
  • 3
    Particular ways of "coding" things like natural numbers within ZF or ZFC are only particular ways. There are a bunch of different ways of "coding" Dirac's generalized functions within systems believed to be consistent: One views them a some kind of limit of ordinary functions, or as linear functionals on a space of test functions, or as convolution quotients, and I think there are others. A few weeks ago I got into a dispute with a professor of mathematics who insisted that generalized funtions "are" linear functionals on a space of test functions, and that therefore$,\ldots\qquad$ – Michael Hardy Oct 27 '16 at 18:21
  • 2
    $\ldots,$notations like $\displaystyle\int_{-\infty}^\infty f(x)\delta'(x),dx = -f'(0)$ are bad notations because they obscure that alleged fact. What the various ways of "coding" have in common is the thing that they're trying to code. I think that thing they have in common is more basic than is anything that is logically "rigorous". And some of the things my interlocutor insisted were true were just "junk theorems" of the sort proposed in this question. $\qquad$ – Michael Hardy Oct 27 '16 at 18:23
  • 1
    @JacquesCarette If the natural numbers are embedded in the whole set of integers, is the theorem "$2$ is a nonnegative integer" a junk theorem or not ? – Philippe Gaucher Nov 30 '16 at 10:19
  • @PhilippeGaucher that is really beside the point: the question is about codings. So, depending on your exact set-theoretical representations, your example could be true in some models and false in others. And you also are imprecise about what 'is' means there: do you mean $\in$ or injection? – Jacques Carette Dec 01 '16 at 03:19
  • @JacquesCarette : Is the term "junk theorem" your own coinage? Has it appeared in any refereed publications by you or by others? – Michael Hardy May 13 '17 at 20:07
  • 1
    @MichaelHardy My own coinage - but inspired by Goguen's "No junk, No confusion" terminology. I am not aware of this appearing in the literature. – Jacques Carette May 14 '17 at 14:19
  • @JacquesCarette : Junk theorems, as you call them, can occur in other parts of mathematics than set theory, and I recently encountered an actual professor of mathematics getting confused by thinking one of those was a respectable theorem. – Michael Hardy May 15 '17 at 17:42
  • @MichaelHardy I would be quite curious about the details! (of the 'theorem', not the guilty party). – Jacques Carette May 16 '17 at 14:06
  • One of them is mentioned in comments above. Perhaps that is the only genuine example so far. First a toy example: Someone learns that a real number "is" a nonempty initial segment of $\mathbb Q,$ other than $\mathbb Q$ itself. Then some "junk theorems" say the real number $5$ is a subset of the real number $6$ and the rational number $5$ is a member of the real number $6$ and the rational number $5$ differs from the real number $5$. Another person learns that a real number is an equivalence class of Cauchy sequences, so those junk theorems do not follow from that. Next, the real example: – Michael Hardy May 16 '17 at 17:30
  • @JacquesCarette : First notice my comment above $\uparrow$ in which I forgot to ping you. Next, look at this: http://chat.stackexchange.com/rooms/44794/discussion-on-question-by-rajesh-dachiraju-what-is-the-total-variation-of-a-dira – Michael Hardy May 16 '17 at 17:31
  • @JacquesCarette : In the same way in which one defines the delta function or its derivative to be a linear operator on a space of test functions, so one can also define it to be a convolution quotient. Just as the initial-seqment-of-$\mathbb Q$ definition of "real number" leads to junk theorems not following from the equivalence-class-of-Cauchy-sequences definition, so also the linear-operator-on-the-space-of-test-functions definition of $\delta$ and $\delta'$ leads to a junk theorem that the convolution-quotient definition doesn't lead to. – Michael Hardy May 16 '17 at 17:35
  • @JacquesCarette : And there's also the limit-of-actual-functions definition of $\delta$ and $\delta'. \qquad$ – Michael Hardy May 16 '17 at 17:35
  • @JacquesCarette : D.U.'s claim that $\displaystyle \text{“ } \int_{-\infty}^\infty f(x) \delta'(x),dx \text{ ''}$ is bad notation is based only on "junk" in the sense in which you used the term. – Michael Hardy May 16 '17 at 17:37
  • 2
    @MichaelHardy Right. They are all accidents of particular choices of definitions and then not making those definitions abstract (as pointed out in the answers below). – Jacques Carette May 17 '17 at 18:13
  • @MichaelHardy For an alternative viewpoint, see Why Numbers Are Sets by Eric Steinhart. – user76284 Jul 27 '20 at 19:45

10 Answers10

173

I apologize for posting as an answer what should really be a comment, connected to one of Jacques Carette's comments on my earlier answer. Unfortunately, this is way too long for a comment. Jacques asked why we would bother with set-theoretic foundations at all. It happens that I wrote down my opinion about that about 15 years ago (in a private e-mail) and repeated some of it on the fom (= foundations of mathematics) e-mail list. Here's a slightly edited version of that:

Mathematicians generally reason in a theory T which (up to possible minor variations between individual mathematicians) can be described as follows. It is a many-sorted first-order theory. The sorts include numbers (natural, real, complex), sets, ordered pairs and other tuples, functions, manifolds, projective spaces, Hilbert spaces, and whatnot. There are axioms asserting the basic properties of these and the relations between them. For example, there are axioms saying that the real numbers form a complete ordered field, that any formula determines the set of those reals that satisfy it (and similarly with other sorts in place of the reals), that two tuples are equal iff they have the same length and equal components in all positions, etc.

There are no axioms that attempt to reduce one sort to another. In particular, nothing says, for example, that natural numbers or real numbers are sets of any kind. (Different mathematicians may disagree as to whether, say, the real numbers are a subset of the complex ones or whether they are a separate sort with a canonical embedding into the complex numbers. Such issues will not affect the general idea that I'm trying to explain.) So mathematicians usually do not say that the reals are Dedekind cuts (or any other kind of sets), unless they're teaching a course in foundations and therefore feel compelled (by outside forces?) to say such things.

This theory T, large and unwieldy though it is, can be interpreted in far simpler-looking theories. ZFC, with its single sort and single primitive predicate, is the main example of such a simpler theory. (I've left large categories out of T in order to make this literally true, but Feferman has shown how to interpret most of category theory, including large categories, in a conservative extension of ZFC.)

The simplicity and efficiency of ZFC and the fact that T can be interpreted in it (i.e., that all the concepts of T have set-theoretic definitions which make all the axioms of T set-theoretically provable) have, as far as I can see, two main uses. One is philosophical: one doesn't need to understand the nature of all these different abstract entities; if one understands sets (philosophically) then one can explain all the rest. The other is in proofs of consistency and independence. To show that some problem, say in topology, can't be decided in current mathematics means to show it's independent of T. So you'd want to construct lots of models of T to get lots of independence results. But models of T are terribly complicated objects. So instead we construct models of ZFC, which are not so bad, and we rely on the interpretation to convert them into models of T. And usually we don't mention T at all and just identify ZFC with "current mathematics" via the interpretation.

Christopher King
  • 5,715
Andreas Blass
  • 72,290
  • 16
    No need to apologize for this second, and wonderful answer. +1! – Asaf Karagila Mar 11 '12 at 23:08
  • 7
    Indeed, that is a wonderful answer. Thank you for posting it, it really does add something new. I wish that, as OP, I could upvote more than once! – Jacques Carette Mar 12 '12 at 02:36
  • 18
    I'd like to add one additional remark to this excellent answer: the theory T is not only many-sorted, but extremely dynamic. A variable $x$ may have the type of a real number in Section 3 of a paper, but the type of a point on a manifold in Section 6, the type of an indeterminate algebraic variable in Section 10, and undefined in all other sections. The notion of (say) a "pseudosmooth widget" may be an undefined type until Definition 5.7, at which point it suddenly becomes a first-class mathematical object (and all the previous axioms of T are now assumed to apply to it). ... – Terry Tao Mar 09 '14 at 16:07
  • 3
    ... although of course, if one wishes to be rigorous in T, one has to go through the exercise of verifying that the definition of a pseudosmooth widget in Definition 5.7 is indeed "well defined" (which one can do either via a set theory encoding, or by checking "consistency", "uniqueness", "coordinate independence", etc.). And so on. All this is already hard to formalise in standard first-order logic (with static variables, etc.), let alone in standard FOL+ZFC. But it would be extremely crippling in practice to give up these features of T when trying to prove a new mathematical result. – Terry Tao Mar 09 '14 at 16:11
  • 12
    @TerryTao, surely one is better off thinking of this dynamism as being of the form let x :: Real in …; let x :: ManPoint in …, with the understanding that we are only ever temporarily binding $x$ locally to some (often ill specified) block, rather than constantly rebinding an already permanently bound $x$? – LSpice Oct 26 '16 at 20:35
  • 10
    Some of the dynamism of T can (and should) be thought of this way, but not all. For instance, it is convenient in T to "abuse notation" by identifying an object with another object of a different type, e.g. identifying a group $(G, 1, \times, ()^{-1})$ with the set $G$, identifying a scalar constant $c$ with the constant function $f: x \mapsto c$, and so forth. – Terry Tao Oct 27 '16 at 01:32
  • 2
    Another source of dynamism is the use of iterative algorithms (e.g. greedy algorithms) in which a number of variables are dynamically updated a finite, infinite, or transfinite number of times until some halting condition is reached. One can formalise this statically of course, by introducing a time parameter and making everything in the algorithm a recursively defined function of that time parameter, but it can often be quicker and more conceptual to instead give dynamic pseudocode for such an argument. – Terry Tao Oct 27 '16 at 01:34
  • @AndreasBlass: Are you sure that $T$ is gonna be a many-sorted theory rather than an order-sorted logic? Wikipedia: "While many-sorted logic requires two distinct sorts to have disjoint universe sets, order-sorted logic allows one sort $s_{1}$ to be declared a subsort of another sort $s_{2}$". I think that for example, the type "integer" should be a subtype of "real number". And every type should be a subtype of the type "object", so that we can have a relation $x\in M$, where $x$ can be any object, and $M$ has type "set". –  Nov 19 '16 at 11:18
  • 1
    @AndreasBlass: A second question: Do you really think that mathematicians generally work in $T$, or is $T$ just supposed to be the natural choice of a formalization of the real informal theory in which mathematicians generally reason? –  Nov 19 '16 at 11:26
  • @AndreasBlass, Terence Tao: A problem I see that could occur when formalizing $T$ is that in natural language we humans say something like "A(x) and B(x)" where B(x) only makes sense if A(x) is true. Thus we "A(x) and B(x)" consider to be false if A(x) is false, even if B(x) is meaningless in this case. It's hard for me to imagine how one can formalize these features of natural language in a formal system. –  Nov 19 '16 at 11:55
  • @AndreasBlass: Another feature of natural language I don't know how to formalize is that for each type/sort $S$, and every predicate $P$ on that type, one expects that there is a type of all the objects $x$ of $S$ that have the property $P(x)$. –  Nov 19 '16 at 18:22
  • @TerryTao: For example on the type of ordered pairs one can define a predicate "isGroup" that says that the first component is a set, and the second an operation on that set, such that the group axioms hold. Thus there should be a type of all groups, so that we can say "For all groups ..." and don't have to say "For all ordered pairs, if this ordered pair happens to be a group, then ...", because this would be unnatural, right? Also, the integers are a type and "even" is a predicate on the integers, thus "even integer" should be a type. –  Nov 19 '16 at 18:23
  • @TerryTao: You say "if one wishes to be rigorous in T, one has to go through the exercise of verifying that the definition of a pseudosmooth widget in Definition 5.7 is indeed "well defined" (which one can do either via a set theory encoding, or by …)" Why should one use a set theory encoding when working in the theory T? Isn't T intended to not involve such unnatural encodings? –  Nov 20 '16 at 16:42
  • The use of a set theory encoding is always an option in T for the purposes of showing that a concept one is trying to introduce is in fact well defined. But one can also do so in other ways (basically by demonstrating existence, uniqueness, and independence from temporarily introduced parameters such as coordinate charts). T doesn't reject set theory, but rather it gives working mathematicians the freedom to use it or not use it depending on the application and on the mathematician's aesthetic tastes. – Terry Tao Nov 28 '16 at 18:57
  • @AndreasBlass I object that most mathematicians work in this theory $T$. For instance, in linear algebra, suppose we have a vector space $V$ over $\mathbb{R}$, and we wish to define its dual space $V^*$, Naturally we take this to be a vector space with underlying set all linear functions from $V$ to $\mathbb{R}$, and we endow it with vector space structure in the usual way. There are many other examples. It's not clear how this would work in your theory. Perhaps instead most mathematicians work in $ZFC$ with expansions by definitions, and just ignore the resulting "junk theorems?" – Danielle Ulrich Nov 30 '16 at 01:28
  • 3
    @DouglasUlrich I see no difficulty in constructing dual spaces in $T$. Just take the construction as written in any standard textbook, and as summarized in your own comment. Note that T includes sorts for sets, functions, and the like --- all the stuff you need to build dual spaces. – Andreas Blass Nov 30 '16 at 01:55
  • @AndreasBlass Perhaps I am misunderstanding, but I thought part of what you were saying was that every vector space had to consist of urelements. The phrase I am looking at is "There are no axioms that attempt to reduce one sort to another" am I misreading this? – Danielle Ulrich Nov 30 '16 at 01:58
  • 1
    @DouglasUlrich If you wanted to introduce $V^$ as a new sort, then you'd specify it with suitable axioms (a non-degenerate bilinear pairing with $V$), rather than constructing it as a space of functions. The space-of-functions description would then serve not as a "reduction" of $V^$ to other sorts like sets or functions but rather as a proof that the new sort and axioms are conservative over the previously available theory. That would be a perfectly reasonable view of dual spaces, but it seems not to be what mathematicians usually do. – Andreas Blass Nov 30 '16 at 02:03
  • @AndreasBlass My point was just that this does seem to impose a limitation on how people do math, or at least think about it. – Danielle Ulrich Nov 30 '16 at 02:13
  • @AndreasBlass This is a minor quibble, relative to your main argument in the post, I realize. – Danielle Ulrich Nov 30 '16 at 02:17
  • 2
    @user99916 : This business about A(x) and B(x) not only can be formalized but has been in some programming languages such as C. You can even write if ((0 == 1) && (1/0)) … and the division by zero will never be executed. Obviously, that's a silly example, but if the B(x) is a routine that might never terminate (or just might be terribly inefficient), as long as A(x) is only true in those cases where B(x) is fine to use, then you can write it that way. – Toby Bartels Mar 15 '17 at 06:08
  • 1
    @TobyBartels, perhaps it would be better to discuss that in a typed context. In a dependently typed language, the equality test can reveal (at the type level) that two things are not equal. As long as you only write 1/x in a context within which that information is available (typically under a pattern match), there is no difficulty whatsoever. – dfeuer Mar 07 '18 at 04:35
  • A couple of things. I think to say that your theory T is encoded in ZFC is better than to say that is interpreted, indeed I am not quite sure what interpreted means in this context (although this is probably just ignorance on my part). Nonetheless, to say that we encode zero as the empty set is better, because this is precisely what is being done. – James Smith Mar 24 '18 at 16:53
  • Also, justifications for encoding T in ZFC are always a little shaky. Many, including me, would say that the main justification is just a kind of historical inertia. Set theory provided a unifying foundation for mathematics well over a century ago now at am time I am led to believe when mathematics was not the connected whole it is generally perceived to be now. To go back to your other justification, namely that encoding T in ZFC affords meta-mathematical or meta-logical properties of T to be proven is something I have often wondered about... – James Smith Mar 24 '18 at 16:54
  • ...My point is here not to disagree with that justification, at least not now, but to ask the question, what is the value of set theory if ZFC is not taken as a foundation for T. I mean, are set theorists primarily only interested in such meta results, or does modern set theory have a place and a purpose outside of this remit? I have thought of asking such a question on MO at times and wonder whether anyone can enlighten me. – James Smith Mar 24 '18 at 17:00
  • Generally I think the "everything is a set" belief is just that and that T, whatever exactly we take T to be, can be treated on its own without the need to encode it as anything else. I would say that "everything is what it is". There is no need for example, to encode zero as the empty set, we can simply have a term called zero and leave it at that. Similarly, there is no need to encode mathematical objects as tuples. We can just define group as a type with two properties. – James Smith Mar 24 '18 at 17:03
  • Finally, I wonder about the assertion that you can prove anything about T by encoding it in ZFC. Surely all of the properties that T possesses must surely be constitutive of T, and proving things about them, or any other formal endeavour do to with T, is best done in the language of T or formalisms that are based on it. At best you will get the same results from ZFC, at worst you will get, well, as the OP suggested, the 'j' word. Unfortunately, $1\cap 2$ does not equal $1$. – James Smith Mar 24 '18 at 17:08
  • 2
    @JamesSmith I"ll try to briefly answer your five comments, in order. (1) "Interpretation" has a standard meaning in mathematical logic, and that's what I intended. Essentially, it means that all the primitive notions of one theory (like T) are expressed in terms of the primitive notions of another theory (like ZFC) and all the axioms of the former theory thereby become theorems of the latter. You can call it "encoding" for conversational purposes, but "interpretation" conveys the precise technical meaning for logicians. – Andreas Blass Mar 24 '18 at 21:46
  • (2) Inertia may have something to do with ZFC being the standard (nowadays) foundation for mathematics; it takes a lot of work to show that a proposed foundation works, and once the work is done for one foundation, there's less motivation to repeat it for others. I'm not sure mathematics is really more connected now than 100 years ago. New connections have indeed been found, but also new areas have developed, and I"m not sure about the trade-off between these two phenomena as far as the overall connectedness of the subject is concerned. – Andreas Blass Mar 24 '18 at 21:50
  • 1
    (3) For many set theorists, including me, the most interesting parts of set theory are not its foundational aspect but rather (a) its role as a mathematical subject in its own right, sometimes called "infinitary combinatorics and (b) its applications to other fields of mathematics. Applications to real analysis were part of Cantor's motivation for developing set theory in the first place, and applications have long been ubiquitous in general topology. More recently, other fields, like abelian group theory and C*-algebras have used a lot of set theory. – Andreas Blass Mar 24 '18 at 21:54
  • (4) I agree. You're a confirming instance of my claim that "mathematicians generally reason in" T. (5) I see no reason why the properties of a theory should be best done in the language of that theory. My nearest dictionary gives no meaning for "constitutive" that would support the claim that all properties of T must be constitutive of T, but I admit that "constitutive" may have a technical meaning in philosophy that I don't know and that would support your claim. Finally, concerning $1\cap2$: ZFC proves some statements that are not the interpretations of statements in T's language; so what? – Andreas Blass Mar 24 '18 at 22:01
  • @AndreasBlass Thanks so much for replying, it's more than my disjointed comments deserved. And I'm glad they were taken in the right spirit. You have a point about connectedness. Another mathematician in fact clarified the historical situation for me a few weeks ago. He said, in brief, that until set theory came along mathematics was indeed disjointed. Geometry had its own axioms, for example, going back to Euclid, and I think he gave two other areas that were in a sense solid but apart. I think the point was that when set theory came along, since it brought with it a... – James Smith Mar 25 '18 at 13:58
  • ...very basic set of axioms that to be common seemed common sense, and since moreover it appeared that everything could be encoded as a set (please forgive the usage), it become the de facto standard, as it were. Anyway, so I was told. Tom Körner once wrote that a glance at any maths textbook will convince that mathematicians make lousy historians. I would go so far as to say that you don't even have to glance at a text book! – James Smith Mar 25 '18 at 14:02
  • Your third comment is really enlightening, thank you. I'm glad to know there's more to modern set theory than foundations! Of course so many mathematical things are sets with additional structure, I don't need to tell you this, but it still wasn't obvious to me whether set theory would influence, say, topology. Again, it's good to learn that it does. – James Smith Mar 25 '18 at 14:05
  • About point four. If A constitutes B, then B is constitutive of A. I hope you appreciated my formal definition! Alternatively, a good definition Google returned is 'having the power to establish or give organised existence to something'. My point being, if you want to prove anything about T then, well, best start with T! And on the last point, I think we will have to agree to differ, but that is half the fun. – James Smith Mar 25 '18 at 14:11
  • [1/2} Dear Andreas, This is very much how i conceive mathematics, with perhaps a personal tendency to remember "my" objects are sets in a definitional extension of ZF. I wonder though exactly what you mean by the first philosophical use: not having to consider the "nature" of defined objects. It seems to me that on the contrary there is a slight problem with considering sets as so fundamental: it obscures the reasons to choose sets as most practical foundation, best suited to human (mathematical) reasoning, in our social context. I'm not sure what you mean by "philosophical" and "nature": – plm Sep 15 '23 at 06:11
  • [2/2] if "philosophical" means relative to the utility (in Mill's utilitarian sense) of a way of thinking (here thinking in terms of sets with common axioms), and "nature of these entities" means the psychological dynamics characteristic of their manipulation -for instance "sets" may relate to visual stimuli, seeing "real sets of objects", and our brain's dynamics mirroring those real objects' belong to their nature; then i think that studying only the philosophy/nature of sets eschews part (probably most) of that of defined objects, which may have their own (eg proof-theoretic) utility. – plm Sep 15 '23 at 06:14
  • You can get closer to this theory if you explicitly "close" it under interpretation. See https://mathoverflow.net/a/464547/65915 – Christopher King Feb 20 '24 at 19:45
66

What you are describing is the idea of "breaking" an abstraction. That there is an abstraction to be broken is pretty much intrinsic to the very notion of "model theory", where we interpret the concepts in one theory in terms of objects and operations in another one (typically set theory).

It may help to see a programming analogy of what you're doing:

uint32_t x = 0x12345678;
unsigned char *ptr = (unsigned char *) &x;
assert( ptr[0] == 0x12 || ptr[0] == 0x78 );  // Junk!

const char text[] = "This is a string of text.";
assert( text[0] == 84 );  // Junk!

// Using the GMP library.
mpz_t big_number;
mpz_init_ui(big_number, 1234);
assert(big_number[0]._mp_d[0] == 1234); // Junk!

All of these are examples of the very same thing you are complaining about in the mathematical setting: when you are presented with some sort of 'type', and operations for working on that type, but it is actually implemented in terms of some other underlying notions. In the above:

  • I've broken the abstraction of a uint32_t representing a number modulo $2^{32}$, by peeking into its byte representation and extracting a byte.

  • I've broken the abstraction of a string being made out of characters, by using knowledge that the character 'T' and the ASCII value 84 are the same thing

  • In the third, I've broken the abstraction that big_number is an object of type integer, and peeked into the internals of how the GMP library stores such things.

In order to avoid "junk", I think you are going to have to do one of two things:

  • Abandon the notion of model entirely
  • Realize that you were actually lying in your theorems: it's not that $2 \in 3$ for natural numbers $2$ and $3$, but $i(2) \in i(3)$ for a particular interpretation $i$ of Peano arithmetic. Maybe making the interpretation explicit would let you be more comfortable?

(Or, depending on exactly what you mean by the notation, the symbols $2$ and $3$ aren't expressing constants in the theory of natural numbers, but are instead expressing constants in set theory.)​​​​

Community
  • 1
  • 5
    Yes, that accords perfectly with my thinking. But I am not sure one has to abandon the idea of a model entirely - just a model which is in the same 'universe' as the abstraction. Your second point (about $i(2)\in i(3)$) is exactly right, in that making the interpretation explicit would make me hugely more comfortable. [I am working on combining code generation and symbolic computation in a typed setting, where all these interpretations are fully explicit, which made me 'see' these subtleties in mathematics more clearly] – Jacques Carette Mar 10 '12 at 19:17
  • 22
    Here's a question to ponder: does making a model of peano arithmetic out of the real numbers count as being in the same 'universe'? If so, is $\sqrt{11 - 6 \sqrt{2}} + \sqrt{11 + 6 \sqrt{2}} = 6$ a junk theorem? –  Mar 10 '12 at 19:35
  • 7
    In computer science, there is a deep theory on how to avoid this kind of junk by forcing type safety. One approach is to view objects as though they were hidden by a non-computable oracle, and you can only access their properties by querying the oracle. – David Harris Mar 10 '12 at 22:03
  • 8
    @David: and a much, much better and more advanced approach is to use techniques of programming language design, of which all the good ones are forms of type theory. @Hurkyl: your question in the context of $\lambda$-calculus and programming languages is answered by realizing that there are two kinds of semantics, Church-style or intrinsic, and Curry-style or extrinsic. – Andrej Bauer Mar 11 '12 at 06:22
  • 18
    @Hurkyl: This is going the other way; a junk theorem is a formal theorem that is not informally correct, while you have an informal theorem that is not formally correct. However, such theorems always have a correct formal analogue, in this case $\sqrt{11 - 6\sqrt{2}} + \sqrt{11 + 6\sqrt{2}} = i(6)$, where $i$ is now the type conversion from natural numbers to real numbers (and actually there are some more applications of $i$ in there). This type conversion is not an artefact but rather something that we very much want; but we suppress all mention of it by abuse of notation. – Toby Bartels Mar 11 '12 at 16:34
  • 1
    In the C programming language, these would not be junk theorems but undefined behavior. Is there any analogue to the set theory? – David Harris Mar 13 '12 at 02:02
  • 1
    @DavidHarris A set-theoretic analogue of undefined behaviour is asking whether $2^{\aleph_0} = \aleph_1$. This is anything but junk, however -- it's just that the "standard" (i.e. ZFC axioms) does not define cardinal exponentiation. – Robert Furber Aug 10 '18 at 18:26
  • @RobertFurber Could you explain why you say that ZFC doesn't define cardinal exponentiation? Isn't cardinal exponentiation $|B|^{|A|}$ defined by $|B^A|$ (i.e. the cardinality of the set of functions $A \to B$)? – ಠ_ಠ Feb 20 '19 at 11:34
  • 2
    @ಠಠ I was attempting to make a distinction between "proving the existence of a function" and "defining a function" (at arguments). This may not be the usual terminology for expressing this distinction. What I mean is that ZFC proves the existence of a two-argument function on alephs, cardinal exponentiation, as you wrote it, but it does not define it even at $(\aleph_0,2)$, because we have models of set theory where $2^{\aleph_0} = \aleph_1$ and others where $2^{\aleph_0} = \aleph{\omega_1}$, and various other things. – Robert Furber Feb 20 '19 at 21:16
  • Junk theorems are avoided in Type Theory, indeed this is exploited in HoTT with the univalence principle (in a nutshell isomorphic objects are equal). See my paper: https://arxiv.org/abs/2111.06368 – Thorsten Altenkirch Sep 06 '23 at 11:05
49

Structural set theory, as described on the nlab page you linked to, is probably the best answer to your question. To avoid junk theorems, one must deviate somewhat from ordinary ZF-style set theory where everything is a set. That's because, once you decide, in the context of such a "material" set theory, that 5 and 17 are to be sets (because there's nothing else for them to be), they have to have a union, and there's no intuitively reasonable choice for that. (I said "union" rather than "intersection" because one might consider the empty set a reasonable intersection; but the union can't be empty unless both sets are.) A very elementary (undergraduate) presentation of some mathematics from this viewpoint is in the book "Sets for Mathematics" by Lawvere and Rosebrugh; a more advanced presentation is (if I remember correctly) Paul Taylor's "Practical Foundations of Mathematics".

Andreas Blass
  • 72,290
  • 8
    The natural follow-up question would be: why stick to 'set theory' and not advocate type theory? – Jacques Carette Mar 10 '12 at 19:11
  • Even though MO seems to really like your answer, I think that Hurkyl's is actually closer to what I was looking for. – Jacques Carette Mar 10 '12 at 19:18
  • 2
    Personally, I find something "truthful" in treating natural numbers (finite ordinals) as sets because $\varnothing = 0$, ${\in} = {<}$, ${\subseteq} = {\leq}$, ${\cup} = {\max}$, and ${\cap} = {\min}$. For an essay arguing this viewpoint, see Why numbers are sets by Eric Steinhart. – user76284 Mar 21 '20 at 01:18
16

Many of these answers are quite satisfying, but I'd just like to emphasize that much of the confusion may come from overloading of symbols like "$\in$", "$\subset$", "$\cap$", and "$2$", that is, such symbols have multiple context-dependent meanings. In particular, the junk theorems you provide are situations where some kind of overloading has been misinterpreted - indeed, the validity of the theorems may change if you switch to viewing the natural numbers as complex numbers.

The overloading of symbols is useful, because many algebraic and geometric structures like rings and manifolds admit a notion of "underlying set", but we should be careful not to confuse the $\subset$ attached to manifolds-as-we-use-them with the $\subset$ attached to a chosen pure set-theoretic encoding of manifolds. For example, the intersection of submanifolds is likely to look quite complicated once we choose a method to unfold such an operation into a pure set-theoretic formula.

Another way to view junk theorems is to say that they are statements that depend on a non-canonical choice of encoding of mathematical objects as pure sets. This is not to be interpreted as a claim that I know a way to sort out the foundations attached to notions like "non-canonical choice of encoding".

S. Carnahan
  • 45,116
13

Although it's a little wordy, there is a method of formalizing things that avoids these theorems. To be sure, theorems such as $ \{ \{ \} , \{ \{ \} \} \} \in \{ \{ \} , \{ \{ \} , \{ \{ \} \} \} \} $ remain, but that's not junk; however, $ 2 \in 3 $ (or even $ 2 _ \mathbb N \in 3 _ \mathbb N $) will not be there.

Define a natural-number system to be an ordered pair $ ( N , \sigma ) $ such that $ \sigma $ is an ordered pair $ ( z , s ) $ such that $ z $ is an element of $ N $, $ s $ is a function from $ N $ to $ N $, $ z $ is not in the range of $ s $, $ s $ is injective, and the only subset $ A $ of $ N $ such that $ z \in A $ and $ s [ A ] \subseteq A $ is $ N $ itself. Given a natural-number system $ \mathbb N = ( N , ( z , s ) ) $, let $ 0 _ \mathbb N $ be $ z $, let $ 1 _ \mathbb N $ be $ s ( z ) $, etc; similarly, you can define $ + _ \mathbb N $, $ \times _ \mathbb N $, etc. You can now prove theorems about natural numbers; such theorems take the form ‘For each natural number system $ \mathbb N $, […].’, much like theorems about groups take the form ‘For each group $ G $, […].’.

Of course, number theory is unlike group theory in an important respect, which is that all natural-number systems are isomorphic (indeed uniquely isomorphic). This is certainly worth proving (after defining what such an isomorphism is so that you can even state it), but you don't actually have to prove it (or even state it) to start stating and proving theorems about prime numbers or whatever. You might at least want to prove that a natural-number system exists (which is the only place in all of this that requires the Axiom of Infinity), although you don't even have to do that to prove theorems about prime numbers; in any case, the system whose existence you choose to prove plays no special role in the rest of the theory.

In something like ETCS, of course, one always does something like this to construct natural numbers, which is why ETCS seems to have fewer junk theorems. But then when you construct $ \mathbb R $ out of $ \mathbb N $, the junk theorems appear in both formal systems, unless you go through the same rigmarole to define a real-number system, etc. But you can do that.

ETA: If I can cite an authority, this approach is pretty much the one taken by Walter Rudin in Principles of Mathematical Analysis (baby Rudin) for $ \mathbb R $. In Chapter 1, Rudin defines a complete ordered field, defines an isomorphism between such, proves that any two such are uniquely isomorphic, and says that we will now use any one of them and not worry about which one it is. Thus the remainder of the book essentially becomes preceded by ‘If $ \mathbb R $ is a complete ordered field’. (In an appendix to the chapter, he proves that one exists, he but makes no further reference to that construction.)

Toby Bartels
  • 2,654
11

The question being, "Would it be correct to say that structural set theory is an attempt to get rid of such junk theorems?", the answer I think is "only partly or only if extremely limited."

Clicking on the link, I find a theory called ETCS as an example of structural set theory. ETCS has 0, N (the natural numbers), and S (the successor function) as primitives in its language, and it assumes effectively as axioms the normal assumptions about them (e.g. it assumes the existence and uniqueness of recursion).

Obviously, if you assume 0, N, and S as primitives and make the normal assumptions about them, rather than constructing them and proving the normal assumptions (Russell's honest toil rather than theft), then one can avoid junk theorems about the natural numbers. The same effect could be achieved, by modifying ZFC by introducing the same primitives and assuming, on top of the normal ZFC axioms, the Peano Axioms.

ETCS does not, however, get rid of all junk theorems unless it is only supposed to be about arithmetic and the natural numbers. If it, for instance, is also supposed to allow the construction of the real numbers and the development of analysis, then it will still get junk theorems about the real numbers.

abo
  • 1,844
  • 3
    "The same effect could be achieved, by modifying ZFC by introducing the same primitives and assuming, on top of the normal ZFC axioms, the Peano Axioms." No, even if you add $0$, $\mathbb{N}$ and $S$ as primitives, you will still be able to ask whether $\mathbb{N}\in S$ which is a "junk question" (and its answer will be a junk theorem) – Guillaume Brunerie Mar 11 '12 at 15:21
  • 5
    The language about natural numbers isn't in ETCS to avoid junk statements about natural numbers but to serve in an axiom of infinity. But you make a good point, that there can still be junk statements involving things like real numbers. For example, if a real number is defined as a lower set of rational numbers, then we have such junk theorems as $3 \in \pi$. We even have $2 \in 3$, where here $2$ is the rational number $2$ and $3$ is the real number $3$. (The abuse of language here is essentially the same as in material set theory.) – Toby Bartels Mar 11 '12 at 16:26
  • 1
    @Toby: I'm not sure what you mean. I suspect you and I have different systems in mind. In ETCS, I'd define an element of a set $X$ to be a map $1 \to X$. So for "$3 \in \pi$" to make sense, $\pi$ would have to be a set and $3$ would have to be a map $1 \to \pi$. And this isn't the case. @abo: for the same reason, I don't see any evidence of junk theorems in ETCS. – Tom Leinster Mar 12 '12 at 15:37
  • @Tom - You are right, but there will still be junk theorems about the embeddings of one set into another. For example, if you are representing the real numbers as a monomorphism to 2^Q, you are going to have theorems about "evaluating a real number at a rational", which wouldn't make sense to most people out of context. – Steven Gubkin Mar 12 '12 at 20:43
  • (although this particular example has a nice interpretation: r(q) =0 if r>q and r(q) = 1 if r<=q, say.) – Steven Gubkin Mar 12 '12 at 21:00
  • 4
    Tom, in ETCS there are two distinct meanings of $x \in y$. In one of these, $y$ is an abstract set (an object of the category $Set$) and $x$ is an element of $y$ as you said. In the other, there is some abstract set $z$ lying around but unmentioned, $x$ is an element of $z$, and $y$ is a subset of $z$ (meaning a monomorphism to $z$). This latter sense may be written $x \in_z y$, but ordinary mathematical practice abused the notation. If real numbers are encoded in ETCS as lower subsets of rational numbers, then $2_\mathbb{Q} \in_\mathbb{Q} 3_\mathbb{R}$ is a theorem. – Toby Bartels Mar 13 '12 at 06:33
  • In second-order arithmetic, we have both an $S$ unary function and a $\in$ binary relation, but $1 \in S$ is not a well formed formula, because each side of $\in$ must be a term of type 0, and $S$ on its own is not a term at all. The same would happen in the extension of ZFC with a larger signature - $S$ on its own would not be a term. @Guillaume Brunerie – Carl Mummert Mar 26 '18 at 21:29
  • 3
    On the other hand, when we define an element of a set $X$ to be a map $1 \to X$, then we can find $\pi$ as a map $1 \to \mathbb{R}$ and we can then ask "is $\pi$ surjective?" Any time we define an object of some kind to be an object of a second kind, we will have junk theorems unless we are unable to ask any questions about objects of the second kind that cannot be asked about objects of the first kind. – Carl Mummert Mar 26 '18 at 21:31
  • 8 years on, I maintain that there are no "junk theorems" in ETCS. The examples mentioned by @TobyBartels and Steven G only look like junk because of abuses of notation. For Toby's example of $3\in_{\mathbb{Q}}\pi$, conscientious notation would be $3 \in_{\mathbb{Q}}(j: \pi\to\mathbb{Q})$, where $j$ is your preferred injection implementing the Dedekind cut. But there's nothing junky there. It's a perfectly meaningful statement about a particular map $j$. While "$3 \in \pi$" looks like junk, the proper form "$3 \in j$" plainly isn't. Similar comments apply to Steven's example. – Tom Leinster Jul 23 '20 at 00:26
  • @TomLeinster : If you're going to use ETCS to do ordinary mathematics, then you've got to adopt some kind of notation (or abuse thereof) to have collections of concrete sets, where the elements of some abstract set are interpreted as subsets of some other abstract set to which elements of the latter abstract set might belong. In whatever notation you use for that, $3 \in \pi$ is a theorem (assuming that you construct real numbers as lower sets of rational numbers). – Toby Bartels Jul 23 '20 at 07:03
  • I mean, suppose that I'm trying to do topology, and I say that a topological structure on a set $A$ is a collection of subsets of $A$ satisfying certain conditions, and then I start writing things like ‘Let $A$ be a set, let $\mathcal{T}$ be a topology on $A$, let $x$ be an element of $A$, let $G$ be an element of $\mathcal{T}$, and consider whether $x \in G$’, then you might object that this is an abuse of notation, but whether you write it that way or add pedantic decorations, this is a thing that mathematicians talk about. – Toby Bartels Jul 23 '20 at 07:31
  • In particular, if $A$ is $\mathbb{Q}$, $\mathcal{T}$ is the Scott topology under $\geq$, $x$ is $3$, and $G$ is $]-\infty,\pi[$, then $3 \in G$. But if we represent real numbers as lower subsets of $\mathbb{Q}$, then $\mathcal{T}$ is the set of extended real numbers (or extended lower real numbers if I'm being constructivist), $G$ is $\pi$, and whatever abuse of notation allowed us to write $3 \in G$ before now allows us to write $3 \in \pi$. – Toby Bartels Jul 23 '20 at 07:31
  • @TobyBartels I'm not sure we disagree very much. I agree that, in your setting, $3 \in \pi$ is a (loosely-stated) theorem. But it's not a "junk" theorem, because the accurate statement is $3\in(j:\pi\to\mathbb{Q})$ where $j$ is the map implementing the Dedekind cut. That has a perfectly sensible meaning. The point is that having defined $\mathbb{R}$ via the subobject $i:\mathbb{R}\to2^\mathbb{Q}$, we're free to treat it as an abstract set (as we almost always do) or as equipped with the map $i$ to make it into a subobject of $2^\mathbb{Q}$ (which we only do when interested in Dedekind cuts). – Tom Leinster Jul 23 '20 at 17:00
  • So in ETCS, there is no canonical membership relation on $\mathbb{R} \times \mathbb{Q}$ enabling one to ask "is $3 \in \pi$?". As of course you know (and I'm aware you do know all this!), the sets $\mathbb{R}$ and $\mathbb{Q}$ are only defined up to isomorphism, like everything else in ETCS. In order to get such a relation, you have to make an explicit choice of embedding $i: \mathbb{R} \to 2^\mathbb{Q}$. Sure, you could choose to abuse notation to obscure your choice of $i$ from your readers, but why would you? – Tom Leinster Jul 23 '20 at 17:06
  • It seems to me that the question of when mathematicians choose to abuse notation, and when it's safe to do so, is separate. We all try to abuse notation to just the right degree, and we constantly make value judgements about what that is. But that's orthogonal to the question of "junk" theorems in ETCS. (Also: I find the emotive term "junk" unhelpful. All mathematical statements have content; it's a question of what it is.) – Tom Leinster Jul 23 '20 at 17:15
  • We should be able to agree on most things in mathematics, but let's try to find the areas of disagreement. There is a canonical membership relation from $\mathbb{Q}$ to $\mathbf{2}^{\mathbb{Q}}$, and this pulls back to a relation from $\mathbb{Q}$ to $R$ given any function $R \to \mathbf{2}^{\mathbb{Q}}$; so, if you define $\mathbb{R}$ as a subset of $\mathbf{2}^{\mathbb{Q}}$, then there is a canonical membership relation from $\mathbb{Q}$ to $\mathbb{R}$. And if you define $\mathbb{R}$ using lower cuts, then the rational number $3$ is related to the real number $\pi$ under this relation. – Toby Bartels Jul 25 '20 at 22:01
  • I agree that the junk theorems that people complain about have non-junky content. The content of $3_{\mathbb{Q}} \in \pi_{\mathbb{R}}$ is that $3 < \pi$. The content of $2_{\mathbb{N}} \in 3_{\mathbb{N}}$ in ZFC is that $2 < 3$. (Is $\in$ always secretly $<$? No, such as if you define real numbers as upper cuts, but it does seem pretty common.) Given a formal definition with apparent junk theorems, you can always tease out what they really mean, and that's something with real content. So I agree about that. But I don't think that this means that junk theorems are entirely unproblematic. – Toby Bartels Jul 25 '20 at 22:11
  • 1
    What I really disagree with is your claim that abuse of notation is orthogonal to junk theorems. To the contrary, I think that notation is key. Nobody objects to ${{},{{}}}\in{{},{{}},{{},{{}}}}$, which is obvious (if you don't get lost in the braces), and nobody objects to $2<3$ (which my 4-year-old understands); they only object to $2\in3$. In ZFC with the von Neumann natural numbers, all of these mean the same thing; it's how you write this that determines whether or not it looks like junk. – Toby Bartels Jul 25 '20 at 22:17
  • And ETCS is the same; because of how the Axiom of Infinity is written in the two set theories, we don't have this particular junk theorem, but we still have the other ones. Write $3\in{q\in\mathbb{Q};|;3<\pi}$ or $3<\pi$, and nobody minds; but write $3\in\pi$, and it's a problem. Yet these all mean the same thing if you define real numbers as lower cuts of rational numbers, a definition that is equally natural in any set theory that (like both ZFC and ETCS) doesn't axiomatize the real numbers directly. – Toby Bartels Jul 25 '20 at 22:22
  • (And notice that every one of these statements involves an abuse of notation in ETCS, so that is not the source of the problem. Sorry, now I'm done.) – Toby Bartels Jul 25 '20 at 22:23
  • MO comment threads are a crappy medium for conversations like this, so while I've enjoyed your stimulating thoughts, Toby, I'm going to make this my last comment. So: (1) No one has been able to come up with an example of a "junk" theorem in ETCS except by abusing notation. (2) As a practical matter, notation must sometimes be abused - but wisely! (3) In ETCS, it's important to distinguish between a set $R$ and a subset $i:R\to S$ (e.g. $\mathbb{R}\to 2^\mathbb{Q}$); both are defined up to iso, but iso means different things for each. In ETCS, "subset" is structure rather than property! – Tom Leinster Jul 25 '20 at 23:54
  • @Tom Leinster : Agreed that this is a poor medium, and we could move to chat (or the nforum) if you want. I guess that while (1) is true as far as I know, you can hardly say anything worthwhile in ETCS without abuse of (or extremely detailed) notation (and this is also true of ZFC, just not quite as much). The question is whether the notation that we adopt, whatever that is, to allow us to say what we want, also allows us to say ‘junk’ that we don't want. I see no difference between ETCS and ZFC in this regard. – Toby Bartels Jul 27 '20 at 01:57
5

The problems you mention occur as a result of two related reasons:

  • Objects such as the set of real numbers, which do not intrinsically belong to set theory, are 'encoded' as a set, so we can ask meaningless questions and obtain junk answers.
  • The encoding is not natural or canonical, and different encodings of the same object give rise to different sets of junk theorems.

It appears that Homotopy Type Theory addresses these issues:

  • Firstly, you cannot ask meaningless questions which involve treating a term of one type as though it were another type (such as treating an ordered pair as a set, or as a real).
  • Secondly, the equality type $A = B$ of two types is defined as the space of isomorphisms between those types, so isomorphic objects are equal (in the sense that the equality type is inhabited). This means that different encodings of the same object (such as the set of real numbers) correspond to equal types.

The first of these bullet points applies equally well to ordinary Martin-Löf type theory; the second relies on Voevodsky's powerful univalence axiom.

David Roberts
  • 33,851
Adam P. Goucher
  • 12,211
  • 1
    Yes - but the answer you give is close to anachronistic. HoTT hadn't really reached the collective consciousness yet. – Jacques Carette Mar 25 '18 at 01:44
  • 2
    The inability to ask meaningless questions would come from any type theory. Even Peano arithmetic, though perhaps not very expressive, has the property that there are no junk theorems: every term represents a number and every atomic sentence represents an honest relationship between numbers. – Carl Mummert Mar 26 '18 at 21:48
  • 2
    Are you saying that in type theory there is no way to prove that $\Bbb R$ and $\Bbb R^2$ have the same cardinality, or that the Cantor space is isomorphic to its square? – Asaf Karagila Feb 14 '19 at 11:05
  • 1
    @Asaf Note that constructively one needs to be clear what "$\mathbb{R}$" means. If $\mathbb{R} = 2^\mathbb{N}$ (the set of functions), then $2^\mathbb{N} = 2^{\mathbb{N}\sqcup \mathbb{N}} = 2^\mathbb{N}\times 2^\mathbb{N}$, where by $=$ I mean isomorphic. Choosing a decomposition $\mathbb{N} = \mathbb{N}\sqcup \mathbb{N}$ for instance into odds and evens gives the isomorphisms canonically. If one means Dedekind cuts, and is working in a framework with Dedekind cuts ≠ Cantor–Cauchy reals, then it's a bit more involved... – David Roberts Mar 07 '19 at 03:03
  • @Adam I wouldn't say $A=B$ is defined to be the type $A\simeq B$ in UF/HoTT. It's an axiom in UF/HoTT that the canonical map $A=B \to A \simeq B$ has contractible fibres. Or in flavours of cubical type theory it's a theorem that this is the case. – David Roberts Mar 07 '19 at 03:05
  • 1
    @David: Yes, I know that there are situations where the set of reals can be injectively mapped into the natural numbers, but there is no bijection between them. That was one of the "Whoa..." moments I've had on this site before. But nevertheless, I think that the bijection between $\Bbb N$ and $\Bbb{N\times N}$ is as constructive as it gets, at least the Cantor pairing one. So very easily we can code finite sets of natural numbers as natural numbers. Even though the natural numbers are not "intrinsicly set theoretic objects". And then we can ask if $3$ is a member of $7$, for example. – Asaf Karagila Mar 07 '19 at 16:28
  • I wouldn't say "3 is a member of 7", but rather make the coding explicit: "3 is a member of the set corresponding to 7". It's like power sets in ETCS: their elements aren't literally subsets, but we talk as if they are, hiding the correspondence under sugaring. – David Roberts Mar 07 '19 at 23:41
  • 4
    @David: Serving someone junk covered in sugar might taste sweet, but it's still junk. To claim that ETCS or HTT removing junk theorems is the very definition disingenuous, at best they make it slightly less natural to pronounce the junk, but it's there just as well. And arguably, asking in a ZFC context whether or not "is $\pi$ an ordered pair?" should receive an answer of "how did you code $\pi$ and how did you code ordered pairs?". – Asaf Karagila Mar 08 '19 at 17:22
  • @JacquesCarette why is HoTT anachronistic? If it hasn't reached the collective consciousness maybe it should. actually it seems that formal verification using Type Theory is becoming more widespread, e.g. using systems like Coq or Lean. Yes, these systems don't implement HoTT and univalence but they already exclude junk theorems. In a way you have the pain without the benefits. – Thorsten Altenkirch Sep 06 '23 at 11:14
  • 1
    HoTT was still very very young 5.5 years ago when that comment was first written @ThorstenAltenkirch ! Things are still evolving indeed. – Jacques Carette Sep 08 '23 at 00:08
  • @JacquesCarette Indeed, however, Junk theorems are also absent from pre HoTT Type Theory. The strange thing about ITT is that you cannot define any property that distinguishes different presentations but you cannot show that they are equal either. – Thorsten Altenkirch Sep 11 '23 at 16:48
1

Among the many subtle realities of mathematics in the 21st century, the most amazing is the lack of imagination. The language of set theory is built from the ground up to be as simple as possible. To appreciate the complexity inherent and information encoded in such simple statements (even the ones you might not find aesthetically pleasing) requires detachment.

This detachment I'm talking about is the clear distinction between: syntax and semantics. Statements made in the formal language have absolutely no meaning outside of formal manipulation, and so are not meant to be seen as anything more than symbols without meaning.

It is only when you attach meaning (or an interpretation) to these symbols that something of value can be said.

That having been said:

The examples you give are not actually statements in the language of set theory; they are artifacts of a general lack of communication between logic/model theory and the rest of mathematics. The symbols you strung together (1, $2$, 5, $4 \subset 54$, $\cap$, and so on) are examples of defined notions, which are used as a convenience.

And when we attach meaning to these statements something amazing happens:

What was $2 \in 3$ becomes the obviously true

$\{ \{\}, \{\{\}\} \} \in \{\{\}, \{ \{\}, \{\{\}\} \}\}$

and $1 \in \langle 0, 3 \rangle$ becomes

$\{\{\}\} \in \{ \{ \{\} \}, \{ \{\{\}, \{ \{\}, \{\{\}\} \}\} \}\}$

In Summary:

You are confusing the formal language with the actual interpretation of the language.

As such you are faced with something every body has known since the 19th century:

Our perception imposes "phantom" structure on the universe in an attempt to have it make sense; not the other way around.

PS: Feel free to edit. You also might want to change the title, since the post I wanted to put here would have gotten me banned.

Not Mike
  • 1,655
  • No, Jacques is asking a perfectly valid question. I feel free to downvote the answer, also because of its tone. – Andrej Bauer Mar 11 '12 at 06:24
  • Ok, thats fine. I'm just being honest mate. – Not Mike Mar 11 '12 at 06:29
  • 13
    There's nothing wrong with being honest, but you suggest Jacques has a misunderstanding of set theory, which doesn't seem to be supported by the evidence. You may disagree with him about whether this phenomenon is important, or how to think about it philosophically, but there's no doubt that the statements he points out are true theorems of ZFC (under standard definitions) that would be marked as wrong or meaningless in many elementary mathematics courses. That's at least a strange situation, even though of course they don't look objectionable when the definitions are expanded out. – Henry Cohn Mar 11 '12 at 06:39
  • No where have I said anything about ZFC, nor have I said anything about misunderstanding set theory. My post is about syntax and semantics, and making sure they are distinguished. It is effectively the post of Hurkyl without the extra stuff. Please read the post. – Not Mike Mar 11 '12 at 06:43
  • Even the OP says this, read his comments to Hurkyl – Not Mike Mar 11 '12 at 06:46
  • 4
    OK, maybe I mischaracterized it as a misunderstanding of set theory, but you do refer to "artifacts of your misunderstanding". I don't think it's productive to write MO answers in a tone that can reasonably be read as insulting. – Henry Cohn Mar 11 '12 at 07:04
  • 2
    Changed the wording. – Not Mike Mar 11 '12 at 07:09
  • 12
    Although I agree that it's important to distinguish syntax from semantics, I don't see how that distinction helps with the original question. You seem to say that, since 2 is defined in set theory as ${{},{{}}}$, this is the only meaning for 2; anything else is mere syntax. Jacques's question is based on the fact that mathematicians generally intend a different meaning for 2, not a set at all but a natural number. By formalizing everything in set theory, do we lose the original meaning of 2 and retain only its set-theoretic surrogate? – Andreas Blass Mar 11 '12 at 22:08
  • @Andreas, This is a result of my personal lack of imagination, I couldn't think of a differing interpretation that highlighted my point. $2$ can have many differing interpretations, some distinct from its intended interpretation and others consistent with it. I did not mean to block out all other contenders. – Not Mike Mar 11 '12 at 23:31
  • @Michael: Set theory exists to formalize other parts of mathematics. Most people go so far as to say that the real proof of a theorem (which we never actually write down) would be a complete unpacking of all encodings back to raw ZFC and a proof of that first order sentence in ZFC. So shouldn't we pay a lot of attention to how that encoding takes place? It seems that we have a pretty good map one direction: Given a formal mathematical statement, with some work you can probably write down its ZFC equivalent. This question focuses on the other direction. The problem is that there isn't – Steven Gubkin Mar 12 '12 at 21:05
  • 2
    The problem is that the map "Normal Mathematics"--->"ZFC" is many to one, and so if you start off with a statement in ZFC, it doesn't lift to a unique interpretation in "Normal Math". (But wouldn't it be interesting to try and set up the map to have as "nice properties" as possible? It is many to one one, but maybe we can get a "path lifting" property - Given a true statement in ZFC and an interpretation of one part of the expression, ther might be a unique way to interpret the rest in a sensible way. I would imagne that automated proofs people are careful to set up this map to minimize work) – Steven Gubkin Mar 12 '12 at 21:12
  • 2
    @Steven, Such a "lifting" is not really something I personally would find useful; but this is just my personal taste. The point I was trying to highlight, was this: A statement which is True, is True for reasons beyond how it is written. In this sense, "junk" only exists, when you haven't taken the time to see what makes it true. Hurkyls' answer sums this up much better than mine. – Not Mike Mar 12 '12 at 21:32
  • Do you care about real numbers, Riemann surfaces, boolean algebra, groups, or any other of the objects most mathematicians care about, or only sets? – Steven Gubkin Mar 12 '12 at 21:43
  • 1
    It would worry me to have a proof of some fact about ordinary mathematics, encoded in set theory, but not to have any way of making sense out of that set theoretic proof. What if an actual argument relied on such junk? "The Riemann hypothesis is true because the critical strip is a function from the set of natural numbers to the set of ordered 7 tuples of groups, and ..." – Steven Gubkin Mar 12 '12 at 21:48
  • 4
    @Steven, if its true, then its not junk, and is perfectly valid to use. – Not Mike Mar 12 '12 at 21:55
  • Moreover, in some sense, that kind of imagination might just be what is needed to solve the problem. As an example, the proof of FLT exploits this kind of jump. – Not Mike Mar 12 '12 at 21:56
  • 1
    @Steven, I'm detecting some sort of misunderstanding here: I'm saying that anything that is True and provable should not be called "Junk." Not because it can be put in the context of sets (this assumption is an unjustified jump in your logic) but because there is a context somewhere unrelated to how it is written, in which it is true. I used sets as an example, so sue me. – Not Mike Mar 12 '12 at 22:06
  • 7
    Steven: to say that set theory exists just to serve as a formal framework is like saying mathematics exists just to allow physicists use the language. – Asaf Karagila Mar 13 '12 at 11:07
  • I didn't say the word "just". I don't think that set theory would be a current object of study without such encodings. – Steven Gubkin Mar 13 '12 at 14:18
  • @Steven Gubkin : I wouldn't worry if a proof of a meaningful theorem uses a junk theorem. The junk theorems are junk because the choice of encoding is arbitrary, but each encoding is based on something meaningful. So if a proof uses the junk theorem $2 \in 3$ (work von Neumann numbers), then it really uses the meaningful theorem $2 < 3$ (or $2 \in {n \in \mathbb{N} \mid n < 3}$, which is basically the same). Even if the proof uses the entire structure of the von Neumann natural numbers, that is a sequence of sets definable from any notion of natural numbers, so define it and use it. – Toby Bartels Jul 17 '19 at 13:30
  • An interesting and worthwhile answer, even though I'd not entirely agree with it. Fractionally, yes. :) To be clear, my own philosophical feeling is that formal mathematics is a narrative of something else (not at all necessarily "platonic"). – paul garrett Jul 25 '20 at 22:37
0

Junk theorems like this are avoided in Type Theory (not just HoTT). This is because I cannot talk about the representation of objects like the natural numbers. This is exploited in Homotopy Type Theory with the univalence principle - in a nutshell: isomorphic types are equal. I have written a paper about this: https://arxiv.org/abs/2111.06368

Thorsten Altenkirch
  • 125
0

To avoid junk theorems, you need to use many-sorted logic.

Consider a theory $P$ as follows:

  • There is a sort for $V$ and a binary relation on it $\in$ that obeys ZFC.
  • If there is an interpretation (without parameters) of a multi-sorted theory $T$ in $P$, we add all of $T$'s sorts and relations and functions to $P$, and add axioms saying that structure formed by them is isomorphic to the structure in $P$ described by the interpretation.
  • We also close $P$ under definitional expansions.

So there is a sort of natural numbers that is isomorphic to the Von Neumann numerals in $V$, but $2 \in 3$ is no longer a wff.

Note that $P$ is closed under all sorts (pun unintended) of operations. For example, $P$ can interpret the theory whose sorts are cartesian products of sorts in $P$, a second-order version of $P$, etc...

Christopher King
  • 5,715