Re: Godel's Incompleteness and Nonmonotonic Logic
From: Herman Jurjus (h.jurjus_at_hetnet.nl)
Date: 08/26/04
- Next message: Herman Jurjus: "Re: Godel's Incompleteness and Nonmonotonic Logic"
- Previous message: russell kym horsell: "Re: Remove all asserted facts?"
- In reply to: Student: "Re: Godel's Incompleteness and Nonmonotonic Logic"
- Next in thread: Jamie Andrews; real address _at_ bottom of message: "Re: Godel's Incompleteness and Nonmonotonic Logic"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Date: Thu, 26 Aug 2004 10:19:13 +0200
Student wrote:
> I haven't read anything about "Default Logic"... I will look into it.
> Thanks for the references by the way.
>
>
>
>>For default logic, inconsistency works pretty much the same as for
>>classical logic: some theories are consistent, others are not.
>>It's not difficult to find simple default theories that definitely have
>>extensions. And i'm sure it works the same way for answer set programming.
>
>
>
> So I guess my question is, is arithmetic (i.e. Peano's theory)
> inconsistent when coded in answer set programming?
In default logic, as long as you don't add defaults to your theory,
the conclusions are just the classical conclusions.
In asp, i don't know.
Surely anybody can
> write a messed up set of inference rules that is inconsistent... I
> could just take A and -A as axioms in my logic program. However,
> anything calling itself a logic shouldn't make arithmetic
> inconsistent.
I'm pretty sure asp doesn't make arithmetic inconsistent.
>>The Goedel sentence contains a coding of a 'provability' predicate.
>>For fixpoint systems such as default logic or asp, such a coding is not
>>available. (The notion of 'provable' there is not the same as classical
>>provability.)
>
>
>
> So there these logics have no notion of proof? The fact that these
> logics are used for computing things implies that there has to be some
> notion of a proof of a formula.
It's more like a computation of the truth value of an entire clause
T |~ p.
For example, answer set programming
> language interpreters will tell me whether or not a query succeeds,
> and the computation history which leads up to this answer can be
> regarded as a proof.
"can be regarded": sure. But it's a very different kind of proof,
compared to a proof in classical logic.
> Assuming that the answer set language I choose is Turing complete,
> then it should be possible to code a predicate "isAProof( P, F )" that
> is true when P is a structure representing a computation history
> resulting in a positive answer for the query formula represented by
> the structure F.
No. As far as i know, both default logic and asp are not decidable,
not even semi-decidable (=set of conclusions is recursive enumerable).
So, for a language strong enough to code arithmetic, only approximations
of the inference operator could be programmed. The fixpoint construction
also will not be codable in that language.
For simpler theories, such as finite sets of horn clauses, the situation
is different (and that is what implementations of asp can handle). But
in such a restricted language, you can't formalize arithmetic...
> What am I missing? I understand that some ASP languages lack function
> symbols, and are therefore not Turing complete, but in Chitta Baral's
> text, he uses something called "AnsProlog"... which is Prolog with
> Answer Set style negation - that should be Turing complete. Hence
> writing an "isAProof" predicate like Godel uses should be
> straightforward (though tedious).
The fixpoint construction (= the definition of provability)
will most probably be not codable in the language.
(But it is of course also possible that Baral's variant is indeed
problematic.)
-- Cheers, Herman Jurjus
- Next message: Herman Jurjus: "Re: Godel's Incompleteness and Nonmonotonic Logic"
- Previous message: russell kym horsell: "Re: Remove all asserted facts?"
- In reply to: Student: "Re: Godel's Incompleteness and Nonmonotonic Logic"
- Next in thread: Jamie Andrews; real address _at_ bottom of message: "Re: Godel's Incompleteness and Nonmonotonic Logic"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Relevant Pages
|
