Suppose the state of the universe at a particular time can be considered as a set of atoms in R^3.
Now let’s suppose we choose IsIsSomeRocksPredicate such that IsIsSomeRocksPredicate(P) implies:
P(r,u) is a binary predicate (the first argument being our candidate bunch of rocks and the second argument being the state of the universe)
Let T be an isometry. Then P(r,u) implies P(T(r), T(u))
P(r,u) implies r is a subset of u
P(r,u) implies that r is a finite set of atoms
Let u and u’ be identical in some neighborhood of r. Then P(r,u) implies P(r,u’)
P(r,u) implies that r is not solidly connected to anything within u (this stops you defining half a rock as a rock)
P(r,u) probably implies some other stuff about the essential rockiness of r.
Then we can pick a P that satisfies this, and come up with an IsSameNumberOfRocks equivalence function. We can also come up with a successor function (adding an extra rock) that is unique up to IsSameNumberOfRocks. A big problem is that the successor function isn’t always defined if there’s a finite number of rocks in the universe, so I guess rocks really don’t behave like numbers.
(I hadn’t realized just how far you need to unpack “2 rocks + 2 rocks = 4 rocks”… I’m interpreting it to mean something like “if you have 2 rocks, and then include another 2 rocks which don’t include any from the first set of 2, then you end up with the same number of rocks as if you picked an entirely different set of 4 rocks”
Suppose the state of the universe at a particular time can be considered as a set of atoms in R^3.
Now let’s suppose we choose IsIsSomeRocksPredicate such that IsIsSomeRocksPredicate(P) implies:
P(r,u) is a binary predicate (the first argument being our candidate bunch of rocks and the second argument being the state of the universe)
Let T be an isometry. Then P(r,u) implies P(T(r), T(u))
P(r,u) implies r is a subset of u
P(r,u) implies that r is a finite set of atoms
Let u and u’ be identical in some neighborhood of r. Then P(r,u) implies P(r,u’)
P(r,u) implies that r is not solidly connected to anything within u (this stops you defining half a rock as a rock)
P(r,u) probably implies some other stuff about the essential rockiness of r.
Then we can pick a P that satisfies this, and come up with an IsSameNumberOfRocks equivalence function. We can also come up with a successor function (adding an extra rock) that is unique up to IsSameNumberOfRocks. A big problem is that the successor function isn’t always defined if there’s a finite number of rocks in the universe, so I guess rocks really don’t behave like numbers.
(I hadn’t realized just how far you need to unpack “2 rocks + 2 rocks = 4 rocks”… I’m interpreting it to mean something like “if you have 2 rocks, and then include another 2 rocks which don’t include any from the first set of 2, then you end up with the same number of rocks as if you picked an entirely different set of 4 rocks”