Examples of the implementation of abstraction in Watson

- s "?x";

{?x}
?x

- ri "BIND@?x"; ex();

{[?1] @ ?x}          (* [?1] is the identity function *)
[?1] @ ?x

- ri "EVAL"; ex();     (* evaluate the function *)

{?x}
?x

- s "[?1]";

{[?1]}
[?1]

- ri "BIND@?y"; ex();

{[[?2]] @ ?y}        (* [[?2]] is the constant function 
 [[?2]] @ ?y         whose value is [?1];
                     this is an example of 
                     relabelling of bound variables *)

- ri "EVAL"; ex();

{[?1]}
[?1]

(* abstraction does not need to be 
with respect to atomic terms *)

- s "(?x+?y)=?x+?y";

{(?x + ?y) = ?x + ?y}
(?x + ?y) = ?x + ?y

- ri "BIND@?x+?y"; ex();

{[?1 = ?1] @ ?x + ?y}
[?1 = ?1] @ ?x + ?y

s "3+3";

{3 + 3}
3 + 3

- ri "UNEVAL@[?1+?1]"; ex();

{[?1 + ?1] @ 3}
[?1 + ?1] @ 3

(* definition of the universal quantifier *)

(* a full account of definition commands is given
in a later section *)

- defineconstant "forall@?x" "?x=[true]";

forall:  
forall @ ?x  =  
?x = [true]
forall , 0

(* definition of the existential quantifier *)

- defineconstant "forsome@?x" "~forall@[~?x@?1]";

forsome:  
forsome @ ?x  =  
~ forall @ [~ ?x @ ?1]
forsome , 0