Path: utzoo!attcan!uunet!lll-winken!lll-tis!ames!pasteur!ucbvax!bloom-beacon!sbsvax.UUCP!yxoc
From: yxoc@sbsvax.UUCP (Ralf Treinen)
Newsgroups: comp.ai.digest
Subject: Re: Are all Reasoning Systems Inconsistent?
Message-ID: <19880826032133.2.NICK@HOWARD-JOHNSONS.LCS.MIT.EDU>
Date: 26 Aug 88 03:21:00 GMT
Sender: daemon@bloom-beacon.MIT.EDU
Organization: The Internet
Lines: 52
Approved: ailist@ai.ai.mit.edu

To: unido!comp-ai-digest@uunet.UU.NET
Path: sbsvax!yxoc
From: Ralf Treinen <unido!sbsvax!yxoc@uunet.UU.NET>
Newsgroups: comp.ai.digest
Subject: Re: Are all Reasoning Systems Inconsistent?
Summary: Theorem T3 not correct
Date: Thu, 25 Aug 88 08:46 EDT
References: <19880820041428.8.NICK@HOWARD-JOHNSONS.LCS.MIT.EDU>
Organization: Universitaet des Saarlandes, Saarbruecken, West Germany
Lines: 41


In a previous article, Jonathan Leivent writes:
> Here is a full version of the contradiction that I am claiming exists.  
... 
[ Q is the equality predicate, s is a substitution operation, "X" is the Godel ]
[ number of X                                                                  ]
> P(a) : the predicate of provability within this reasoning system
...
> Theorems:
> 
> T1. AaAb[Q(a,b)P(a) = P(b)] ; just says that P behaves normally
> 
> T2. Aa[P(s("~P(*)",a)) -> ~P(a)] ; If I can prove that I can't prove X, then I
> 				   can't prove X
> 
> T3. If X can be proven within this reasoning system, then P("X") is true
[ "this reasoning system" is the original one together with (at least) T1,T2 ]
...
[ derives a contradiction by constructing a Godel number G, such that ~P(G)  ]
[ can proven in the above system and then applying Theorem T3 ("step 5").    ]
...
> Perhaps the weak link in the contradiction is step 5, which is somewhat of a
> "meta" step.  What bothers me most is that there seems to be no formal way of
> writing T3, even though it seems to be obviously true
...

Theorem T3 is not correct. Just take the empty reasoning system that doesn't
allow to derive any theorem at all. The provability predicate for this
reasoning system is the constant predicate *false*. The formula ~P(G)
constructed above is provable in the this system, but P("~P(G)") is false.

BTW: The empty reasoning system IS consistent.

-- 
------------------------------------------------------------------------------
EAN  :treinen%fb10vax.informatik.uni-saarland.dbp.de [ @relay.cs.net from US]
UUCP : ...!uunet!unido!sbsvax!treinen   | Ralf Treinen
        or treinen@sbsvax.UUCP          | Universitaet des Saarlandes        
CSNET: treinen%sbsvax.uucp@Germany.CSnet| FB 10 - Informatik (Dept. of CS)  
ARPA : treinen%sbsvax.uucp@uunet.UU.NET | Bau 36, Im Stadtwald 15          
Phone: +49 681 302 2065                 | D-6600 Saarbruecken 11, West Germany 
------------------------------------------------------------------------------