Suppose we define "finite set" as a set on which there can exist a cyclic path that passes through all of its elements. (The details of the formulation are present below).
I have two questions:
- Is the above definition equivalent to a known definition of "finite set"?
- If the answer to 1. is yes, then to which of these known definitions it is equivalent?
Formal workup:
Define: $ P \text { is a path on S} \iff \forall m \in P [\exists k,l \in S [m=(k,l)]] \\ \wedge \forall y\in S [\exists k [(y,k) \in P \lor (k,y) \in P]] \\ \wedge \forall s [\exists k ((s,k) \in P) \implies \exists! k ((s,k) \in P )] \\ \wedge \forall s [\exists k ((k,s) \in P) \implies \exists! k ((k,s) \in P )] \\ \wedge \exists z \forall s ([\exists k ((s,k) \in P) \wedge \not \exists r ((r,s) \in P)] \implies s=z) \\ \wedge \exists z \forall s ([\exists k ((k,s) \in P) \wedge \not\exists r ((s,r) \in P)] \implies s=z) $
Define: $P \text { is a path} \iff \exists S (P \text{ is a path on S})$
Define: $x \text { is a point on } P \iff \exists S (P \text { is a path on S} \wedge x \in S)$
Define: $x \text { is an end point on } P \iff x \text { is a point on } P \\ \wedge \exists!m \in P (\exists k [m=(x,k)] \lor \exists l [m=(l,x)])$
Define: $ P \text { is an endless path on } S \iff P \text{ is a path on } S \\ \wedge \not \exists x (x \text { is an end point on } P)$
Define: $ Q \text { subpath } P \iff P \text { is a path } \wedge Q \text { is a path } \wedge Q \subset P $
Define: $ P \text { is a continuous path} \iff P \text { is a path } \\ \wedge \forall Q,T,A,B (Q\neq \emptyset \wedge T\neq \emptyset \wedge Q \text { is a path on } A \wedge T \text { is a path on } B \wedge Q \text { disjoint } T \wedge (Q \cup T) \text{ subpath } P \implies \neg (A \text{ disjoint } B))$
Define: $ P \text { is a cyclic path on } S \iff P \text { is an endlesss path on S } \wedge P \text { is a continuous path}$
Define: $ \text { set S is finite} \iff \exists P (P \text { is a cyclic path on S})$
What I like about this definition is that it doesn't mention the naturals, it doesn't mention well foundedness or well-ordered relations in an explicit manner, it depends on "endlessness", which goes in the opposite direction to the common notion of the finite set as a set that has every subset of it having two ends, so it looks different from the common known definitions of the finite, on the other hand it does depict the point of failure of finiteness in the non-standard naturals, we can have a $\mathbb{Z}$-chain that can go unnoticed if we cannot see all sub-paths on a set, so a really infinite set can be disguised as finite. Although it appears trivial (and I had already knew half of the answer to it), yet still I think that confirming its equivalence with the known definitions of finite set is a relevant issue, especially in theories where separation fails like $NF$ and the alike.