Path: utzoo!attcan!uunet!husc6!bloom-beacon!XN.LL.MIT.EDU!jon
From: jon@XN.LL.MIT.EDU (Jonathan Leivent)
Newsgroups: comp.ai.digest
Subject: Are all Reasoning Systems Inconsistent?
Message-ID: <19880807031833.2.NICK@HOWARD-JOHNSONS.LCS.MIT.EDU>
Date: 7 Aug 88 03:18:00 GMT
Sender: tytso@bloom-beacon.MIT.EDU
Organization: The Internet
Lines: 37
Approved: ailist@ai.ai.mit.edu

Date: Fri, 5 Aug 88 15:52 EDT
From: Jonathan Leivent <jon@XN.LL.MIT.EDU>
Posted-Date: Fri, 5 Aug 88 15:52:04 EDT
To: AILIST@AI.AI.MIT.EDU
Subject: Are all Reasoning Systems Inconsistent?
cc: jon@XN.LL.MIT.EDU


A while ago, I posted a proof I had stumbled upon that seemed
to lead to inconsistencies.  After some more thought about
it, and after reading some replies, I dcided to reformulate
it.  Originally, I claimed that the construction of the
sentence S = P(n) -> A leads to a contradiction - what I meant
is that a particular sentence could be constructed in a reasoning
system such that the mere assertion of the existence of that
sentence leads to a contradiction.  I phrased the sentence as
indicated above because I had thought of it while reading
something about Lob's Theorem in a paper by Raymond Smullyan
in the 1986 conf proceedings of Theoretical Aspects of
Reasoning about Knowledge (title: "Logicians who reason about
Themselves" - an interesting paper for people into Godel's
theorem).  Anyway, I decided that the sentence I was interested
in was really:

(En)[P(n) = ~P(n)]

Where P(m) means "m is the Godel number of a theorem in this
reasoning system".  This theorem is actually a corollary of
Godel's theorem - it is proven by constructing the sentence
with Godel number n that satisfies the above theorem.  The thing
that bothers me is that the statement (En)[P(n) = ~P(n)] is
contradictory itself, yet obviously true (by construction).

I'm sorry about the delay in reposting: I was away from work for
a week.

-- Jon Leivent