Path: utzoo!utgpu!attcan!uunet!husc6!linus!spdcc!bloom-beacon!NRL-CSS.ARPA!mclean
From: mclean@NRL-CSS.ARPA (John McLean)
Newsgroups: comp.ai.digest
Subject: Are all Reasoning Systems Inconsistent?
Message-ID: <19880805041434.7.NICK@HOWARD-JOHNSONS.LCS.MIT.EDU>
Date: 5 Aug 88 04:14:00 GMT
Sender: daemon@bloom-beacon.MIT.EDU
Organization: The Internet
Lines: 38
Approved: ailist@ai.ai.mit.edu

Date: Tue, 26 Jul 88 10:42 EDT
From: John McLean <mclean@nrl-css.arpa>
To: AIList@AI.AI.MIT.EDU
Subject: Are all Reasoning Systems Inconsistent?

In AIList vol 8. issue 23, Jonathan Leivent presents the following argument
where P(x) asserts that the formula with Godel number x is provable
and the Godel number of S is n where S = (P(n) -> A):

   >1.  S = (P(n) -> A)
   >2.  P(n) -> S
   >3.  P(n) -> (P(n) -> A)
   >4.  P(n) -> P(n)
   >5.  P(n) -> (P(n) ^ (P(n) -> A))
   >6.  (P(n) ^ (P(n) -> A)) -> A
   >7.  P(n) -> A
   >8.  S
   >9.  P(n)
   >10. A

What Jonathan is pointing out was proven by Tarksi in the 30's:  a theory
is inconsistent if it contains arithmetic and has the property that for
all all formulae A we can prove P("A") --> A, where "A" is the Godel number
of A.  [Tarski actually proved the theorem for any predicate T such that
T("A") <--> A, but it is easy to show that the provability predicate P
has the property that A --> P("A").]  This is not so strange if we
realize that P(n) is really an existential formula (Ex)Bew(x,n),
where Bew(x,y) is derivable iff x is the Godel number of a proof whose
last line is the formula whose Godel number is y.  It follows that if y
is the Godel number of a theorem then Bew(x,y) is derivable and hence,
so is P(n) by existential generalization.  However, the converse is false.
(Ex)Bew(x,y) may be derivable when the formula corresponding to y is not.
In other words, arithmetic is not omega-complete.  This does not affect our
proof theory, however, beyond showing that we cannot have a general proof
rule of the form P("A") --> A.  We can assert P("A") --> A as a theorem
only when we derive it from the basic theorems of number theory and logic.

John McLean