Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83; site csd1.UUCP
Path: utzoo!linus!philabs!cmcl2!csd1!condict
From: condict@csd1.UUCP (Michael Condict)
Newsgroups: net.lang.prolog
Subject: Re: Marcel's Dilemma
Message-ID: <149@csd1.UUCP>
Date: Sat, 14-Jan-84 13:22:28 EST
Article-I.D.: csd1.149
Posted: Sat Jan 14 13:22:28 1984
Date-Received: Sun, 15-Jan-84 07:29:49 EST
References: <15320@sri-arpa.UUCP>
Organization: New York University
Lines: 29

Whoa... Marcel's problem is not meaningless at all.  What he did was express
informally three axioms about the predicate "on", axioms which may be formal-
ized in first-order logic as:

	(1) on(a) or on(b)
	(2) on(a) implies not on(b)
	(3) for all x, on(x) or not on(x)

This is called axiomatizing a predicate and is done all the time in logic.
The meaning of it is that we subsequently want to attempt to prove things
about "on", "a" and "b", using these axioms.  We would, if we could successfully
express these axioms in Prolog, not try to prove something like "on(x)", but
rather something like "on(a),on(b)" (which would be refutable).  We would
be using Prolog in theorem-prover mode, not as a programming language in-
terpreter that is supposed to compute values for variables.

While it is true that there are often many different relations (the word
relation is usually used to refer to the semantic set of pairs that is
denoted by a predicate symbol) satisfying a set of axioms, in this case
there is exactly one relation, if we restrict it to the domain {a,b}.  It is
the relation R such that xRy iff x is the logical negation of y.

The point is that we certainly do not need higher-order logic to make sense
of any of this.  Any complete theorem prover for full first-order logic could
prove all the theorems that are a logical consequence of the above axioms.
It is the restriction to Horn-clause logic that makes the problem require
the higher-order/hacking facilities of Prolog.

Michael Condict