Prolog - Prolog & Incompleteness

Author

Prolog & Incompleteness

Jurgen Van Gael

2004-03-27, 12:10 am

Hi,

I have just started a prolog programming course this semester and this is
something which has been on my mind lately. Prolog tries to prove first
order predicate logic theorems given certain inference steps. As prolog
allows arithmetic it seems as if prolog logic has all necessary ingredients
to be subject to godel's incompleteness theorem. My question is if there
indeed are truths which prolog will never be able to prove or if certain
builtin assumptions (closed world, ...) free prolog of being incomplete.

looking forward for your replies,

Jurgen

Benjamin Johnston

2004-03-27, 12:10 am

Consider,

a :- a.
a.

Submitting the query "a.", will result in an infinite loop using Prolog's
proof mechanism. So, clearly, prolog is incomplete.

Also, as Prolog is a turing complete language; you can implement in Prolog a
proof checker for any logic that has a computable proof verification
procedure - so Godel's theorem applies (assuming an idealized computer with
unlimited precision arithemetic) and as do all the results about
decidability and the halting problem.

I belive this is Godel's Therem translated into Prolog:

provablepassingself(Term - FreeVar) :-
copy_term(Term - FreeVar, Term2 - FreeVar2),
FreeVar = Term2 - FreeVar2,
call(Term).

godel :- \+provablepassingself((\+provablepassing
self(FreeVar)) - FreeVar).

The minus used is not aritmethical, it's like a difference list.

"Jurgen Van Gael" <jurgen.vangael@student.kuleuven.ac.be> wrote in message
news:c2v430$21ae8a$2@ID-177529.news.uni-berlin.de...
> Hi,
>
> I have just started a prolog programming course this semester and this is
> something which has been on my mind lately. Prolog tries to prove first
> order predicate logic theorems given certain inference steps. As prolog
> allows arithmetic it seems as if prolog logic has all necessary
ingredients
> to be subject to godel's incompleteness theorem. My question is if there
> indeed are truths which prolog will never be able to prove or if certain
> builtin assumptions (closed world, ...) free prolog of being incomplete.
>
> looking forward for your replies,
>
> Jurgen
>
>

Jamie Andrews; real address @ bottom of message

2004-03-27, 12:10 am

Jurgen Van Gael <jurgen.vangael@student.kuleuven.ac.be> wrote:
> I have just started a prolog programming course this semester and this is
> something which has been on my mind lately. Prolog tries to prove first
> order predicate logic theorems given certain inference steps. As prolog
> allows arithmetic it seems as if prolog logic has all necessary ingredients
> to be subject to godel's incompleteness theorem. My question is if there
> indeed are truths which prolog will never be able to prove or if certain
> builtin assumptions (closed world, ...) free prolog of being incomplete.

Prolog is incomplete for a number of reasons. One of the
simplest queries that it can't solve (first described by Keith
Clark and discussed in more detail by Andreka and Nemeti) is as
follows. Let the predicate "inflist" be defined by:

inflist([X|Xs]) :- inflist(Xs).

"inflist" represents the property of a list of being infinite.
A list of the form [X|Xs] is infinite if Xs is infinite. Now,
in Prolog there can't be any infinite lists, so the query
inflist(Y) should fail, and the query (\+ inflist(Y)) (i.e.
"inflist(Y) is unprovable") should succeed. But both of those
queries goes into infinite recursion; neither terminates at all.
Prolog can't determine the truth or falsehood of either query,
so it is incomplete. To put a sharper point on it, consider the
predicate "foo" defined by:

foo(X) :- inflist(Y).
foo(a).

Clearly there is one solution to the query foo(Z), i.e. Z=a.
However, Prolog will never find it because it will first go off
trying to find an infinite list.

Your point about Goedel's incompleteness theorem is correct
as well, but Prolog does not even encode all the axioms of
arithmetic, so it can't even prove all the things that *can* be
proved in arithmetic. In particular, it can't prove anything by
induction. If you define integers and addition in the way that
is standard in formal arithmetic, you should be able to prove
that X+Y = Y+X. However, we can't prove that in Prolog. The
best that we could do is to set Prolog to work searching for an
X and Y such that X+Y is not Y+X, and feel relieved that it goes
off into infinite recursion and doesn't return an answer.

So, to summarize, yes, Prolog is vulnerable to Goedel's
incompleteness theorem and there are true formulas that cannot
be proven in Prolog. However, there are many formulas that
Prolog can't prove in additions to the ones that it can't prove
via Goedel's argument.

--Jamie. (nel mezzo del cammin di nostra vita)
andrews .uwo } Merge these two lines to obtain my e-mail address.
@csd .ca } (Unsolicited "bulk" e-mail costs everyone.)

Alan Bal jeu

2004-03-27, 12:10 am

"Jamie Andrews; real address @ bottom of message" <me@privacy.net> wrote in
message news:c3fks0$21rcmp$1@ID-193590.news.uni-berlin.de...
> Jurgen Van Gael <jurgen.vangael@student.kuleuven.ac.be> wrote:
is[color=darkred]
ingredients[color=darkred]
>
> Prolog is incomplete for a number of reasons. One of the
> simplest queries that it can't solve (first described by Keith
> Clark and discussed in more detail by Andreka and Nemeti) is as
> follows. Let the predicate "inflist" be defined by:
>
> inflist([X|Xs]) :- inflist(Xs).
>
> "inflist" represents the property of a list of being infinite.
> A list of the form [X|Xs] is infinite if Xs is infinite. Now,
> in Prolog there can't be any infinite lists, so the query
> inflist(Y) should fail, and the query (\+ inflist(Y)) (i.e.
> "inflist(Y) is unprovable") should succeed. But both of those
> queries goes into infinite recursion; neither terminates at all.
> Prolog can't determine the truth or falsehood of either query,
> so it is incomplete. To put a sharper point on it, consider the
> predicate "foo" defined by:
>
> foo(X) :- inflist(Y).
> foo(a).
It is true that basic Prolog will hang on the query ?- foo(a). However,
one can easily write an interpreter in Prolog, which operates directly
on Prolog facts, and can prove foo(a). Prolog is Turing-complete, and
thus Goedel-incomplete.

As a theorem-prover, prolog's default depth-first-search algorithm is
limited as you describe. But with conditionals and recursion available
to the programmer, any other prover can be coded.

Sponsored Links