Return to Frege's question, What justifies arithmetic? And consider the ur-proposition that counting a finite set always produces the same number, and ask whether this has a logical justification, that is a justification from assumptions which are necessarily true. Note that few of us actually first believed this assertion because of a logical proof. We accepted it say by authority - we were told it was so - or by experience - we experimented and discovered that counting the same set in two different ways always produced the same. Neither of these methods of justification, of course, necessarily ensure truth.
OK you say, but there is a proof from bedrock principles using induction which is entirely from logical principles. Model a counting of a finite set $A$ as an injective function from an initial segment of the natural numbers (beginning with 1) onto $A$, that is a sequence without repetitions. For the base case suppose a counting of a set produces the number 1. Then there is one thing, and the only way to count the set would produce the number 1. So check for the base case.
Now suppose $m$ is the successor of $n$ and the induction hypothesis holds for $n$ (that is, if we count any set to have the number $n$, then any other counting of the set must also produce the number $n$). Consider a set $A$ where one counting produces the number $m$, and another counting produces the number $v$. It does seem an acceptable (and logical) principle that if $m$ is the successor of $n$, and we have counted to $m$, then we need to have counted first to $n$, and then counted one more. That is, if $\boldsymbol f$ counts $A$ as $m$, then there exists $\boldsymbol f',B,b$ such that $b \in A \land B = A $\ $\{b\} \land\boldsymbol f'$ counts $B$ as $n$. Induction proves that $v \neq 1$ has a predecessor $u$. Letting $\boldsymbol g$ count $A$ as $v$, then there exists $\boldsymbol g',C,c$ such that $c \in A \land C = A$ \ $ \{c\} \land \boldsymbol g'$ counts $C$ as $u$. And - we can't apply the induction hypotheses immediately because while $B$ is of size $n$, and $C$ is of size $u$, $B$ and $C$ need to be the same set to apply the hypothesis, but they may be different since $b$ and $c$ may be different.
The way the proof must continue is that (assuming that $b$ and $c$ are different, since if they are the same there is no problem) we assert the existence of a sequence $\boldsymbol g''$, where we replace $b$ by $c$, that is where $\boldsymbol g'(i) = b$, assign instead $\boldsymbol g''(i) = c$ and leave everything else the same. Then by simple logic $\boldsymbol g''$ counts $B$ and indeed counts it as as $u$. Then one can apply the induction hypothesis, and the ur-proposition follows.
Only the assumption that there exists a sequence with the one replacement - that is, given a sequence $abcd...x...$, there must exist a sequence $abcd...y...$, for any $x$ and $y$ - is, or does not appear to be, a logical assumption. The new sequence is not a part of the older one, and its existence is not implicit in the older's existence. The assumption simply does not fall out of the meaning of "sequence." It is in fact very useful - I claim that with it and some other, only necessarily true, assumptions, one can develop arithmetic -, and so it can be given the justification that it leads to results which are useful in the sciences, and therefore it is desirable to make it. But this is different from being logical, and the question must be raised if in some cases reality is better represented without this assumption or perhaps making a different one. Modern physics is full of non-intuitive explanations; perhaps it can be better presented by using a non-intuitive mathematics.
So is the uniqueness of counting necessarily true? That one proof depends on a non-logical assumption, is not conclusive, since after all perhaps there is another, this time logical, proof where the replacement assumption is not needed. I have tried a bit and failed from assumptions which satisfy me, so I conjecture that it is essential in the framework of these assumptions. Anyway, my question is, is it? I formalize the question in the following way.
Consider FOL with equality, with one constant 1, with one two-place predicate $\sigma$ (successoring), and with two types (standard and bold). Standard types are natural numbers, and bold types are finite sequences of natural numbers.
Define:
$\boldsymbol f^D(x)$ abbreviates $\exists y \space \boldsymbol f(x) = y$
This defines $x$ being in the domain of $\boldsymbol f$.
$\boldsymbol f^H(x)$ abbreviates $\boldsymbol f^D(x) \land \forall y (\sigma(x,y) \Rightarrow \neg \space \boldsymbol f^D(y))$
This defines $x$ as the top or high number in the initial segment defining the sequence $\boldsymbol f$.
$\boldsymbol f =_k \boldsymbol g$ abbreviates $\forall x \neq k \forall y(\boldsymbol f(x) = y \iff \boldsymbol g(x) = y)$
This says $\boldsymbol f$ and $\boldsymbol g$ are defined and have the same values for the same $x$, except perhaps at $k$.
Consider the following axioms:
1/ $\forall x \forall y \forall z (\sigma x,y \land \sigma x,z \Rightarrow y = z)$
2/ Induction schema, i.e. $\phi (1) \land \forall n \forall m (\sigma n,m \land \phi (n) \Rightarrow \phi (m)) \Rightarrow \forall n \space\phi (n)$
3/ $\forall\boldsymbol f \space \boldsymbol f^D (1)$
4/ $\forall\boldsymbol f \exists n \space \boldsymbol f^H (n)$
5/ $\forall\boldsymbol f \forall n \forall m \space (\boldsymbol f^H(m) \land \sigma n,m \Rightarrow \exists \boldsymbol f' ((\boldsymbol f')^H(n) \land \boldsymbol f' =_m \boldsymbol f)) $
6/ $\forall\boldsymbol f \forall n \forall m \space (\boldsymbol f^D(m) \land \sigma n,m \Rightarrow \boldsymbol f^D(n)) $
7/ $\forall \boldsymbol f \forall i \forall c (\boldsymbol f^D(i) \Rightarrow \exists \boldsymbol f' (\boldsymbol f'(i) = c \land \boldsymbol f' =_i \boldsymbol f))$
Now 1/ through 7/ are sufficient to prove:
(UNIQUENESS) $\forall k \forall n \forall \boldsymbol f \forall \boldsymbol g (Img(\boldsymbol f) = Img(\boldsymbol g) \land Injection(\boldsymbol f) \land Injection(\boldsymbol g) \land \boldsymbol f^H(k) \land \boldsymbol g^H(n)\Rightarrow k = n)$,
where
$ Img(\boldsymbol f) = Img(\boldsymbol g) $ abbreviates $\forall y(\exists x \space \boldsymbol f(x,y) \iff \exists x \space \boldsymbol g(x,y))$ and
$Injection(f)$ abbreviates $\forall x \forall y (\boldsymbol f(x) = \boldsymbol f(y) \Rightarrow x = y)$
(Indeed I would claim 1/ through 7/ are sufficient to develop a satisfactory arithmetic.)
My question is: Is there a model in which 1/ through 6/ (i.e. eliminate 7/) are true but in which UNIQUENESS is false?
NOTE. Let $\phi (k)$ abbreviate
$\forall n \forall \boldsymbol f \forall \boldsymbol g (Img(\boldsymbol f) = Img(\boldsymbol g) \land Injection(\boldsymbol f) \land Injection(\boldsymbol g) \land \boldsymbol f^H(k) \land \boldsymbol g^H(n)\Rightarrow k = n)$
Then using only 1/ through 6/ I can prove $\phi(1)$ and, for any $k$, $\forall x_1,x_2,...,x_k (\sigma 1,x_1 \land \sigma x_1,x_2 \land \space ... \space \land \sigma x_{k-1},x_k \Rightarrow \phi (x_k)) $
UNIQUENESS however of course is $\forall k \phi (k)$, and this I cannot prove, hence my question.
