If someone can prove that one cannot prove from the axioms statement that is opposite to some true statement in the system, does it mean that this system is consistent ? For example, is proving that one cannot prove from the axioms of arithmetic that 0=1 enough for proving arithmetic is consistent ? I thought this is true because of the "principle of explosion".
Edit: possible proof why it is enough. If we can prove that within the system we can't prove some concrete statement "A" and "not A" at once than it means that there are no possibility of proving any other opposite statements "B" and "not B" at once, because if there was such a possibility, then by principle of explosion we could both prove "A" and "not A". So from the axioms we can't prove two opposite statements. Is it valid proof ?

  • 4
    $\begingroup$ Short answer: yes. $\endgroup$ – Wojowu Apr 8 '18 at 21:34
  • 1
    $\begingroup$ Slightly longer answer: yes, by definition: an inconsistent system is one in which every statement is provable. And, no, you don't have to close the question. $\endgroup$ – Rob Arthan Apr 8 '18 at 21:44
  • 1
    $\begingroup$ If you can prove $A \land \lnot A$ for any $A$ the system is inconsistent and you can prove $B \land \lnot B$ for every $B$. $\endgroup$ – Rob Arthan Apr 8 '18 at 21:51
  • 1
    $\begingroup$ @spaceisdarkgreen - in formal arithmetic we have the axiom: $\forall n \lnot (S(n)=0)$ and we define $1=S(0)$. Thus, from axiom we have : $\lnot (S(0)=0)$ i.e. $1 \ne 0$. So we have proved in first-order version of Peano arithmetic that $1 \ne 0$. The issue of proving the consistency of the theory is exactly to prove somehow that there is no proof of $1=0$, and this is not so easy. $\endgroup$ – Mauro ALLEGRANZA Apr 9 '18 at 7:29
  • 1
    $\begingroup$ The fact is that $\vdash (1 \ne 0)$ and $\nvdash (1=0)$ are not the same. IF we know that the theory $F$ is consistent, then from the fact that $F \vdash \lnot (1=0)$ is enough to conclude that $F \nvdash (1=0)$, but the issue is that we have to prove consistency. $\endgroup$ – Mauro ALLEGRANZA Apr 9 '18 at 7:30

Before we start just a little remark:

If someone can prove that one cannot prove from the axioms statement that is opposite to some true statement in the system, does it mean that this system is consistent?

If by system you mean a formal system made of axioms and inference rules for building proofs for theorems then you should not talk about truth: truth is a concept that has to do with interpretations/models not with proof systems.

With that said I guess that the answer to your question is no, allow me to explain why.

Assume that we have a formal system (i.e. a set of axioms and inference rules) in which you can formalize the syntax of the formal system you want to study. If we were able to prove inside this meta-system (meta-theory) that the theory object of study does not prove a contraddiction this would mean that, assuming that our meta-theory is consistent, the object theory is also consistent.

Unfortunately this move the problem to proving the consistency of the meta-theory so it does not resolve anything.

What is more, if we were able to use the same system as both the meta-theory and the object-theory then a result of self consistency, i.e. a proof inside the system of the system's consistency, would not solve the problem since inconsistent systems are able to prove everything including their consistency.

So the best results one can hope for are those in which we prove the consistency of a system in a meta-theory whose consistency we trust.

Hope this helps.

  • $\begingroup$ In case something is not clear or you have any question please ask. $\endgroup$ – Giorgio Mossa Apr 8 '18 at 22:50
  • $\begingroup$ And is it possible to prove consistency of a formal system just with logic ? In that case we don't need to prove that logic is consistent (or is it also possible ?). And as you said proving self-consistency doesn't works, so why anyone cares about second Gödel incompletness theorem ? $\endgroup$ – Юрій Ярош Apr 9 '18 at 6:58
  • $\begingroup$ About the first question: I suppose it depends on what kind of logic are you using. I doubt you can do that in first order logic because to prove formal consistency you need to have a theory stong enough to internalize (i.e. define in the language of the theory) the notion of formula and proof for the object theory, what's more you also need enough strength to prove statements about the system. Logic, meaning the first order theory in some language with no axiom at all, doesn't seem to have this power. $\endgroup$ – Giorgio Mossa Apr 9 '18 at 9:28
  • $\begingroup$ About the second question. You have to look at Gödel's incompleteness theorem with the eyes of a believer: Peano axioms are consistent because they have a model, natural numbers (whatever they are). The point is that Gödel's theorem prove that PA is an incomplete system, in particular there are formulas that are true in the model of the natural numbers but not in every model, hence they are not provable in PA. What's more any recusively axiomatizable system strong enough to prove PA consistency is incomplete. .....(continues ) $\endgroup$ – Giorgio Mossa Apr 9 '18 at 9:43
  • $\begingroup$ ....this means that that we cannot have a recursive set of axioms which is capable of proving all the formulas that are true in the model of natural numbers, i.e. the theory of natural numbers in not recursively axiomatizable. $\endgroup$ – Giorgio Mossa Apr 9 '18 at 9:44

An inconsistent system can prove anything (unless the logic is paraconsistent). Unfortunately, "proofs" of certain things being unprovable in a given system often assume the consistency of that system or another one. For example, "ZF can't decide AC" really should end with "if ZF is consistent".

  • $\begingroup$ OK, so if this proof is based on the consistency of other system B will it be enough for proving system A is consistent ? $\endgroup$ – Юрій Ярош Apr 8 '18 at 21:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.