A finite alternative to Hilbert's Hotel?

Question

Here, I propose a finite alternative to Hilbert's hotel as the intuition for logically developing Dedekind's definition of infinite. I would like to know if this analogy entirely justifies the given formalism. If not, can anyone suggest changes?

A walk through a finite village

Suppose you start at any house in this finite village, and set out on a walk through the village, going from one house to another. Suppose further that, after you set out, you do not go to any house in the village (including your starting point) more than once. And after you set out, you also do not stop unless you return to your starting point. You may or may not go to every house in the village.

Intuitively, you could not avoid returning to your starting point under these conditions. You could, of course, return to your starting point without first going to every other house in the village. If you kept going, however, you would eventually run out of different places to go, and you would have to return to your starting point. Going anywhere else would be going there more than once. This would be true of any finite village. (It would not be true of any infinite village.)

How can we describe such paths mathematically? We can let $S$ be the set of houses in the village. Every path as described above can be represented (up to and including the point of return) by an injective function $f: S\to S$. If you are at house $x$, then the next house on your walk would be uniquely given by $f(x)$.

Why an injective function? To ensure that you visit each house no more than once, $f$ must be injective, i.e. if $f(x) = f(y)$, then $x = y$.

Suppose we let $x_0$ be the house that is your starting point. Since you must eventually return to $x_0$, there must exist a house $x_n$ such that $f(x_n) = x_0$, i.e. $x_n$ would be last house you visited before returning to your starting point $x_0$.

A set $S$ can then be said to finite if and only if

$\forall x_0, f:[x_0 \in S \land f:S\to S\implies [Injective(f) \implies \exists x_n \in S: f(x_n)=x_0]$

This can be shown to be equivalent to Dedekind's definition of finite, with it's negation being the definition of infinite.

Answer 1

The only comment I'd make is that it's not clear why you'd have to visit the first house twice. That seems odd to me, since that's exactly what we were trying to avoid, wasn't it? Maybe more appropriate would be if all families traded houses (though possibly still ended up in their usual house) such that there was, at most, one family per house. That also makes it clear that you could actually state the condition as "A set $S$ is finite if and only if every injection $S\rightarrow S$ is also a surjection"

It'd also be good to show why infinite sets might not satisfy this - that is, you could have every family move one house over, leaving the first house unoccupied (like in Hilbert's hotel).

Answer 2

Nice question!

I think the most natural and direct formalization of the intuition you're providing is:

Definition. A set $X$ is finite (in the walk-through-a-village-sense) iff there is no injection $f : \mathbb{N} \rightarrow X$.

The function $f$ describes a path, namely $(f(0),f(1),f(2),\ldots).$ This admits a cool little generalization:

Definition. (General) An algebraic structure $X$ is $N$-finite (in the walk-through-a-village-sense) iff there is no injective homomorphism $N \rightarrow X$, where $N$ is an algebraic structure over the same signature.

For example, a torsion group is just a $\mathbb{Z}$-finite group, in the walk-through-a-village-sense.