10
$\begingroup$

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:

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

  2. If such a system exist, could it possibly be a reasonable foundation for mathematics?

Improve this question
$\endgroup$
8
  • 7
    $\begingroup$ I don't know that anyone has worked this out, but I'd expect an analog of Gödel's second incompleteness theorem to apply to paraconsistent theories that can formalize enough of arithmetic. Such a theorem would be about nontriviality rather than consistency, since the former is the important desideratum for paraconsistent theories. The theorem I envision would say that a nontrivial, sufficiently strong theory cannot prove its own nontriviality. The proof should be rather similar to Gödel's proof for ordinary theories. $\endgroup$
    – Andreas Blass
    Commented Sep 30, 2016 at 17:19
  • $\begingroup$ I think the main reason to consider a paraconsistent logic, is Russell's paradox, or some other paradox. Since basic arithmetic does not have a paradox, a paraconsistent theory doing basic arithmetic will just be weaker than the related logic that has the explosion of absurdum. $\endgroup$
    – Lucas K.
    Commented Sep 30, 2016 at 18:27
  • $\begingroup$ @AndreasBlass: Are you sure? Paraconsistent logics are weaker than clasical logics (so as to avoid the inconsistency proving that every wff of the formal language in question is a theorem). For example, Priest's Logic of Paradox ($LP$) does not contain Modus Ponens. One can now ask of a given system of logic, "What are the rules of inference necessary to obtain Goedel's theorem (or your hypothetical analog of it)"? $\endgroup$
    – Thomas Benjamin
    Commented Oct 3, 2016 at 11:05
  • 3
    $\begingroup$ @ThomasBenjamin I though the first sentence of my comment made it clear that I'm not sure. Even if a result of the sort I envision were known or if its negation were known, I might well not be aware of it, since I pay practically no attention to paraconsistent logic. $\endgroup$
    – Andreas Blass
    Commented Oct 3, 2016 at 14:41
  • 6
    $\begingroup$ @ThomasBenjamin Fortunately, my conjecture included the slightly vague phrase "that can formalize enough of arithmetic". Not being a paraconsistent expert, I wouldn't want to try to make that phrase precise in the context of paraconsistent theories. Nevertheless, in view of the passages you quoted, I'm inclined to suppose that a theory with two-element models does not formalize enough of arithmetic. $\endgroup$
    – Andreas Blass
    Commented Oct 13, 2016 at 17:07

3 Answers 3

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
10
  • 7
    $\begingroup$ "There's basically no reason to think that ZFC is inconsistent." --- this is not a terribly strong argument. Are there positive reasons for thinking it's consistent? The fact that no inconsistency has been discovered is some evidence, although not as impressive as it seems, given that the vast bulk of modern mathematics can be formalized in much weaker systems. Does the system have a compelling philosophical coherence? Some would say yes, but I don't see it --- to me ZFC looks like a bit of a hodgepodge, an attempt to skirt the paradoxes without really understanding their source. $\endgroup$
    – Nik Weaver
    Commented Sep 30, 2016 at 19:49
  • 2
    $\begingroup$ The argument from large to small. Set theorists have added many additional axioms to ZFC. If ZFC was inconsistent, then these theories are also inconsistent, plus it should be easier to prove consistency. But set theorists have largely been unable to prove them inconsistent. Not only that, they seem to form a coherent picture and even answer questions in real analysis that are independent of ZFC (and give the nicest possible answer). $\endgroup$
    – arsmath
    Commented Oct 1, 2016 at 20:20
  • 3
    $\begingroup$ @ThomasBenjamin Sure, but I cannot express the level of certainty I have that Nelson is wrong. I am more certain that PA is consistent than I am that a person named Ed Nelson existed, or that a place called Princeton exists, or even that you exist. I would put my certainty about PA below my certainty that I exist, but only by a little bit. $\endgroup$
    – arsmath
    Commented Oct 13, 2016 at 12:40
  • 2
    $\begingroup$ That said, a paraconsistent foundation for some fragment of arithmetic is a perfectly worthy research goal. $\endgroup$
    – arsmath
    Commented Oct 13, 2016 at 12:41
  • 2
    $\begingroup$ Another argument for ZFC's consistency are the reflection principle(s). In my view they prove that ZFC is "as consistent as it possibly can be without violating Gödel's theorem". I would even go so far as to say that it is a nontrivial mental exercise to precisely find out why the reflection principle doesn't actually prove consistency. Or put in another way: To someone who isn't familiar with the finer points of logic the reflection principle seems just as good as a true proof of consistency. $\endgroup$
    – Johannes Hahn
    Commented Nov 20, 2016 at 13:01
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Again, why the downvote? $\endgroup$
    – Thomas Benjamin
    Commented Jan 12, 2022 at 21:18
  • $\begingroup$ For some reason, posts about certain regimes of set theory or category theory seem to pick up a phantom downvote or two on MO. Methinks there are some readers with a distaste for the subjects, and occasionally a post will tread across a toe more forcefully than others and earn a downvote. (i consider them a badge if honor on questions/answers that are otherwise well received, like this one; we have successfully aggravated a hater) $\endgroup$
    – Alec Rhea
    Commented Feb 28, 2022 at 4:35
  • $\begingroup$ I once got a downvote on a well-received question and all of its answers (also otherwise well received answers lol) $\endgroup$
    – Alec Rhea
    Commented Feb 28, 2022 at 4:40
5
$\begingroup$

Zach Weber has been working on developing a paraconsistent set theory that can serve as a foundation for mathematics.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .