jon@XN.LL.MIT.EDU (Jonathan Leivent) (07/24/88)
Date: Tue, 19 Jul 88 10:16 EDT From: Jonathan Leivent <jon@XN.LL.MIT.EDU> Posted-Date: Tue, 19 Jul 88 10:16:06 EDT To: AILIST@AI.AI.MIT.EDU Subject: Are all Reasoning Systems Inconsistent? cc: adams@XN.LL.MIT.EDU, jon@XN.LL.MIT.EDU Within any (finite) reasoning system, it is possible to construct a sentence S from any preposition A such that S = (S -> A) using Godel-like methods to establish the recursion. However, such a sentence leads to the inconsistent conclusion that A is true - any A! 1. S = (S -> A) ; the definition of S, true by construction 2. S -> (S -> A) ; a weaker form of 1. [U = V, so U -> V] 3. S -> S ; an obvious tautology 4. S -> (S ^ (S -> A)) ; from 2. and 3. by conjunction of the consequents [U -> V and U -> W, so U -> (V ^ W)] 5. (S ^ (S -> A)) -> A ; modus ponens 6. S -> A ; from 4. and 5. by transitivity of -> [U -> V and V -> W, so U -> W] 7. S ; from 1. and 6. [U = V and V, so U] 8. A ; from 6. and 7. by modus ponens Am I doing something wrong, or did logic just fall down the rabbit hole? -- Jon Leivent
mclean@NRL-CSS.ARPA (John McLean) (08/05/88)
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
jon@XN.LL.MIT.EDU (Jonathan Leivent) (08/07/88)
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
hartley@NRL-AIC.ARPA (Ralph Hartley) (08/26/88)
Date: Tue, 16 Aug 88 08:06 EDT From: Ralph Hartley <hartley@nrl-aic.arpa> Subject: Re: Are all reasoning systems inconsistent? To: AILIST-REQUEST@LCS.MIT.EDU Resent-Date: Thu, 18 Aug 88 14:12 EDT Resent-From: Rob Austein <SRA@XX.LCS.MIT.EDU> Resent-To: ailist-request@MC.LCS.MIT.EDU Your problem lies in T2 >T2. Aa[P(s("~P(*)",a)) -> ~P(a)] ; If I can prove that I can't prove X, > then I can't prove X This implies Ea(~P(a)) i.e. that the system is consistent. Godel's 2nd (less well known) theorem states that if it is possible to prove a system consistent within the system then the system is NOT consistent. Therefore T2 cannot be a theorem in any consistent system. BTW - This is also a flaw in Hofstadter's reasoning about the prisoners dilema. His argument goes as follows: 1. The other player uses the same reasoning as I do. 2. This reasoning produces a unique result (cooperate or defect but not both) 3. Therefor whatever I do he will do too. 4. So I should cooperate. The problem, again, is that (1) and (2) imply that my logic is consistent - therefore it is not. Ralph Hartley hartley@nrl-aic.ARPA
yxoc@sbsvax.UUCP (Ralf Treinen) (08/26/88)
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 ------------------------------------------------------------------------------