I just finished reading a McFarlane's article in the newest Synthese, about neo-Logicism. He argues that the ideas which Wright and Hale put forward in favor of our license to adopt Hume's principle as a stipulation, would seem to equally support just directly laying down the axioms of PA.
This seems 100% right to me, and it occurs to me that my thesis proposal about how a priori knowledge is possible, can be seen as taking this strategy.
However, I wouldn't say that we literally do stipulate the axioms of PA (would anyone say this? I mean it seems like an obvious psychological/historical fact that people generally don't make any such stipulation). Rather, we come to find these statements (and others obvious) which then functions like a stipulation in that it helps determine the meaning of our words in such a way as to make it likely that these statements we find obvious will express truths.
Just saying this doesn't completely dispel worries about the epistemology of math though. For not all stipulations are OK - some stipulations, like those for "tonk" would not lead to a practice that counted as reliable reasoning. So there are two remaining questions.
1. Given that some stipulations are bad, how do we manage to make good stipulations so often?
2. Given that some stipulations are bad, how can we be justified in making any stipultion?
I think the answer to 1 is a combo of quinean/millian theory revision with a nudge from nature, together with facts about the relative profusion of abstract objects as targets for our stipulations.
I think the answer to 2 is that we can't help but start from what we find obvious and reason in ways that seem compelling, so we have prima facie warrant to do this - in the absence of any reason to think to doubt that these feelings of obviousness could be reliable in a given sphere.