Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorstevevickers
   • CommentTimeNov 29th 2018
   • PermaLink
   Author: stevevickers
   Format: TextThe page [[finite set]] list various notions of finiteness, but one seems to be missing: sets that are Kuratowski finite with decidable equality. On the face of it that is the same as Bishop finiteness (isomorphic with some [n]), by taking an enumeration of the elements and using decidability of equality to omit duplicates. However, existence of that enumeration is weaker than choosing one. The distinction can be seen in sheaves over the circle S^1. The twisted double cover is, locally, Kuratowski finite with decidable equality. It even has a well-defined cardinality of 2. Locally, but not globally, it is isomorphic to [2]. To force global Bishop finiteness, or a theory of finite sets that is equivalent to that of natural numbers, you need the extra structure of a decidable total order. To put it another way, the notion of Bishop finiteness splits into local (weaker) and global versions. Does anyone have any views on what would be a widely acceptable terminology for this? In my paper "[Strongly algebraic = SFP (topically)](http://www.cs.bham.ac.uk/~sjv/papersfull.php#SFP)" I referred to the stronger version as "strongly finite" or "finite cardinal"".

   The page finite set list various notions of finiteness, but one seems to be missing: sets that are Kuratowski finite with decidable equality. On the face of it that is the same as Bishop finiteness (isomorphic with some [n]), by taking an enumeration of the elements and using decidability of equality to omit duplicates.
   
   However, existence of that enumeration is weaker than choosing one. The distinction can be seen in sheaves over the circle S^1. The twisted double cover is, locally, Kuratowski finite with decidable equality. It even has a well-defined cardinality of 2. Locally, but not globally, it is isomorphic to [2].
   
   To force global Bishop finiteness, or a theory of finite sets that is equivalent to that of natural numbers, you need the extra structure of a decidable total order.
   
   To put it another way, the notion of Bishop finiteness splits into local (weaker) and global versions.
   
   Does anyone have any views on what would be a widely acceptable terminology for this? In my paper "[Strongly algebraic = SFP (topically)](http://www.cs.bham.ac.uk/~sjv/papersfull.php#SFP)" I referred to the stronger version as "strongly finite" or "finite cardinal"".
2. • CommentRowNumber2.
   • CommentAuthorUlrik
   • CommentTimeNov 29th 2018
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexI'm not sure I understand. I think the “exists” on the page is meant to represent mere existence (truncated sigma in HoTT). Your example falls under this definition.

   I’m not sure I understand. I think the “exists” on the page is meant to represent mere existence (truncated sigma in HoTT). Your example falls under this definition.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 29th 2018
   • (edited Nov 29th 2018)
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think Steve is right. Check out [[finite object]] for a discussion of this local vs global distinction. If "finite" is to be a mere *property* of a set, then the "global" notions cannot be defined inside the "usual" higher-order internal logic of a topos, which is why the page [[finite set]] only discusses the notions that internalize to the "local" ones. Steve is saying we can however define them if we regard finiteness as a *structure*. Equivalently, we can define them in the internal dependent type theory of the topos, as non-truncated "properties" using a $\Sigma$ instead of an $\exists$. If we want a consistent way to refer to the latter notions, I suppose "strongly" isn't too bad, although a more descriptive word might be something like "algebraically". By the way, Steve, if you want to make `[links](like this)` you need to select the "Markdown+Itex" radio button below the text box when you post (which should be the default).

   I think Steve is right. Check out finite object for a discussion of this local vs global distinction.

   If “finite” is to be a mere property of a set, then the “global” notions cannot be defined inside the “usual” higher-order internal logic of a topos, which is why the page finite set only discusses the notions that internalize to the “local” ones. Steve is saying we can however define them if we regard finiteness as a structure. Equivalently, we can define them in the internal dependent type theory of the topos, as non-truncated “properties” using a $\Sigma$ instead of an $\exists$. If we want a consistent way to refer to the latter notions, I suppose “strongly” isn’t too bad, although a more descriptive word might be something like “algebraically”.

   By the way, Steve, if you want to make [links](like this) you need to select the “Markdown+Itex” radio button below the text box when you post (which should be the default).

4. • CommentRowNumber4.
   • CommentAuthorUlrik
   • CommentTimeNov 29th 2018
   • (edited Nov 29th 2018)
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexOh I see. But there's still some further distinction, then, between finite sets of the form $Fin(n)$ for some element $n:Nat$, and those of the form $Fin(n)$ for an external natural number $n$. (These differ over disconnected bases.) So maybe we can say strongly finite and externally finite, respectively? Edit to add: Instead of strongly finite set we could also just say totally ordered finite set. That seems to be unambiguous.

   Oh I see. But there’s still some further distinction, then, between finite sets of the form $Fin(n)$ for some element $n:Nat$, and those of the form $Fin(n)$ for an external natural number $n$. (These differ over disconnected bases.)

   So maybe we can say strongly finite and externally finite, respectively?

   Edit to add: Instead of strongly finite set we could also just say totally ordered finite set. That seems to be unambiguous.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeNov 29th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, that's true. I don't like "totally ordered" because I wouldn't want to consider the ordering part of the structure. That is, an isomorphism between strongly finite sets shouldn't have to respect the orderings.

   Yes, that’s true.

   I don’t like “totally ordered” because I wouldn’t want to consider the ordering part of the structure. That is, an isomorphism between strongly finite sets shouldn’t have to respect the orderings.

