DEFINITION: FORALL(X) as a PREDICATE!

[Graham Cooper]

ALL(X) is a difficult function to define as it's an INTRA FUNCTION, it
has access to the arbitrary particular string which is how we define
functions with arbitrary symbols.

e.g.

ALL(X) E(Y) Y = X + 1

is the same function as

ALL(A) E(B) B = A + 1


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

So if you use P = [X = Y + 1]

How can you Quantify over P by treating it as a function argument?

ALL(A) P

has forgotten what the variable names are inside P and is meaningless!

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

BORROWING off PROLOG SYNTAX, or HORN CLAUSES
but we will only examine an atomic predicate.

*******************

PROLOG ATOMS

term
VAR
predicate(.....)

# here I use the word predicate for the predicate name, not including
the arguments.

*******************

A term is written in lowercase such as tom, fred, 0, 1, set1, nums,
reals,

A VAR or VARIABLE is written in uppercase.

*******************

Prolog uses the DOUBLE VARIABLE INSTANTIATION RULE.

Here is a Prolog predicate that returns true iff the X ordinates are
the same.

vertical( point(X,Y) , point(X,Z) ).

********************

FORALL vs FORANY

Let's examine the AXIOM OF EXTENSIONALITY

ALL(S1) ALL(S2) ALL(X) (XeS1 <-> XeS2) <-> (S1=S2)

**********************

Procedurally the ALL(S1) ALL(S2) are not required.

This works equally as well.

ANY(S1) ANY(S2) ALL(X) (XeS1 <-> XeS2) <-> (S1=S2)

**********************

But note:

ANY(S1) ANY(S2) ANY(X) (XeS1 <-> XeS2) <-> (S1=S2)

ANY(X) is ambiguous, does the equation hold for ANY X
or is there any X for which the equation CAN hold?
meaning the same as EXIST(X)!

In PROLOG, S1 and S2 work just by using the double variable
instantiation rule to match to any (1) value of sets in the current
model under examination.

***************************

TOWARDS PROLOG

ALL(X) (XeS1<->XeS2) <-> (S1=S2)


The ALL(X) is MANDATORY! It cannot be processed using double
variable instantiation rule.

*************************************
HIGH ORDER PROLOG ATOMS
*************************************

term
VAR

predicate(.....)
ALL(......)

*************************************

e.g.
ALL(n) p(n)

is just
N(p(N))

DEFINITION:
ALL( string ) is a predicate type that returns the conjunction
of all boolean values of the predicate string argument for all
solutions of the variable ALL.

e.g. INDUCTION FORMULA

p(0) & ALL(n) p(n)->p(s(n))
-> ALL(n) p(n)

Using HIGH ORDER PROLOG method.

