Why mathematicians would prefer at times to work with inconsistent systems (from which I assume everything can be proven unless changing the logic used)? In particular, how could working with an inconsistent system be useful or advantageous? What kind of a philosophy of mathematics could justify an appeal to inconsistent mathematics? And what's the relation between inconsistent mathematics and the foundations of mathematics? Is it the case that appealing to inconsistent mathematics means embracing for good "mathematics without foundations"?
Let me first address the issue of foundations, for a recent review see Azzouni's Is there still a Sense in which Mathematics can have Foundations? There is of course a legacy label "foundations of mathematics", which covers things that came out of foundational programs of early 20th century, like mathematical logic and the axiomatic method. There are even new "foundational" proposals like neologicism, or most recent univalent foundations of Voevodsky, see Are Univalent Foundations of mathematics a modern version of logicism? (they are closer to constructivism).
All of these use "foundations" in a Pickwickian sense that has only historical family resemblance to the philosophical meaning of the word. The idea is to give comprehensive expositions of mathematics from a refreshing/fruitful perspective, not to provide it with a philosophical justification a la Kant or Frege, nor to reduce it to composites of "true" elements a la Bourbaki. Defenders of one "true" set theory are few, and of its role as an ultimate justifier, even fewer. Heck, a neologicist, openly disclaims that "the attractions... do not depend upon the claim that the various instances of Hume’s Principle are logical truths, analytic truths, or any such thing", see The Julius Caesar Objection.
Priest, the father of modern dialetheism, is proposing paraconsistent "foundations" of mathematics in this aesthetic sense, and arguing for them on pragmatic grounds. His Is Arithmetic Consistent? is a review of promised attractions. He starts with a Wittgenstein inspired undermining of the naive idea that our arithmetic is "intuitively" consistent. Imagine two users of arithmetic, α and β, one consistent, the other paraconsistent. The paraconsistent one is called M, and has a (very large) largest number n=n+1:
"As Wittgenstein demonstrated, any determinacy there is in the notion of rule-following is to be grounded in the fact that we have dispositions to proceed in a socially universal (or at least, pretty common) way. Both α, β proceed in the same way for all actual situations. The divergence between them could appear only in situations that transcend anything humanly possible. What makes one think that in such situations one would behave like α rather than β? Our knowledge of how we would proceed in hypothetical situations is notoriously unreliable. Even worse, it is not even clear that there is any fact of the matter here."
Then he points out that paraconsistency wipes out all the unpleasant classical meta-theorems (incompleteness, unprovability of consistency, undefinability of truth, etc.) in one fell swoop:
"The hope that we might have a decision procedure to solve mathematical problems goes back, at least, to Leibniz... if M is the correct arithmetic, there exists just such a decision procedure (and a very simple - though exponential - one at that).
Let us move on to Tarski's Theorem: classical arithmetic cannot contain its own truth predicate... Unsurprisingly the issue of the solution to the semantic paradoxes, and especially the Liar Paradox, is raised here. The fact that we cannot have a unified account of numbers and truth means that a Tarskian "metalinguistic" solution to the paradoxes must ultimately be endorsed. This is highly problematic, as many have noted. By contrast, M provides a clean and simple solution [the Liar is both true and false]."
One can try to enlist Hegel's and Wittgenstein's support here, see Can paraconsistent or other logics make the impossible happen? And Priest's seductions do not stop there. Next he promises to vindicate the Hilbert's program of finitary justification that we all thought was killed off by Gödel. But not so fast:
M puts the whole situation in a quite different light. First, M can be axiomatised. Secondly, as (viii) of § 1 tells us, any non-theorem of M can be shown in M to be a nontheorem. In particular, any untrue (in the interpretation of M) finitary statement can be shown not to be provable. Moreover, since M is decidable, the methods used are strictly finitary. So is Hilbert's Programme vindicated? Maybe, maybe not. First, some true finitary statements in M, and in particular, some equations turn out to be inconsistent (have true negations). Hilbert might not have been too happy about this, though if M is true arithmetic, this unhappiness can legitimately be set aside."
Be it as it may, I do not expect that M will have many takers, any more than Lewis's modal realism, which offers similar semantic benefits in modal logic. There is just too much incredulity to get over to take either one of them seriously (as Lewis and Priest are well aware of). Priest's take on the rule-following skepticism might be too skeptical for most, the unified truth predicate loses much of its glamor when true contradictions are around, and Hilbert's unhappiness would be widely shared, I suspect. At present, there are also problems on the technical side, as Beziau points out in Are paraconsistent negations negations?
"Certainly until now, no paraconsistent negations having "nice" features have been presented. By "nice", we mean having interesting mathematical properties together with a coherent intuitive interpretation. That does not mean that there are no such things, but at least they have not been discovered yet. The present investigations do not permit one to be very optimistic about the chance to discover such things, since many classical techniques of mathematical logic, such as logical matrices, possible world semantics, sequent calculus, etc., have been applied - not in a real systematic way, it is true - without success."
Let's start with the basics. For millennia, mathematics was about the formal structure, the axioms, but it's more than that. It includes the rules of inference, which spent most of the time since Euclid untouched, unexamined. It's almost a truism that, when we look hard and objectively at what we have taken for granted, we learn something. Geometry expanded considerably when people got brave enough to ditch Euclid's parallel postulate, and the geometry that grew from that is what we use today.
Naive set theory was the beginning of set theory. It can be expressed informally. It's intuitive and easy to understand. It could be a common-sense basis for almost all mathematics. It has one very large problem: it leads to Russell's paradox. Modern formal set theory has to dodge around this in some mostly ad hoc fashion.
So, what would we need to keep naive set theory? Russell's paradox is a reductio ad absurdam. What happens if we remove that, and related things, from the rules of inference we use? What's left, and how useful and/or interesting is it?
We haven't removed all of mathematics, as it turns out. Proofs need to be constructive, not based on contradiction. Cantor's diagonalization works to show that the reals are uncountable, because it gives instructions on how to construct a new real number that's not in the list. Russell's paradox is not constructive. Neither is Goedel's incompleteness theorem. What's left of mathematics turns out to be quite fruitful.