Do second-order categoricity proofs require a background concept of set?
Solution 1:
I'm glad to hear that you're reading my paper, and your question is interesting. (I just noticed your question now.)
My remark about the categoricity proofs requiring set theory applies equally whether you undertake the categoricity argument in second-order logic, which I view as a flavor of weak set theory, or plural logic, which has an essential set theoretic nature. The main point I am making in the remark is that it seems hopeless to base our confidence in the definiteness of concept of the finite by appealing to the set-theoretic realm (whether via a full set-theory or via second-order logic or plurals), since we would seem to have even less confidence in the definite nature of that realm. In other words, how can we base our confidence in the easy case on our knowledge about something much murkier? (See also this informal essay about it.)
But to answer your mathematical question at the end: yes, categoricity can depend on the set-theoretic background. One easy way to see this is that basic fact that different models of set theory can have different non-isomorphic natural numbers $\mathbb{N}$, even though each of these models believes that their version of $\mathbb{N}$ is characterized by the second-order Peano axioms. In a recent joint paper of Ruizhi Yang and myself, Satisfaction is not absolute, we provide several more striking examples. Namely, there can be different models of set theory $M_1$ and $M_2$, which agree on their natural number structures $\langle \mathbb{N},+,\cdot,0,1,<\rangle^{M_1}=\langle \mathbb{N},+,\cdot,0,1,<\rangle^{M_2}$, but they do not agree on arithmetic truth, in the sense that they have an arithmetic sentence $\sigma$ such that $M_1\models\mathbb{N}\models\sigma$ and $M_2\models\mathbb{N}\models\neg\sigma$. This can be construed as a dependence of categoricity on the set-theoretic background.
Here are a few other ways to show that categoricity can change with the set-theoretic background.
Let $t$ be the $L$-least Suslin tree with the unique branch property. Consider the theory $T$ asserting the elementary diagram of $t$ together with the assertion "$b$ is a branch through $t$", using a new predicate symbol $b$. In the forcing extension obtained by forcing with $t$, there is a unique branch through $t$, and the theory is fully categorical in that model (in second-order logic). But if one forces with $t$ again, then in that set-theoretic universe, the very same theory is no longer categorical, since there is a choice for the branch.
Similarly, in the countable context one can write down the theory that describes the natural number structure $\mathbb{N}$ plus the assertion that $Z$ is a predicate whose extension on $\mathbb{N}$ is exactly $0^\sharp$ (this is definable in second-order logic). This theory is categorical in second-order logic, if $0^\sharp$ exists, since there is ony one thing that will satisfy it, but it is not satisfiable at all if $0^\sharp$ does not exist. Or one could make the theory say that $Z$ is $0^\sharp$, if $0^\sharp$ exists, and otherwise anything. This is categorical if and only if $0^\sharp$ exists.