The mathematics community at large seems pretty satisfied right now with the common practice of 1. starting with some axioms and 2. deriving theorems from them by employing some logic. All mathematics is done like this (as far as I know).

Here's the problem I see with this, specifically in the logic part (although I'm not so confident that I can explain it clearly). In defining a logic, you say things like, "A theory T is called a formal theory, if and only if there is an algorithm allowing to verify, is a given text a correct proof via principles of T, or not" (I just copied that from a webpage, so don't worry about the details). I'm focusing specifically on the "if and only if" part. What does "if and only if" mean, logically (i.e. how do I apply it)? Well, It means different things in different logics (our common notion of it changes especially in paraconsistent logics). So do words like "and," "or," and "is." For example, in our daily speaking language when we say "the light is on," we would consider that equivalent to "the light is not off." Not so if we were using a paraconsistent logic. So why assume, in important definitions such as the above, that we are using some agreed upon logic (the logic people normally assume is Aristotelian logic, which assumes the law of non-contradiction and the law of the excluded middle).

Here's my attempt to say it in one sentence with commentary: Using a logic (i.e. applying it to axioms to derive theorems) necessarily entails using another logic (not necessarily the same as the other one) that is not formally defined (it's not that you can't formally define it, but that you are not using it formally but casually, assuming that Aristotelian logic is the "right logic").

Thus, if I applied a logic to some axioms using a paraconsistent logic (which allows contradictions to a degree) instead of Aristotelian logic, a different theory would emerge.

I guess it seems to me that logic is so embedded in our natural language that it's impossible to define a truly "formal" logic in the sense that it does not assume anything (which is precisely what mathematicians have desired to do); even a formal logic assumes the casual use of another logic.

aboutthe theory, you just reasoninthe theory. You thus don’t need any of the mathematical logic machinery which treats theories asobjectsand studies their general properties. You only need to be able to recognize a valid proof, i.e., to be familiar with the axioms and derivation rules (“proof techniques”) of your theory. $\endgroup$ – Emil Jeřábek Oct 25 '12 at 10:59