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?

  • 66
    $\begingroup$ 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. $\endgroup$ Mar 10, 2012 at 16:41
  • 46
    $\begingroup$ 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! $\endgroup$ Mar 10, 2012 at 16:44
  • 25
    $\begingroup$ Isn't the set theory you are looking for type theory? Why do you want sets, or global membership? $\endgroup$ Mar 10, 2012 at 18:12
  • 47
    $\begingroup$ 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. $\endgroup$ Mar 11, 2012 at 6:18
  • 15
    $\begingroup$ 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. $\endgroup$ Mar 11, 2012 at 16:18

10 Answers 10


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.)​​​​

  • 5
    $\begingroup$ 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] $\endgroup$ Mar 10, 2012 at 19:17
  • 22
    $\begingroup$ 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? $\endgroup$
    – user13113
    Mar 10, 2012 at 19:35
  • 7
    $\begingroup$ 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. $\endgroup$ Mar 10, 2012 at 22:03
  • 8
    $\begingroup$ @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. $\endgroup$ Mar 11, 2012 at 6:22
  • 18
    $\begingroup$ @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. $\endgroup$ Mar 11, 2012 at 16:34

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.

  • 16
    $\begingroup$ No need to apologize for this second, and wonderful answer. +1! $\endgroup$
    – Asaf Karagila
    Mar 11, 2012 at 23:08
  • 7
    $\begingroup$ 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! $\endgroup$ Mar 12, 2012 at 2:36
  • 18
    $\begingroup$ 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). ... $\endgroup$
    – Terry Tao
    Mar 9, 2014 at 16:07
  • 12
    $\begingroup$ @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$? $\endgroup$
    – LSpice
    Oct 26, 2016 at 20:35
  • 10
    $\begingroup$ 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. $\endgroup$
    – Terry Tao
    Oct 27, 2016 at 1:32

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".

  • 8
    $\begingroup$ The natural follow-up question would be: why stick to 'set theory' and not advocate type theory? $\endgroup$ Mar 10, 2012 at 19:11
  • $\begingroup$ Even though MO seems to really like your answer, I think that Hurkyl's is actually closer to what I was looking for. $\endgroup$ Mar 10, 2012 at 19:18
  • 2
    $\begingroup$ 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. $\endgroup$
    – user76284
    Mar 21, 2020 at 1:18

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".


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.)


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.

  • 3
    $\begingroup$ "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) $\endgroup$ Mar 11, 2012 at 15:21
  • 5
    $\begingroup$ 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.) $\endgroup$ Mar 11, 2012 at 16:26
  • 1
    $\begingroup$ @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. $\endgroup$ Mar 12, 2012 at 15:37
  • 4
    $\begingroup$ 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. $\endgroup$ Mar 13, 2012 at 6:33
  • 3
    $\begingroup$ 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. $\endgroup$ Mar 26, 2018 at 21:31

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.

  • 1
    $\begingroup$ Yes - but the answer you give is close to anachronistic. HoTT hadn't really reached the collective consciousness yet. $\endgroup$ Mar 25, 2018 at 1:44
  • 2
    $\begingroup$ 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. $\endgroup$ Mar 26, 2018 at 21:48
  • 2
    $\begingroup$ 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? $\endgroup$
    – Asaf Karagila
    Feb 14, 2019 at 11:05
  • 1
    $\begingroup$ @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... $\endgroup$
    – David Roberts
    Mar 7, 2019 at 3:03
  • 4
    $\begingroup$ @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?". $\endgroup$
    – Asaf Karagila
    Mar 8, 2019 at 17:22

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.

  • 13
    $\begingroup$ 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. $\endgroup$
    – Henry Cohn
    Mar 11, 2012 at 6:39
  • 4
    $\begingroup$ 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. $\endgroup$
    – Henry Cohn
    Mar 11, 2012 at 7:04
  • 12
    $\begingroup$ 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? $\endgroup$ Mar 11, 2012 at 22:08
  • 4
    $\begingroup$ @Steven, if its true, then its not junk, and is perfectly valid to use. $\endgroup$
    – Not Mike
    Mar 12, 2012 at 21:55
  • 7
    $\begingroup$ 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. $\endgroup$
    – Asaf Karagila
    Mar 13, 2012 at 11:07

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


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...


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.