Search All of the Math Forum:

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

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

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: Set Theorists use EXTENSIONALITY ..... Logic Programmers UNIFY!
Posted: Jun 13, 2013 2:46 AM

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]

directly follows from

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

[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

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

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