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?

  • 1
    $\begingroup$ You can demonstrate 1) by demonstrating a model, or 2) by demonstrating a proof of a contradiction. $\endgroup$ – Steven Landsburg Apr 11 '13 at 13:40
  • $\begingroup$ Steven, could you elaborate a bit on what you mean by demonstrating a model? $\endgroup$ – supernaturalgospel Apr 12 '13 at 3:59

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.

  • 6
    $\begingroup$ Erm, I think you mean must be either not RA or inadequate for arithmetic $\endgroup$ – Richard Rast Apr 11 '13 at 13:38
  • $\begingroup$ What I was thinking was that if the system is clever enough to provide proofs that are not obviously nonsense then it must at least be able to do arithmetic. That's not quite a theorem as it stands but maybe with a bit of imagination you could turn it into one. $\endgroup$ – Paul Taylor Apr 11 '13 at 13:45
  • $\begingroup$ I believe there are very simple theories which can prove their own consistency, but which are not adequate for arithmetic (and are believed to be consistent). I'm blanking on an example right now though. $\endgroup$ – Richard Rast Apr 11 '13 at 14:39
  • $\begingroup$ (There is a typo, as indicated by Richard's first comment.) $\endgroup$ – Andrés E. Caicedo Apr 11 '13 at 15:14
  • 2
    $\begingroup$ @Richard: In mathoverflow.net/questions/55311/… there is a link to a brief explanation of self-verifying theories, and a list of references, including the nice work of Dan Willard on this subject. $\endgroup$ – Andrés E. Caicedo Apr 11 '13 at 15:17

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.