3
$\begingroup$

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?

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

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
6
  • 6
    $\begingroup$ Erm, I think you mean must be either not RA or inadequate for arithmetic $\endgroup$ Apr 11, 2013 at 13:38
  • 1
    $\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$ Apr 11, 2013 at 13:45
  • 1
    $\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$ Apr 11, 2013 at 14:39
  • 1
    $\begingroup$ (There is a typo, as indicated by Richard's first comment.) $\endgroup$ Apr 11, 2013 at 15:14
  • 3
    $\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$ Apr 11, 2013 at 15:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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