Logic in maths foundation I'm not very keen on mathematical logic, but really want to study it. And as I know any try of maths foundation was using mathematical logic, so is it something that we always have as an "axiom" in maths foundations ? And do we always take the same logic for "axiom", I mean there is first-order logic, second-order logic, propositional logic (maybe I am messing up with classification, so sorry for that, I know a little about mathematical logic) ? Can be my question is not very clear, sorry for that, if it is so I will try to make it clearer. Thanks in advance. 
 A: Let me answer one particular interpretation of your question:

To what extent is there an agreed-upon logical framework for mathematics - and to the extent to which there is one, what distinguishes it?

(I write "what distinguishes it" deliberately: it is quite possible for something to be adopted initially for one reason, and then for other more convincing features of it to come to light later. I suspect you're less interested in the historical reasons than you are in the current analysis, although correct me if I'm wrong.)
There are several responses to this question. "One level up," there is the well-worn discussion over the role of ZFC as the "standard" axiom system within which mathematics takes place, including the following important observations:

*

*Most working mathematicians cannot list the ZFC axioms.


*As a matter of practice, the ZFC axioms are almost always much more powerful than anything we actually need.


*That said, the ZFC axioms provide an incredibly powerful framework for analyzing principles of high consistency strength, and in light of Godel's theorem (and subsequent work, including work of Friedman) we should be interested in ways to study such principles.


*ZFC has a reasonable claim to relative usability amongst similarly powerful systems, although that is being challenged by e.g. homotopy type theory.


*And many others (and you can find further discussion of this topic throughout this site, including this old question).
But I think you're asking something more fundamental - about the specific logic we use to formalize mathematics in the first place. Here there are, I think, two main "axes" along which we can make decisions:

*

*Expressive power. In my opinion, one of the most important "primordial" observations in mathematical logic is that propositional logic is not enough to do anything useful. While simple syllogisms are of course important, mathematics talks about objects and fundamentally uses quantification, and neither of these are things propositional logic can handle. First-order logic emerges as one candidate; the obvious alternative is second-order logic. In a precise sense, third-order logic is reducible to second-order logic, so this seems to be the main distinction. There are of course additional options, but I'd say that these two are the most important ones.


*The nature of truth. Or, more accurately, of truth values. "Classical" logic adopts at the very beginning the idea that there are two truth values, "True" and "False," and that they interact via the logical connectives in certain specific ways - most importantly, that the law of the excluded middle holds. There are many alternatives to this, including intuitionistic logic, paraconsistent logic, many-valued logic, etc. Importantly, the "truth question" emerges even before the "expressiveness" question: it's already present in propositional logic. One possible response to this is that we should first resolve this question before moving on to the previous one; a reasonable objection is that our analysis of the structures we are trying to express facts about will inform our understanding of truth. (Incidentally, along these lines I recommend Humberstone's epic tome "The Connectives".)
Both of these inspire huge debates, which this answer box can't adequately cover. Let me say a very brief bit about the situation as I see it, beginning with my understanding of the convention which emerged:

By and large, mathematicians adopt classical first-order logic; we work inside the first-order theory ZFC, which lets us talk about higher-order concepts in a first-order way.

Or rather, this is the foundational framework which emerged around mathematical practice, and has so far proved sufficient and the norm within the foundationally-interested community.
The adoption of classical logic, I think, is most firmly ingrained: it reflects ideas about truth which the majority of the mathematical community hold. Of course this is not to say that we present a unified front here, only that it seems to be the great majority view. Note that this point is widely recognized and accepted by working mathematicians, via the common acceptance of proof by contradiction.
The adoption of first-order logic is more technical (although of course the debate around it is more narrow in audience and scope, while in my opinion no less fundamental). The main issue with first-order logic, I think, are the limits on its expressive power provided by the compactness theorem and the Lowenheim-Skolem theorem. Within logic these has come to be seen largely as positive features; in particular, compactness is necessary for us to have a good notion of "proof." Lindstrom's theorem then isolates first-order logic as a maximal logic with these properties, and this forms I think a strong basis for adopting it rather than second-order logic. Debates about the problems inherent in second-order logic can be found in many places; in particular, Quine, Shapiro, and Vaananen are good names to search for.

Finally, let me end by saying that this paper of Ferreiros may be of interest to you: The Road to Modern Logic - An Interpretation, The Bulletin of Symbolic Logic, Vol. 7, No. 4 (Dec., 2001), pp. 441-484. Author's website, ASL, JSTOR, DOI: 10.2307/2687794.
