Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



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]
~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 TUPLEATATIME 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:
SETATATIME 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  
GOALATATIME UNIFY



