Following a comment by Peter Smith, I've been reading A. R. D. Mathias's paper The Ignorance of Bourbaki.
Parts of the paper are above my head, but I understand it well enough for my own amateurish purposes - apart from one sentence.
The context is a quotation from Dieudonne's A Panorama of Pure Mathematics (1982):
The first axiomatic treatments (Dedekind-Peano arithmetic, Hilbert Euclid geometry) dealt with univalent theories , i.e. theories which are entirely determined by their complete system of axioms, unlike the theory of groups.
Mathias's commentary on this passage ends with the following sentence, which baffles me:
In saying that Peano arithmetic is univalent, Bourbaki probably has in mind some second-order characterisation of the standard model of arithmetic, which is, of course, to beg the question.
I can only imagine that he means that even the second-order axioms cannot stand on their own, because any such version of the Peano Axioms has two hidden prerequisites:
Reference to a particular (but unmentioned) version of set theory.
Reference to a "standard model of arithmetic", whose existence and uniqueness is silently taken for granted (thus "begging the question" in a simpler sense than item 1).
But neither of these ideas is really clear to me, nor do I have any idea whether the author is alluding to either of them, both of them, or neither.
(When one is confused, it is hard to explain the precise way in which one is confused!)
If the meaning of the quoted sentence is not obvious to others, I'll consider asking the author himself about it via e-mail, but I'm marginally less nervous about posting a question here - and perhaps an answer to the question here will also interest others.
The paper is about Bourbaki's blind spot in relation to developments in logic since 1929. As my own blind spots are incomparably more severe than any of Bourbaki's, it is entirely possible that I will fail to understand a perfectly good explanation of the meaning of the above sentence!
But I will be well enough satisfied by an answer that reduces my current bafflement, by one sentence in an otherwise intelligible paper, to a more familiar perplexity about mathematics itself.
Second order PA (2oPA) is "univalent" aka categorical, in the strong sense that, when using standard, "full" 2nd order semantics, its only model is the standard model of arithmetic. The only thing "2nd order" about 2oPA is the induction axiom, which is no longer a schema but a single sentence which quantifies over all subsets. In "full" 2nd order semantics, "all subsets" really means just that, whereas in Henkin semantics, the 2nd order set quantifier ranges merely over the sets of the model, which form a collection that's closed under requisite operations (union, intersection, complement, projection, etc.) but which might not be the full powerset.
As you noticed, full 2nd order semantics implicitly references a background set theory — not a "version" of set theory, but actually a model $M$ of set theory (specifically, its powerset of $\omega$, $\mathcal{P}(\Bbb \omega)^M = \mathcal{P}(\Bbb \omega)\cap M$). However, the notion of a (/the) standard model of arithmetic is hardly controversial. If we can't agree on what is and isn't "in there", then we can't agree on much else, and we won't have a metatheory of anything.
Readers who liked the cited paper of Adrian Mathias also like his follow-up, A term of length 4,523,659,424,929. Abstract: Bourbaki suggest that their definition of the number 1 runs to some tens of thousands of symbols. We show that that is a considerable under-estimate, the true number of symbols being that in the title, not counting 1,179,618,517,981 disambiguatory links.