Is there a reasonably strong foundation for mathematics that can prove its own consistency?

Question

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.

EDIT:

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/

EDIT end.

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.

Answer 1

If we consider a first order theory $T$, capable of arithmetic, consistent, and recursive, Gödel's Second Incompleteness Theorem shows that if $T \not \vdash con(T)$ (in classic first order logic). As Zhen Lin pointed out, making our deductive system weaker means that our consequences will be a subset of our original consequences. Hence, if we view $T$ is a weaker deductive system (e.g. intuitionistic logic), clearly, $T \not \vdash Con(T)$.

Do there exist systems that do prove there own consistency? Yes. $Th_L(\mathbb{N})$ does (where $L = \{+,\times,0,1\}$) however it is not recursive. (However, you must believe that $Th(\mathbb{N})$ is consistent for this happen, which most people do)

Do there exist (consistent) systems that are recursive and prove there own consistency? Yes. (See http://en.wikipedia.org/wiki/Self-verifying_theories). However, this does not contradict Gödel's Second Incompleteness Theorem. These systems are incredibly weak and do not fully "comprehend" arithmetic. This is what I believe you are actually looking for.

According to the wikipedia page, proving the totality of multiplication is not possible. Let's suppose that $S$ is one of these theories. Then, $S \not\vdash (\forall x \forall y \exists z)(x\cdot y=z)$. Therefore, while we can find some $S \vdash con(S)$, $S$ does not know that there exists an element which is the product of any two arbitrary elements.

So while there are systems which can prove their own consistency, there are no "reasonable and foundational" first order theories which do so. That's why Gödel's Theorems are so important. Any time we attempt to avoid them, we lose so much foundational information that the trade off just doesn't seem worth it. As for myself, I am comfortable in assuming that the natural numbers $are$ consistent until proven otherwise.