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$+ $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.