Date: Jun 13, 2013 2:46 AM Author: Graham Cooper Subject: Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY! On Jun 12, 9:12 pm, Jan Burse <janbu...@fastmail.fm> wrote:

> Alan Smaill schrieb:

>

> > Not in general, the way you go about it.

>

> > What happens in the example you were just asked about?

> > (rather than in the ones you have already worked out, where

> > the set of positive solutions is finite).

>

> Comprehension also doesn't work when the intended

> set is finite and when negative information

> is lacking.

>

> Compare:

>

> p(1). /* I */

>

> With:

>

> forall X (p'(X) <-> X=1). /* II */

>

> They are two different kettle of fish. And we are

> here touching the very basics of FOL. Namely that

> an primeformula:

>

> p(t)

>

> Only makes a statement about what should be in

> an interpretation, and doesn't make a statement

> for what is not in the interpretation. To say

> that something is not in the interpretation we

> would need the negation of a primeformula:

>

> ~p(t)

>

> The above makes a statement about what should not

> be in an interpretation, but similarly it doesn't

> make a statement about what is in the interpretation.

>

> The p' definition can actually be expanded into:

>

> forall X ((p'(X) <- X=1) & (p'(X) -> X = 1))

>

> Which can expanded into:

>

> forall X (p'(1) & (~p'(X) <- X != 1))

>

> So it is a positive and a negative statememt. The

> positive statement is:

>

> p'(1). /* IIa */

>

> The negative statement is:

>

> forall X (~p'(X) <- X != 1). /* IIb */

>

> Whereby what we are saying about p is only a positive

> statement, namely:

>

> p(1). /* I */

>

> As a result, assuming the domain is natural numbers,

> we cannot deduce the following:

>

> T |- ~(2 in { x in nat | p(x) })

>

> Proof: There is a model where p(2). Simply take

> M[p] = {1,2}. This model satisifies the formula p(1).

>

> But we can deduce the following:

>

> T |- ~(2 in { x in nat | p'(x) })

>

> Proof: The only model that satisfies p' is

> M[p'] = {1}.

>

> So when Prolog does the following:

>

> p(1).

>

> ?- setof(X,p(X),L).

> L = [1]

>

> Then this is quite an illusion that the above is

> based on Horn clauses solely.

>

> Bye

>

You don't seem to be listening.

[1]

~tail <- ~head

directly follows from

head <- tail

============

[2]

Contrapositive Modus Ponens captures this information from [1]

theorem ( ~(X) ) :-

rule( X , Y )

theorem ( ~(Y) ).

It's closer to Proof by Contradiction than Modus Ponens

IF X->Y

AND ~Y

then X must be wrong!

============

I agree TUPLE-AT-A-TIME HORN CLAUSES

cannot do negative logic

because it cannot do SUBSET

or set theory, or membership of distinct classes

===========

I am using BREADTH WIDTH UNIFY!

*ALL* matching clauses must return TRUE!

NO I DON"T WANT TO HEAR WHAT LOGIC THEORY THIS VIOLATES and what it

can't do... It can't do this and it can't do that because it's never

been programmed before!!

I am using:

SET-AT-A-TIME HORN CLAUSES

more powerful than YOUR PROLOG

There are 2 Horn Styles. Tuple A.A.T. and Set A.A.T.

In MY PROLOG I can do this:

subset S1 S2 :-

e(all_X , S1)

e(X,S2)

You haven't got this far!

You haven't even ATTEMPTED Set Specification in Prolog!

===================

N.S.T.

e( X , set ) <-> p(X)

-----------------------------

Z.F.C

e(X , set ) -> p(X)

----------------------------

PROLOG Set Theory

e(X , set ) <- p(X)

==================

Since you are all 20 years of technology behind me I will come back in

20 years after my Fishing Expedition!

Thank you and Good Night!

Herc

--

http://phpPROLOG.com

A.I. Software / Database on the Web!

DATABASE QUERY

id ref term ref term

---------------------- ----------------

6 1 test1

6 2 aaa

7 1 test1 <=> 1 test1

7 2 bbb <=> 2 bbb

---------------------- ----------------

GOAL-AT-A-TIME UNIFY