p(0) ^ N(p(N)->p(s(N))
-> N(p(N))

This notation provides a direct computational method for
backward chaining formula to their axiomatic derivation
by using double variable instantiation on the ALL type predicate
inside the predicate and branching into width first (conjunction)
solution search mode in a modified Unify() algorithm.


Herc
--
You pretended that there's something fishy with using the symbol oo
to
denote an element of the structure. (And, though you may not have
used
the word "dubious", you said "there are a couple of things wrong with
[N*]", so I think that my wording here isn't in the least
misleading.)
~ Jesse F Hughes leading by example

[Gary Forbis]

On Friday, November 2, 2012 1:14:26 PM UTC-7, Graham Cooper wrote:
> ALL(X) is a difficult function to define as it's an INTRA FUNCTION, it
> has access to the arbitrary particular string which is how we define
> functions with arbitrary symbols.

That wasn't too helpful to me. What do you mean by "INTRA FUNCTION"?

The best I could find was from http://www.cs.rochester.edu/u/xiaoming/csc254-intra-function-code-generation-assignment

Grammar modification for control flow: (i.e. all intra-function control flow is changed to gotos and if-gotos.) <if-statement> --> if left_parenthesis <operand> <comparison op> <operand> right_parenthesis goto LABEL semicolon
<goto-statement> --> goto LABEL semicolon
<label-statement> --> LABEL colon
LABEL is just another name for ID token

> e.g.
>
> ALL(X) E(Y) Y = X + 1
>
> is the same function as
>
> ALL(A) E(B) B = A + 1

For all A there exists a B where B = A + 1.

OK, you are defining A and B as the free variables
in the expression B = A + 1. I think I understand.

> ------------------
>
> So if you use P = [X = Y + 1]

Why would you do that? What does P respresent?

> How can you Quantify over P by treating it as a function argument?
>
> ALL(A) P
>
> has forgotten what the variable names are inside P and is meaningless!

It would be helpful if you stuck as close as possible to a single
syntax unless you are responding to some one who uses a different
syntax and seems less willing to adjust.

> -------------------
>
> BORROWING off PROLOG SYNTAX, or HORN CLAUSES
> but we will only examine an atomic predicate.
>
> *******************
>
> PROLOG ATOMS
>
> term
> VAR
> predicate(.....)
>
> # here I use the word predicate for the predicate name, not including
> the arguments.

I'm not sure what you mean by a predicate here. Sure, prolog has
a loose meaning but as far as I know for prolog a predicate is a
term with or without qualificaiton. That is "true" is a built in
predicate as is "false" as is "assert(X)". Heck I've just (re)learned
"!" and "fail" are predicates.

> *******************
>
> A term is written in lowercase such as tom, fred, 0, 1, set1, nums,
> reals,
>
> A VAR or VARIABLE is written in uppercase.
>
> *******************
>
> Prolog uses the DOUBLE VARIABLE INSTANTIATION RULE.
>

> Here is a Prolog predicate that returns true iff the X [c]ordinates are

> the same.
>
> vertical( point(X,Y) , point(X,Z) ).

I'm still relearning prolog just for you.
How do I know when vertical returns
YES, NO, or vertical(point(1,3), point(1,5))?

> ********************
>
> FORALL vs FORANY
>
> Let's examine the AXIOM OF EXTENSIONALITY
>
> ALL(S1) ALL(S2) ALL(X) (XeS1 <-> XeS2) <-> (S1=S2)

I still don't understand XeS1. I think you mean X is an element of S1.
is that correct or incorrect?

> **********************
>
> Procedurally the ALL(S1) ALL(S2) are not required.
>
> This works equally as well.
>
> ANY(S1) ANY(S2) ALL(X) (XeS1 <-> XeS2) <-> (S1=S2)

Now I'm confused. You used E(X) above to mean exists, or so
I thought. This seems to imply "ANY" is distinct from "E" (exists).
I don't know of any formal quantifiers other than universal and
existential. In informal language we might say "any one who bites
on that is a fool. We'd typically translate that to:
ALL(X)(bites(X,that) -> fool(X))
Why have you introduce a new quantifier?

> **********************
>
> But note:
>
> ANY(S1) ANY(S2) ANY(X) (XeS1 <-> XeS2) <-> (S1=S2)
>
> ANY(X) is ambiguous, does the equation hold for ANY X
> or is there any X for which the equation CAN hold?
> meaning the same as EXIST(X)!

Yes, I would agree your use of ANY was ambiguous. More
so, I took it as a variety of existential quantification
until I remembered your use of E(X) above. I like your
use of EXIST(X) as a quantifier better and would prefer
you used ELEMENT_OF(x,S1) as well. I'll use it here:

ESISTS(S1) EXISTS(S2) ALL(X)(
(ELEMENT_OF(X,S1) <-> ELEMENT_OF(X,S2)) <-> (S1=S2))

is a pretty weak claim. It leaves open the possibility
that there exists S1 and S2 for which S1 and S2 contain
exactly the same elements but we wouldn't say the sets
are equal.

> In PROLOG, S1 and S2 work just by using the double variable
> instantiation rule to match to any (1) value of sets in the current
> model under examination.

Google didn't turn up any definition for "double variable
instantiation rule". I'll have to try to determine it from
context since I don't know what you mean here.

> ***************************
>
> TOWARDS PROLOG
>
> ALL(X) (XeS1<->XeS2) <-> (S1=S2)
>
> The ALL(X) is MANDATORY! It cannot be processed using double
> variable instantiation rule.

I don't get what you are saying but I have a suggestion. I
don't know if it will work.

is_predicate(man).
is_predicate(human).
is_predicate(woman).
man([joe,jim,john]).
woman([emma,ella,elizabeth]).
human(X):- man(X).
human(X):- woman(X).

elementof(X,Y):- is_predicate(X),call(X(Y)).

?elementof(X,john)
if it works should return
elementof(man,john)
elementof(human,john)
or
man(john)
human(john)
I don't know. I don't have a prolog compiler
or interpretor and don't remember prolog.

(must later I came back here. found http://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/ISO-Hiord
)

> *************************************
> HIGH ORDER PROLOG ATOMS
> *************************************
>
> term
> VAR
>
> predicate(.....)
> ALL(......)
>
> *************************************
>
> e.g.
>
> ALL(n) p(n)
>
> is just
> N(p(N))

have you implemented that?
I would have thought you implemented

p(X) to return all X in p. For instance, using the above facts:

?man(X).
would return
man(joe)
man(jim)
man(john)

> DEFINITION:
>
> ALL( string ) is a predicate type that returns the conjunction
> of all boolean values of the predicate string argument for all
> solutions of the variable ALL.

More work needed. ALL returns a list of TRUE and FALSE?

> e.g. INDUCTION FORMULA
>
> p(0) & ALL(n) p(n)->p(s(n))
> -> ALL(n) p(n)

I don't get this at all. If you assert the fact:

natnum(0).

Then this function:

natnum(X):-
X > 0,
Xp is X - 1,
natnum(Xp).

should have the following behavior

?natnum(5)
YES
?natnum(5.2)
NO

I don't know what would be returned by
?natnum(X)

I'm thinking I've defined a very inefficient
routine where using the mod function would be
much faster.

> Using HIGH ORDER PROLOG method.
>
> p(0) ^ N(p(N)->p(s(N))
> -> N(p(N))

What does "HIGH ORDER PROLOG" reference?
Certainly nothing that looks like what you wrote.

> This notation provides a direct computational method for
> backward chaining formula to their axiomatic derivation
> by using double variable instantiation on the ALL type predicate
> inside the predicate and branching into width first (conjunction)
> solution search mode in a modified Unify() algorithm.
>
> Herc

More work. More coding in prolog if that's what you want.
Less handwaiving.

[Graham Cooper]

On Nov 3, 1:48 pm, Gary Forbis <forbisga...@msn.com> wrote:
> On Friday, November 2, 2012 1:14:26 PM UTC-7, Graham Cooper wrote:
> > ALL(X) is a difficult function to define as it's an INTRA FUNCTION, it
> > has access to the arbitrary particular string which is how we define
> > functions with arbitrary symbols.
>
> That wasn't too helpful to me.  What do you mean by "INTRA FUNCTION"?
>

Hi Gary, sorry I missed your post before.

PROLOG cannot see or examine the string itself of it's lines of code.

equals( S1, S2 ) :- e( A, S1 ) , e( A, S2 ).

This is the same as:

equals( X, Y ) :- e( Z, X ) , e (A , Y ).

You could substitute the 2nd version for the 1st version and it
wouldn't make a difference.

------

In 2nd order logic and axiom writing, you can use VARS for FORMULAS.

So if version 1 was P
and version 2 was Q

and you wanted to ADD A QUANTIFIER

A(A) P
A(A) Q

those 2 formulas are different because A() cannot see what variables
it is referring to inside P and Q.

The variable lettering is arbitrary on a line by line basis.

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

A(A) P

A(A) equals( S1, S2 ) :- e( A, S1 ) , e( A, S2 ).

THIS IS AN AXIOM OF SET EQUALITY

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

A(A) Q

A(A) equals( X , Y ) :- e( Z, X ) , e( Z, Y ).

THIS IS AN AXIOM OF SET INTERSECTION

and the A(A) is meaningless

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

That is why A(X) needs to see INSIDE the formula.

A(x) ..... P(...x...)

is like

{ x | P(...x...) }

it is a SYNTACTIC LEVEL NOTATION








>
> The best I could find was fromhttp://www.cs.rochester.edu/u/xiaoming/csc254-intra-function-code-gen...

>
> Grammar modification for control flow: (i.e. all intra-function control flow is changed to gotos and if-gotos.) <if-statement> --> if left_parenthesis <operand> <comparison op> <operand> right_parenthesis goto LABEL semicolon
>  <goto-statement> --> goto LABEL semicolon
>  <label-statement> --> LABEL colon
>  LABEL is just another name for ID token
>
> > e.g.
>
> > ALL(X) E(Y)   Y = X + 1
>
> > is the same function as
>
> > ALL(A) E(B)  B = A + 1
>
> For all A there exists a B where B = A + 1.
>
> OK, you are defining A and B as the free variables
> in the expression B = A + 1.  I think I understand.
>
> > ------------------
>
> > So if you use P =  [X = Y + 1]
>
> Why would you do that?  What does P respresent?
>

It's a 2OL VAR which is a PREDICATE

>
> > How can you Quantify over P by treating it as a function argument?
>
> > ALL(A) P
>
> > has forgotten what the variable names are inside P and is meaningless!
>
> It would be helpful if you stuck as close as possible to a single
> syntax unless you are responding to some one who uses a different
> syntax and seems less willing to adjust.
>
> > -------------------
>
> > BORROWING off PROLOG SYNTAX, or HORN CLAUSES
> > but we will only examine an atomic predicate.
>
> > *******************
>
> > PROLOG ATOMS
>
> > term
> > VAR
> > predicate(.....)
>
> > # here I use the word predicate for the predicate name, not including
> > the arguments.
>
> I'm not sure what you mean by a predicate here.  Sure, prolog has
> a loose meaning but as far as I know for prolog a predicate is a
> term with or without qualificaiton.  That is "true" is a built in
> predicate as is "false" as is "assert(X)".  Heck I've just (re)learned
> "!" and "fail" are predicates.
>

Not really they have side effects so by definition are not pure
functions.

They use the Environment not their parameters list to determine their
'result'.

>
> > *******************
>
> > A term is written in lowercase such as tom, fred, 0, 1, set1, nums,
> > reals,
>
> > A VAR or VARIABLE is written in uppercase.
>
> > *******************
>
> > Prolog uses the DOUBLE VARIABLE INSTANTIATION RULE.
>
> > Here is a Prolog predicate that returns true iff the X [c]ordinates are
> > the same.
>
> > vertical( point(X,Y) , point(X,Z) ).
>
> I'm still relearning prolog just for you.
> How do I know when vertical returns
>   YES, NO, or  vertical(point(1,3), point(1,5))?
>

if the X values are the same it should!

?- vertical( point( 1,2 ) , point(1,9) ).
YES

> > ********************
>
> > FORALL vs FORANY
>
> > Let's examine the AXIOM OF EXTENSIONALITY
>
> > ALL(S1)  ALL(S2)  ALL(X)   (XeS1  <->  XeS2)    <-> (S1=S2)
>
> I still don't understand XeS1.  I think you mean X is an element of S1.
> is that correct or incorrect?
>
> > **********************
>
> > Procedurally the ALL(S1) ALL(S2) are not required.
>
> > This works equally as well.
>
> > ANY(S1)  ANY(S2)  ALL(X)  (XeS1 <-> XeS2)   <->  (S1=S2)
>
> Now I'm confused.  You used E(X) above to mean exists, or so
> I thought.  This seems to imply "ANY" is distinct from "E" (exists).
> I don't know of any formal quantifiers other than universal and
> existential.  In informal language we might say "any one who bites
> on that is a fool.  We'd typically translate that to:
>
>   ALL(X)(bites(X,that) -> fool(X))
>
> Why have you introduce a new quantifier?

RIGHT!

Sometimes you can covert LOGIC to PROLOG

LOGIC
ALL(x) bites(x,that) -> fool(x).

PROLOG
bites(X,that) -> fool(X).

just by capitalising the x in ALL(x)

and changing it to *ANY* solution for X.


-----

Other times you have to DO ALL THE CALCULATIONS
for EVERY SOLUTION to X.

Like the AXIOM OF SET EQUALITY - PROLOG cannot do that ALL(elements)
with simple native clauses!

>
> > **********************
>
> > But note:
>
> > ANY(S1)  ANY(S2)  ANY(X)  (XeS1 <-> XeS2)   <->  (S1=S2)
>
> > ANY(X) is ambiguous, does the equation hold for ANY X
> > or is there any X for which the equation CAN hold?
> > meaning the same as EXIST(X)!
>
> Yes, I would agree your use of ANY was ambiguous.  More
> so, I took it as a variety of existential quantification
> until I remembered your use of E(X) above.  I like your
> use of EXIST(X) as a quantifier better and would prefer
> you used ELEMENT_OF(x,S1) as well.  I'll use it here:
>
>   ESISTS(S1) EXISTS(S2) ALL(X)(
>    (ELEMENT_OF(X,S1) <-> ELEMENT_OF(X,S2)) <-> (S1=S2))
>
> is a pretty weak claim.  It leaves open the possibility
> that there exists S1 and S2 for which S1 and S2 contain
> exactly the same elements but we wouldn't say the sets
> are equal.

That's what Set Theory uses to define set equality, since

MEMBER e SET

'e' is the only relation used to determine set membership.

so it follows by extension.

It's actually called AXIOM OF EXTENSIONALITY

>
> > In PROLOG, S1 and S2 work just by using the double variable
> > instantiation rule to match to any (1) value of sets in the current
> > model under examination.
>
> Google didn't turn up any definition for "double variable
> instantiation rule".  I'll have to try to determine it from
> context since I don't know what you mean here.
>

haha! I read someone else use the term... must have jumbled up the
words..

> > ***************************
>
> > TOWARDS PROLOG
>
> > ALL(X)  (XeS1<->XeS2)  <->  (S1=S2)
>
> > The ALL(X) is MANDATORY!   It cannot be processed using double
> > variable instantiation rule.
>
> I don't get what you are saying but I have a suggestion.  I
> don't know if it will work.
>
> is_predicate(man).
> is_predicate(human).
> is_predicate(woman).
> man([joe,jim,john]).
> woman([emma,ella,elizabeth]).
> human(X):- man(X).
> human(X):- woman(X).
>
> elementof(X,Y):- is_predicate(X),call(X(Y)).
>
> ?elementof(X,john)
> if it works should return
>   elementof(man,john)
>   elementof(human,john)
> or
>   man(john)
>   human(john)
> I don't know.  I don't have a prolog compiler
> or interpretor and don't remember prolog.
>

I avoid list processing for my work.


> (must later I came back here.  foundhttp://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/ISO-Hiord

In Peano arithmetic there is only the digit 0
and s(0) = 1 s(s(0)) = 2 ...

num(0).
num(s(X)) :- num(X).

>
> > Using HIGH ORDER PROLOG method.
>
> > p(0) ^ N(p(N)->p(s(N))
> > -> N(p(N))
>
> What does "HIGH ORDER PROLOG" reference?
> Certainly nothing that looks like what you wrote.
>
> > This notation provides a direct computational method for
> > backward chaining formula to their axiomatic derivation
> > by using double variable instantiation on the ALL type predicate
> > inside the predicate and branching into width first (conjunction)
> > solution search mode in a modified Unify() algorithm.
>
> > Herc
>
> More work.  More coding in prolog if that's what you want.
> Less handwaiving.

I won't be implementing high order Prolog now as I have a simple set
theoretic method to handle ALL(x).

ALL(x): d(x)->p(x)

is just

{x | d(x)} C {x | p(x)}

or

all(X, d(X), p(X))

is probably the predicate I will hand code as an extra function into
microPROLOG.

It is BREADTH FIRST, checks ALL solutions, PROOLG is depth first
( although you can use bagof or fail..)

Herc