Re: Godel's Incompleteness and Nonmonotonic Logic

From: Stephan Lehmke (Stephan.Lehmke_at_ls1.cs.uni-dortmund.de)
Date: 08/25/04 

Date: 25 Aug 2004 09:15:15 GMT

In article <1b626f1.0408241341.45b728fa@posting.google.com>,
        jagasian@mailinator.com (Student) writes:
>> Does "Answer Set Logic" have anything to do with negation by failure?
>> To get the kind of paradox you're after, one would at least imagine
>> provability to have to be decidable.
>
> Decidability is a separate issue. The problem is that an inconsistent
> logic will allow for incorrect answers.

This is not neccessarily true. If the logics we're talking about
are of the "negation by failure" type, then provability of -F is
defined as non-provability of F. Assuming that provability is
recursively enumerable, if non-provability were also recursively
enumerable, it would immediately follow that both are decidable.

If provability is known to be recursively enumerable but undecidable,
as is the case for first order logic, it immediately follows that
non-provability is not recursively enumerable. Hence a "logic" of
"negation by failure" type is either decidable or non-axiomatiseable
and hence incomplete, without any reference to Goedel theorems.

Thus, even though a "logic" of "negation by failure" type might
_seem_ to be Hilbert-complete by definition, it isn't, and isn't
even complete in the classical sense if provability is not decidable.

You see that inconsistency doesn't enter the picture at all.

>> How to stitch this together with second order logics to which Goedels
>> incompleteness theorems refer escapes me.
>
> Godel's two famous theorems apply to first-order predicate logic.

I'm not completely sure what two theorems you are referring to,
but if the theorem generally known as `the' "incompleteness theorem"
is among them then this statement is clearly false.

> See
> Kleene's "Introduction to Metamathematics", Kleene's "Mathematical
> Logic", or Girard's "Proof Theory and Logical Complexity : Volume I",
> if you cannot get your hands on the Godel's original work (or a
> translation thereof).

You are very generous with your references. I have none of them
immediately available, but as they stem from respectable authors, I am
sure you will find in them no claim that first-order predicate logic
is in danger of being incomplete in the standard meaning of this
concept.

>> Closed world assumption, which is a more mainstream representative of
>> the kind of nonmonotonic logics you seem to be talking about,
>> guarantees "Hilbert completeness" only wrt ground atomic formulae.
>
> Well, the answer set style logics work with non-ground formula by
> assuming a possibly infinite grounding. See "Knowledge
> Representation, Reasoning, and Declarative Problem Solving" by Chitta
> Baral.

It is nice to cite things, but on usenet it is considered good form
to define the things one is talking about.

Maybe you could give a rigorous definition of "answer set style logics"?

regards
Stephan 

-- 
  Stephan Lehmke     		 Stephan.Lehmke@cs.uni-dortmund.de
  Fachbereich Informatik, LS I	 Tel. +49 231 755 6434 
  Universitaet Dortmund		 FAX 		  6555
  D-44221 Dortmund, Germany      http://ls1-www.cs.uni-dortmund.de

Relevant Pages

  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... >> provability to have to be decidable. ... > Decidability is a separate issue. ... If the logics we're talking about ... without any reference to Goedel theorems. ...
    (comp.lang.prolog)
  • Re: Simple yet Profound Metatheorem
    ... >>premises is not a valid proof in these logics. ... denoted by the "absurdity symbol") from P&~P and then ... truth as provability. ...
    (sci.logic)
  • Re: Sorry Godel - All Truths are Provable
    ... truth-value of a statement has to coincide with its provability-value. ... Doesn't have to, but for most logics it does, ... Lemma 2: Completness of Provability: ... V The Completeness Theorem, 4.1 Completness Theorem ...
    (sci.logic)
  • Re: A question on GIT.
    ... Maybe you're confusing truth with provability -- or something like that. ... Decidability is a question of what you can prove in a system, ... proof of its undecidability. ...
    (sci.logic)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... Decidability is a separate issue. ... > incompleteness theorems refer escapes me. ... the answer set style logics work with non-ground formula by ...
    (sci.logic)