Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Replies: 4   Last Post: Jun 13, 2013 4:47 AM

 Messages: [ Previous | Next ]
 Guest
Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Posted: Jun 12, 2013 6:20 AM

Graham Cooper <grahamcooper7@gmail.com> writes:

> On Jun 12, 9:57 am, Jan Burse <janbu...@fastmail.fm> wrote:
>> Graham Cooper schrieb:
>>

>> > I thought it was a good time for awww.phpPROLOG.com  blurb!
>>
>> > Elements of Sets occur in groups!
>>
>> > Try :  SET SPECIFICATION
>>
>> > e( A , setname )  :-  predicate(A).
>>
>> > its exactly the topic around sci.logic for the last 20 years!
>>
>> Do you mean the comprehension axiom? Something
>> along the following schema:
>>
>>    forall x exists y forall z(z in y <-> z in x & A(z))
>>
>> Abbreviated as:
>>
>>    forall x exists y (y = {z in x | A(z)})
>>
>> Problem is that comprehension doesn't work without
>> negative information. Take the following Horn clauses:
>>
>>     even(n).
>>     forall X (even(s(s(X))) <- even(X)).
>>
>> Then we cannot derive:
>>
>>     T |- s(n) in {z in nat | even(z)} /* not derivable */
>>
>> The reason is that Horn clauses don't prevent the predicate
>> even to have odd extra elements in an interpretation. So
>> that the collection {.|.} varies, and a definite statement
>> about a membership of s(n) is not possible.
>>

>
> Yes it is.

Not in general, the way you go about it.

(rather than in the ones you have already worked out, where
the set of positive solutions is finite).

>
--
Alan Smaill

Date Subject Author
6/12/13 Guest
6/13/13 Graham Cooper
6/13/13 Graham Cooper