Re: Blank node quantification

This is probably a gross simplification, but do I take this to mean that if
a blank node is present in a formula, then implication is taken to be
existential with forSome, else if no blank node present then implication is
universal with forAll?

On Wed, Jun 16, 2021 at 11:34 AM Pierre-Antoine Champin <
pierre-antoine@w3.org> wrote:

> 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
>
>
>