Is such a proof enough for proving the system is consistent?

Question

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 ?

Answer 1

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.

Answer 2

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".