Is a paraconsistent and provably non-trivial foundation for math possible? Would it be possible to use a paraconsistent logic and axioms similar to ZFC to create a formal sytem, that can be proven to be non-trivial (so that there are some statements which can´t be proven in the system), and which can serve as a foundation for mathematics?
Because it´s possible that the current ZFC + first order logic foundation is inconsistent, and if it´s inconsistent then it would be completely trivial and worthless. And according to my understanding of gödel´s second incompleteness theorem it´s impossible to show that ZFC is consistent (at least without using a formal system that´s even more questionable). This means it´s impossible to prove that the current ZFC foundations are non-trivial, and the same holds for any other foundation that uses first order logic and contains basic arithmetic.
Naturally, I think it would be more desirable to have a foundation that is demonstrably non-trivial, than a foundation where we can´t possibly prove non-triviality. That´s why I wonder whether a paraconsistent foundation could be demonstrably non-trivial.
So basically I have two questions:


*

*Is it possible to have a non-trivial paraconsistent formal system containing basic arithmetic, whose non-triviality can be proven in "weaker" formal systems?

*If such a system exist, could it possibly be a reasonable foundation for mathematics?
 A: There's basically no reason to think that ZFC is inconsistent.  Even if it is inconsistent, there's an attractive fragment called Peano arithmetic, which seems self-evidently consistent to me.  Gödel's incompleteness still holds here, and it holds in even weaker fragments of arithmetic.  It's because as soon as you have a fragment of arithmetic large enough to do anything interesting, you can encode proofs as numbers in that arithmetic, and then you can derive Gödel's results.  This seems intrinsic to the nature of arithmetic to me -- proofs are strings of symbols that we can store in a computer, so of course we can represent it as a big number.
That said, people have attempted things in the direction you suggest.  One approach is what's called relevance logic.  There's a version of arithmetic for relevance logic that is provably non-trivial.  My impression is that it only captures a small fragment of arithmetic, though.  My link provides additional details, including references for relevance arithmetic.
A: Zach Weber has been working on developing a paraconsistent set theory that can serve as a foundation for mathematics.
A: One should note that as regards your question 1, systems of relevant arithmetic with inconsistent models such as $R{\sharp}$, $R{\sharp}{\sharp}$, and the systems $RM3^{i}$ can prove (with finitary proofs) their own non-triviality (see Friedman's and Meyer's paper "Whither Relevant Arithmetic",The Journal of Symbolic Logic, Vol. 57, No. 3(Sep., 1992), pp. 824-831; and Meyer's and Mortensen's paper, "Inconsistent Models for Relevant Arithmetics", Journal of Symbolic Logic, Vol. 49, No. 3 (Sep.,1984)).  Note also that (for example) that
$$
PRA+(\text{Quantifier-free Transfinite Induction up to }\epsilon_0)
$$
can prove the consistency of $PA$, but are incomparable in logical strength. Why then is it necessary that the nontrivial paraconsistent system that can serve as a foundation for mathematics have its non-triviality proven in a weaker formal system?
If one drops the criterion mentioned in question 1 (the proof of non-triviality of a paraconsistent system in a weaker formal system), there is a paraconsistent system in which one can develop standard set theory (and in so doing produces a paraconsistent foundation for mathematics).  This is the system Hyper-Frege ($HF$)+ 'There is an infinite well-founded set'  ($HF_{\infty}$).  $HF$  first appears in Thierry Libert's paper "$ZF$ and the Axiom of Choice in Some Paraconsistent Set Theories" (Logic and Logical Philosophy, Vol. 11 (2003), 91-114; and $HF_{\infty}$ appears in Olivier Esser's paper "A Strong Model of Paraconsistent Logic", Notre Dame Journal of Formal Logic, Vol 44, No. 3 (2003), pp. 149-156.  If one considers Esser's Theorem 3.2 (my comments will be in square brackets),

The theory $HF_{\infty}$ is mutually interpretable with $GPK^{+}_{\infty}$ which is also [equiconsistent with] $KM$ [Kelly-Morse class theory] + 'On is weakly compact'.  The theory $HF$ is mutually interpretable with $PA_2$ [second-order arithmetic--practitioners of Reverse Mathematics please take note].

one sees that $HF_{\infty}$ can serve as a foundation for most (if not all) modern mathematics, and that most ordinary mathematics can be interpreted and developed in $HF$.  It also should be noted that Esser's construction of a model for $HF_{\infty}$ shows that $HF_{\infty}$ is non-trivial.  It is unknown to me whether $HF$ or $HF_{\infty}$ can prove their own non-triviality.
