I've been thinking a lot about foundations, again, and specifically how to make isomorphism invariance clearer - which seems to be one of the main purposes of alternative foundations such as Homotopy Type Theory.

The problem seems to be that we often have different models of the same object which we would really like to identify with each other (as a simple example, $\mathbb{N} = \{\varnothing, \{\varnothing\}, \{\varnothing, \{\varnothing\} \}, \dots\}$ is an entirely different set from the $X \subseteq \mathbb{Z}$ we tend to call $\mathbb{N}$) and in ZFC, under the current definitions, we cannot formally do so. What we tend to do if we ever point this out at all is simply call it an abuse of notation, and justify it by claiming that the clear isomorphisms existing between the two models will preserve any theorems we want to invoke.

Homotopy type theory claims to make this easier by making it so that if we have two isomorphic objects we can say they are equal (in some sense I'm not entirely clear on) and so carry across any theorems we like. The problem is that it seems we really need to leave our comfort zone to be able to do this.

My question is...could this all be fixed by changing our point of view on some definitions? For instance, rather than saying "The set of natural numbers is [some specific set]", we could have the definition be phrased something like "$(X, Succ, 0)$ is a natural numbers set if and only if [Peano Axioms]", and then have as a theorem that $\{\varnothing, \{\varnothing\}, \{\varnothing, \{\varnothing\} \}, \dots\}$ is a natural numbers set.

What I'm effectively suggesting is that we relegate the phrase "set of natural numbers" to the same level as "group", so that rather than proving that some statement is true of a particular set which we have called the set of natural numbers, we prove that the statement is true for any set of natural numbers. When we want to work with natural numbers, we simply say "Let $\mathbb{N}$ be a set of natural numbers" in the same way that we often say "Let $G$ be a group".

What kind of problems arise from working in this way?

If I'm not being clear enough please let me know, because I do have a few specific definitions in my head that I could give as examples which might clarify what I mean.

EDIT: While structural set theory is effectively what I want, my question is whether or not this type of definition change would give us the benefits of structural set theory without leaving ZFC.

  • $\begingroup$ @NoahSchweber Not quite, the point is... is this a way of doing this within the usual foundation? $\endgroup$ – Nethesis Jan 14 '16 at 13:26
  • 2
    $\begingroup$ Oh, I see, I misunderstood. Sure we can - phrases like "the set of natural numbers" are just convention, anyways. $\endgroup$ – Noah Schweber Jan 14 '16 at 13:27
  • 1
    $\begingroup$ Does it bother people that different compilers may produce different binaries for the same code? That different languages implement the same algorithm ever do slightly different? That different algorithms can solve the same task? I never understood why mathematics should be any different. $\endgroup$ – Asaf Karagila Jan 14 '16 at 13:28
  • $\begingroup$ @AsafKaragila I don't necessarily think it should be, I'm just wondering if there's any problem with editing the definitions in such a way that it becomes clearer that different implementations are essentially equivalent, and it becomes clear what is true of any implementation. $\endgroup$ – Nethesis Jan 14 '16 at 13:31
  • $\begingroup$ @Nethesis I like this perspective! Have an upvote :). $\endgroup$ – Alberto Takase Feb 16 at 4:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.