Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math.independent

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Graham Cooper

Posts: 4,255
Registered: 5/20/10
Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Posted: Jun 13, 2013 2:46 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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





Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.