Why might Dieudonne have been "begging the question" by appealing to second-order Peano Axioms?
By "In saying that Peano arithmetic is univalent", they assert that there is only one model of Peano arithmetic (up to isomorphism). But this is not the case, since there are nonstandard models of arithmetic. However second-order Peano axioms are categorical. So the assertion makes sense if they had in mind a second-order axiomatization. But let's take a look at the following commentary by Mathias:
My reading of all these extracts is that Bourbaki had grasped the positive worth of the work of Hilbert and his school, and welcomed the idea of the reduction of the question of correctness of mathematics to a set of rules, but nevertheless persisted, even after Gödel’s work showed that Hilbert’s program could never be completed, in thinking of logic and set theory as stuff one settled in Volume One and then forgot about.
So basically, by finding their way to the uniqueness of true arithmetic, he interprets this appeal to second-order axioms as negating all the subtleties introduced by the incompleteness, equating "true" and "provable". While this erroneous view can still somehow work when thinking about arithmetic, it fails miserably when applied to set theory, which makes the position fairly untenable. The author then goes on to explain that this mathematical misconception found its origin in French philosophical tradition.
But whatever the reason, the fact remains that they did not accommodate Gödel’s incompleteness theorems in their view of mathematics: and no sociological or psychological explanation of Bourbaki’s resistance to Gödel’s insights can resolve the mathematical and philosophical difficulties presented by Gödel’s work to believers in Hilbert’s programme.
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.
Comment to Graffitics's answer.
The quote is from:
- Nicolas Bourbaki, L'architecture des mathematiques, into François Le Lionnais (ed.), Les grands courants de la pensée mathématique (1948), page 45. See Engl.transl., page 35.
The issue is not (according to my understanding) about first-order vs second-order axiomatization.
Bourbaki is discussing the (seminal) notions of méthode axiomatique and of structure:
page 40 - Engl.transl., page 28 - On peut maintenant faire comprendre ce qu'il faut entendre, d'une façon générale, par une structure mathématique. [...] Faire la théorie axiomatique d'une structure donnée, c'est déduire les conséquences logiques des axiomes de la structure, en s'interdisant toute autre hypothèse sur les éléments considérés (en particulier, toute hypothèse sur leur «nature» propre).
page 41 - Les relations qui forment le point de départ de la définition d'une structure peuvent être de nature assez variée. Celle qui intervient dans les structures de groupe est ce qu'on appelle une «loi de composition», c'est-à-dire une relation entre trois éléments déterminant le troisième de façon unique en fonction des deux premiers. Lorsque les relations de définition d'une structure sont des «lois de composition», la structure correspondante est appelée structure algébrique.
page 43 - Guidés par la conception axiomatique, essayons donc de nous représenter l'ensemble de l'univers mathématique. Certes, nous n'y reconnaîtrons plus guère l'ordre traditionnel, qui, tel celui des premières nomenclatures des espèces animales, se bornait à ranger côte à côte les théories qui présentaient le plus de ressemblances extérieures. Au lieu des compartiments bien délimités de l'Algèbre, de l'Analyse, de la Théorie des Nombres et de la Géométrie, nous verrons, par exemple, la théorie des nombres premiers voisiner avec celle des courbes algébriques, ou la géométrie euclidienne avec les équations intégrales; et le principe ordonnateur sera la conception d'une hiérarchie de structures, allant du simple au complexe, du général au particulier.
In this context we have to read the final remark about:
page 45 - Engl.transl., page 35 - les premières axiomatisations, et qui eurent le plus de retentissement (celles de l'arithmétique avec Dedekind et Peano, de la géométrie euclidienne avec Hilbert) portaient sur des théories univalentes, c'est-à-dire telles que le système global de leurs axiomes les déterminait entièrement, et n'était 'par suite susceptible de s'appliquer à aucune théorie autre que celle d'où on l'avait extrait (au rebours de ce que nous avons vu pour la théorie des groupes, par exemple).
Dedekind-Peano axiomatization, as well as Euclid-Hilbert's one, aims at the "univocal characterization" of its intended structure.
According to Bourbaki's point of view, the "general" notion of structure is mathematically more interesting and fruitfully.
Note
Mathias' concern about the meager attention by Bourbaki regrading mathematical logic is correct; see:
page 37 - Engl.transl., page 25 - toute théorie mathématique est un enchaînement de propositions, se déduisant les unes des autres conformément aux règles d'une logique qui, pour l'essentiel, est celle codifiée depuis Aristote sous le nom de «logique formelle», convenablement adaptée aux buts particuliers du mathématicien. C'est donc un truisme banal de dire que ce «raisonnement déductif» est un principe d'unité pour la mathématique [...]. Le mode de raisonnement par enchaînement de syllogismes n'est qu'un mécanisme transformateur, applicable indifféremment à toutes sortes de prémisses, et qui ne saurait donc caractériser la nature de celles-ci. [...] Codifier ce langage, en ordonner le vocabulaire et en clarifier la syntaxe, c'est faire œuvre fort utile, et qui constitue effectivement une face de la méthode axiomatique, celle qu'on peut proprement appeler le formalisme logique (ou, comme on dit aussi, la «logistique»). Mais - et nous insistons sur ce point - ce n'en est qu'une face, et la moins intéressante.
As noted by Mathias, Bourbaki (in 1948) seems totally unaware of Gödel's results of 1931 regarding the incompleteness of arithmetic and of 1940 regarding the consistency of the Continuum Hypothesis and the Axiom of Choice and their impact with the subsequent development of mathematical logic as a mathematical discipline: model theory, set theory, computability, etc.