Ever since I have read about both Gödel's incompleteness theorem(s?), which I believe roughly means: "A system at least as strong as Peano arithmetic cannot prove its own consistency." and learned about other possible, weaker, foundations for mathematics, like Bishop's constructive mathematics I have been wondering about the following question:
Is there a reasonably strong foundation for mathematics that can prove its own consistency?
Reasonably meaning: It can formalize a sort of real analysis, linear algebra, abstract algebra, graph theory, category theory, theoretical computer science and so on and so forth.
I am NOT searching for foundations with classical logic; I am "willing to sacrifice" axioms / rules of inference, even structural rules, like the "Weakening rule" until only very "trivial" rules remain (like $\wedge$-Introduction or $\rightarrow$-Elimination).
Real analysis for instance does not have to be like the real analysis we know from classical mathematics, but whatever "flavor" of analysis could work in such a system, even if it appears to be "broken".
The arithmetic should not be the Peano arithmetic (or even Heyting arithmetic), but an arithmetic, such that the "Gödel-theorem" in question fails to be a theorem, like the arithmetic on logic R:
"Relevant logic has been used as the basis for mathematical theories other than set theory. Meyer has produced a variation of Peano arithmetic based on the logic R. Meyer gave a finitary proof that his relevant arithmetic does not have 0 = 1 as a theorem. Thus Meyer solved one of Hilbert's central problems in the context of relevant arithmetic; he showed using finitary means that relevant arithmetic is absolutely consistent. This makes relevant Peano arithmetic an extremely interesting theory. Unfortunately, as Meyer and Friedman have shown, relevant arithmetic does not contain all of the theorems of classical Peano arithmetic. Hence we cannot infer from this that classical Peano arithmetic is absolutely consistent (see Meyer and Friedman 1992)." - http://plato.stanford.edu/entries/logic-relevance/
Hence, a further question is:
Does (or could) a type of relevant logic with some kind of set theory or type theory provide such a foundation?
Of course, I do not expect, that such a theory has all the theorems of Peano arithmetic; instead I would expect that there "relevant versions" of classical theorems, like $\epsilon$-trichotomy is the constructive analysis version of regular trichotomy.
Although I am interested in this topic I should mention, I am not a logician or an undergraduate in mathematics, therefore I humbly request an answer in rather simple terms.