[Math] Since an inconsistent system can prove its own consistency…

formal-prooflo.logic

Say a proof for the consistency of a formal system (proved within the formal system) is known. There are two possible cases: 1. the formal system is consistent and it can be and has been proven to be, or 2. the formal system is inconsistent (i.e. contains a contradiction), thus anything is provable, hence the proof of its consistency.

Is there a way to determine whether 1 or 2 is the case?

Best Answer

Gödel's Incompleteness Theorem says that if a system is

  • consistent,
  • recursively axiomatised and
  • adequate for arithmetics

then it is cannot prove its own consistency.

If your formal system can prove its own consistency, it must either

  • be able to prove anything, eg that $0=1$, or
  • be (consistent,) recursively axiomatised and adequate for arithmetic.

So the question comes down to whether you can prove $0=1$ in it.

In general this is undecidable.

Indeed, this is exactly the Entcheidungsproblem, if I recall correctly.

Related Question