Re: Blank node quantification

On 16/06/2021 14:24, Nathan Rixham wrote:
> 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?

Nitpicking: implications themselves are not quantified, variables are.

Actually, my proposal does not change the way blank node behave in rules 
(well, in simple cases, at least). Currently, blank nodes are currently 
scoped to the formula in which they occur, whether it is a rule or not. 
In my proposal, blank nodes will be scoped to the formula in which they 
occur ONLY if this formula is the body or head of a rule.

>
> On Wed, Jun 16, 2021 at 11:34 AM Pierre-Antoine Champin 
> <pierre-antoine@w3.org <mailto: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
>>
>>