- From: Gregg Kellogg <gregg@greggkellogg.net>
- Date: Mon, 12 Aug 2019 10:25:47 -0700
- To: public-n3-dev@w3.org, public-cwm-talk@w3.org
- Cc: Sandro Hawke <sandro@w3.org>, Ivan Herman <ivan@w3.org>, Tim Berners-Lee <timbl@w3.org>, Doerthe Arndt <doerthe.arndt@ugent.be>, William Van Woensel <william.vanwoensel@gmail.com>
On The N3 Dev meeting today, among other things, we discussed the ordering of universal and existential quantifiers in Notation-3 [1]. The original Team Submission [2] states "If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials”. However this makes some useful logical statements impossible (or at least difficult) to state, as we explore in our issue #6. For Example, in FOL "∀h: ∃g: loves(h,g)” and "∃g: ∀h: loves(h,g)” have different meanings, but in N3 stating "@forSome <#g>. @forAll <#h>. <#g> <#loves> <#h> .” is effectively equivalent to "∀h: ∃g: loves(h,g)”. (more discussion in [3]). We’d like some insight into this restriction. One thought was that maintaining ordering between variables is difficult within a graph, so that once statements are reduced to the data-model, there’s no way to reconstruct which came first (although, this could possibly be overcome). Perhaps there are other motivations for this. If anyone can help shed light on this decision, we’d appreciate the feedback. Gregg Kellogg gregg@greggkellogg.net [1] https://docs.google.com/document/d/1A3HAUhjaVnnJ6yVbFAvIBRJQjUY9aFlQ2_bGxkD0mnE/edit#heading=h.m0y49qer6so [2] https://www.w3.org/TeamSubmission/n3/#Quantifica [3] https://github.com/w3c/N3/issues/6#issuecomment-465154994
Received on Monday, 12 August 2019 17:26:13 UTC