Re: Blank node quantification

Fiddling with yet another example that came to my mind:

Example 6:

   _:u a :Unicorn.
   _:e a :UnicornEater.
   { ?x a :Unicorn } => { { [] a :UnicornEater } => { ?x :is :threatened 
} }.

is equivalent to (using old-style explicit quantifiers)

   @forSome v:u, v:e.
   v:u a :Unicorn.
   v:e a :UnicornEater.
   { ?x a :Unicorn } => { { @forSome v:e2. v:e2 a :UnicornEater } => { 
?x :is :threatened } }.

I would expect it to produce (1)

   { @forSome v:e2. v:e2 a :UnicornEater } => { v:u :is :threatened }. # 
with v:u still quantified by the top @forSome

which in turn would produce (2)

   v:u :is :threatened. # with v:u still quantified by the top @forSome

Note that the rule produced at (1) can not be expressed with the 
implicit quantification scheme that I am proposing (nor is it with the 
/current/ implicit quantification scheme, by the way). More precisely, 
v:u is existentially quantified outside the formula that contains it, 
despite the fact that this formula is the object of log:implies.

So in that case, we would still need to skolemize v:u (generate a 
witness) in order to express that rule.

   pa

On 16/06/2021 09:26, Pierre-Antoine Champin wrote:
> Hi all,
>
> here's a crazy idea. I am not even sure I like it myself, but I wanted 
> to ear others' opinion about it.
>
> During our last call, William made a point, with which I agree 
> (assuming I understood it correctly). To sum it up: people use blank 
> node in data more as "local" identifiers than as proper existential 
> variables. This pleads for quantifying blank nodes at the top level.
>
> On the other hand, as we also pointed out during the call, blank nodes 
> as used in rule bodies (and rule heads, I believe) need to be 
> quantified locally.
>
> Hence my crazy idea: why not make the scope of blank node determined 
> by the log:implies (=>) predicate?
>
> More precisely:
>
> * a formula that is the subject or object of log:implies defines a new 
> scope for blank nodes
>
> * any other formula inherits the scope of its immediate parent
>
> * blank nodes in the top level scope are quantified *before* 
> universals (which is consistent with viewing them as "local constants")
>
> Below is a long (apologies) list of examples.
>
> WDYT?
>
>   pa
>
>
> Examples 1:
>
>     :alice :belives { [] a :Unicorn }.
>     [] a :Person.
>
> is equivalent to (using old-style explicit quantifiers)
>
>    @forSome v:u, v:p.
>    :alice :belives { v:u a :Unicorn }.
>    v:p a :Person.
>
> ----
>
> Example 2:
>
>     { [] a :Unicorn } => { :world a :MagicalPlace }.
>
> is equivalent to (using old-style explicit quantifiers)
>
>     { @forSome v:u. v:u a :Unicorn } => { :world a :MagicalPlace }.
>
> (i.e. no change with today's interpretation)
>
> ----
>
> Example 3:
>
>     { ?x a :Person } => { ?x :mother [] }.
>
> is equivalent to (using old-style explicit quantifiers)
>
>     { ?x a :Person } => { @forSome v:m. ?x :mother v:m }.
>
> (i.e. no change with today's interpretation)
>
> ----
>
> Example 4:
>
>     :alice :belives { [] a :Unicorn }.
>     { ?x :believes { [] a :Unicorn } } => { ?x a :GulliblePerson }.
>
> is equivalent to (using old-style explicit quantifiers)
>
>     @forSome v:u1.
>     :alice :believes { v:u1 a :Unicorn }.
>     { @forSome v:u2. ?x :believs { v:u2 a :Unicorn } } => { ?x a 
> :GulliblePerson }.
>
> which, unless I am mistaken, is also equivalent to
>
>     @forSome v:u1.
>     :alice :believes { v:u1 a :Unicorn }.
>     { ?x :believs { ?u2 a :Unicorn } } => { ?x a :GulliblePerson }.
>
> I would expect this to produce.
>
>     :alice a :GulliblePerson.
>
> ----
>
> Example 5:
>
>     :alice :belives { [] a :Unicorn }.
>     { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.
>
> is equivalent to (using old-style explicit quantifiers)
>
>     @forSome v:u1.
>     :alice :believes { v:u1 a :Unicorn }.
>     { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.
>
> I would have no problem with this producing
>
>     :alice :wishesToRide v:u1.  # where v:u1 is still quantified by 
> the top @forSome
>
>