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.