6. • CommentRowNumber6.
   • CommentAuthorUlrik
   • CommentTimeNov 30th 2018
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexNow I'm confused again: If you want the identity type of StronglyFiniteSet to correspond to isomorphism, then you're back to the usual (Bishop / decidable K) FinSet, right? (Form the pregroupoid of strongly finite sets and isomorphisms and Rezk/stack complete.) I thought the point was that StronglyFiniteSet should be equivalent to (internal) Nat. But maybe the point is really that you're interested in the pregroupoid (or precategory) structure on Nat/StronglyFiniteSet?

   Now I’m confused again: If you want the identity type of StronglyFiniteSet to correspond to isomorphism, then you’re back to the usual (Bishop / decidable K) FinSet, right? (Form the pregroupoid of strongly finite sets and isomorphisms and Rezk/stack complete.)

   I thought the point was that StronglyFiniteSet should be equivalent to (internal) Nat. But maybe the point is really that you’re interested in the pregroupoid (or precategory) structure on Nat/StronglyFiniteSet?

7. • CommentRowNumber7.
   • CommentAuthorstevevickers
   • CommentTimeDec 1st 2018
   • PermaLink
   Author: stevevickers
   Format: MarkdownItexIt's true that if "strongly finite" has the total order as part of the structure, then the corresponding homomorphisms have to preserve it. However, that doesn't stop you considering other morphisms and in fact that's exactly what you do when constructing the classifying toposes for various theories. There are five examples in which each is classified by a presheaf topos $[C, Set]$ where $C$ has strongly finite sets as objects, but varied morphisms. More economically, we can take the objects to be natural numbers. Then $C$ can be constructed internally in any elementary topos with nno (or arithmetic universe, for that matter). 1. Sets $C$ has, for morphisms, arbitrary functions between the corresponding finite cardinals. 2. Sets with decidable equality. The corresponding structure, which must be preserved by homomorphisms, is the inequality relation. Hence homomorphisms are injective. The morphisms of $C$ are injective functions between the finite cardinals. 3. Kuratowski finite sets. The structure is the finite subset (element of the free semilattice) that contains all the elements, and homomorphisms preserve this and so are surjective. The morphisms of $C$ are surjective functions between the finite cardinals. 4. Kuratowski finite sets with decidable equality Homomorphisms are isomorphisms The morphisms of $C$ are isomorphisms between the finite cardinals, so $C$ is a groupoid. 5. Kuratowski finite sets with decidable equality and decidable total order. Homomorphisms are order preserving isos - so there's at most one. The morphisms of $C$ are identity functions between the finite cardinals, so $C$ is just the discrete category on N. A similar principle applies to theories of algebras, where the classifying topos is that of covariant functors to $Set$ from the category of finitely presented algebras. Again, "finitely" is interpreted in the strong way, so that we have the category of strongly finite presentations.

   It’s true that if “strongly finite” has the total order as part of the structure, then the corresponding homomorphisms have to preserve it. However, that doesn’t stop you considering other morphisms and in fact that’s exactly what you do when constructing the classifying toposes for various theories. There are five examples in which each is classified by a presheaf topos $[C, Set]$ where $C$ has strongly finite sets as objects, but varied morphisms. More economically, we can take the objects to be natural numbers. Then $C$ can be constructed internally in any elementary topos with nno (or arithmetic universe, for that matter).

   1. Sets $C$ has, for morphisms, arbitrary functions between the corresponding finite cardinals.

   2. Sets with decidable equality. The corresponding structure, which must be preserved by homomorphisms, is the inequality relation. Hence homomorphisms are injective. The morphisms of $C$ are injective functions between the finite cardinals.

   3. Kuratowski finite sets. The structure is the finite subset (element of the free semilattice) that contains all the elements, and homomorphisms preserve this and so are surjective. The morphisms of $C$ are surjective functions between the finite cardinals.

   4. Kuratowski finite sets with decidable equality Homomorphisms are isomorphisms The morphisms of $C$ are isomorphisms between the finite cardinals, so $C$ is a groupoid.

   5. Kuratowski finite sets with decidable equality and decidable total order. Homomorphisms are order preserving isos - so there’s at most one. The morphisms of $C$ are identity functions between the finite cardinals, so $C$ is just the discrete category on N.

   A similar principle applies to theories of algebras, where the classifying topos is that of covariant functors to $Set$ from the category of finitely presented algebras. Again, “finitely” is interpreted in the strong way, so that we have the category of strongly finite presentations.