Gödel theorems imply that arithmetic can not be complete under recursive axiomatization and consistency assumptions. Unexpectedly, consistency can be dropped in a meaningful way by switching to a paraconsistent logic that allows contradictions but blocks the law of explosion ("contradiction implies anything"). Such arithmetics can be complete, have the truth predicate definable within them, and admit a procedure for deciding truth/provability of sentences. But it gets better, "a consequence of Meyer's construction was that within his arithmetic R# it was demonstrable by simple finitary means that whatever contradictions there might happen to be, they could not adversely affect any numerical calculations". What puzzles me here is "finitary means". That presumably should be the same regardless of the logic used, yet R# proves consistency of numerical computations, which Peano arithmetic can not do (I think). What gives?
If I understand correctly, paraconsistent arithmetics divide arithmetical sentences into three categories: pure truths (provable and not disprovable), pure falsehoods (disprovable and not provable), and "Liar sentences" (both provable and disprovable). Gödel sentences come out as Liars, but at least in some arithmetics so do simple statements about very large numbers (what is "large" depends on a particular version). For instance, there might be a number $n$ that satifies both $n=n+1$ and $n\neq n+1$, and there is the smallest among them! But for smaller numbers they agree with Peano on everything. Is the trick that even if we prove a sentence we may not be able to tell if it is a pure truth or a Liar?
Are there "Peano complete" paraconsistent arithmetics, where every theorem of Peano arithmetic is a pure truth? Is it possible to have an arithmetic where the entire trichotomy is decidable, i.e. there is a procedure that decides whether a sentence is a pure truth, a pure falsehood or a Liar. I guess this would be a formalization of "completeness modulo Gödel sentences" but it sounds too good to be true. Can Gödel's argument be modified to show that there can be no such thing?
We use definition from the question:
to answer the question
For every formula $\phi$, the longer formula $E_\phi \equiv \lnot (\phi \land \lnot \phi)$ is a theorem of PA. In any inconsistent system, there is at least one $\phi$ such that $E_\phi$ is disprovable. Therefore, it is not possible for an inconsistent theorem to prove every theorem of PA while not disproving any theorem of PA.
Thus any paraconsistent system in which every theorem of PA is a pure truth must actually be consistent.