Re: Modal Concepts?

Dear Henry,

First of all my apologies that I did not react earlier to your mail, the main reason was that I am not very strong in modal logic and did not want to answer before having a look one the modal concepts you mentioned. I still did not do that, but the conversation starts to get interesting, so I will answer with all my ignorance ;).

Am 26.08.2021 um 11:31 schrieb Henry Story <henry.story@bblfish.net<mailto:henry.story@bblfish.net>>:



On 26. Aug 2021, at 10:18, Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu<mailto:pierre-antoine.champin@ercim.eu>> wrote:

Hi Henry, all,

On 17/08/2021 11:03, Henry Story wrote:
Hi,

 I was wondering how many modal concepts could be deal with
in N3. Perhaps there is already a good study of those?

I guess we could perhaps say that Truth could be considered modal,
and that is already defined with log:Truth.

Necessity could be easy:

{ 2 + 2 = 4 } a log:Necessity .

It means one could always add it to any graph, even those of one’s
opponents. Perhaps definitions in ontologies are like that? Perhaps not.

{cat color Green} log:Possible, may be a way of disproving something.

I guess we could define modalities as classes of quoted graphs, and add some axioms of the form


 { {?s ?p ?o} a :Necessity } => { ?s ?p ?o }.
 { ?s ?p ?o } => { { ?s ?p ?o } a :Possibility }.

That seems right, yes.


 { ?f a :Necessity; log:includes { ?s ?p ?o }} => { {?s ?p ?o} a :Necessity }.
 { ?f a :Possibility; log:includes { ?s ?p ?o }} => { {?s ?p ?o} a :Possibility }.

That looks right too.


but beyond that, what could we do with it?

Well for one we can start modeling what in access control areas is known as the ”:says” operator.
It is  not a simple sentential operator like necessity and possibility, but an indexed one.

See Martin Abadi’s "A Modal Deconstruction of Access Control Logics"
https://link.springer.com/chapter/10.1007/978-3-540-78499-9_16


It can also be represented in what is known in Functional Programming as Indexed Strong Monads
as argued in Abadi’s paper
Access control in a core calculus of dependency
https://dl.acm.org/doi/abs/10.1145/1159803.1159839


I only had a quick look. This has not been done in N3 yet, but we could try to see whether we could implement such kinds of hierarchies.

These are really just mathematical ways of getting to the relation we have
discussed here before namely

:Jane :says { Superman a :FlyingBeing . }

The indexed strong monads are indexed on Agents (eg. Jane) and the
context is what is between the `{ }` and there are rules about
what can and cannot be brought into that scope.


So, if I for example want to mimic the example for ICL in the paper, I could do:

General rules:

#unit
{?a :says {?s ?p ?o}}<={?a a :Principal. ?s ?p ?o}.

#cruc
{?a :says {?s=>?t}. ?a :says ?s}=>{?a :says ?t}.

#idem
{?a :says {?a :says ?y}}=>{?a :says ?y}.

 Rules for example:

:admin a :Principal.
:Bob a :Principal.

{:admin :says {:file1 :action :delete}}=> {:file1 :action :delete}.
:admin :says {:Bob :says {:file1 :action :delete}}=> {:file1 :action :delete}}.
:Bob :says {:file1 :action :delete}.


Is that what you have in mind?

You can play with the example here: http://ppr.cs.dal.ca:3002/n3/editor/s/k2ZCePx6


I am not happy with the first unit rule since it only supports triples and the principle has to be declared, but these things could be fixed. Note that I wrote the first rule backwards because it would otherwise really mess up the performance.
If you want to go there, we could try to write the rules in the paper and see whether everything is possible (as a starting point for further discussions).



I am not an expert in modal logic, but my intuition is that without a proper negation, that won't bring us very far...

I thought we did have negation, with log:Falsehood. But I can’t find it on the cwm builtins.
I think I did see it in the cwm code examples though.

There was indeed log:Falsehood (earlier n3:Falsehood, see for example https://www.w3.org/TeamSubmission/n3/#Quoting ) in the original n3 proposals but that has never been implemented.

N3 supports scoped negation as failure (in cwm you can for example use log:notIncludes in combination with log:conclusion and/or log:semantics) and EYE also supports integrity constraints (if you use the literal false as conclusion of a rule).



In any case it is needed on the web, for an agent to be able to express disagreement on some topic
with another. Well perhaps we can get relative disagreement with a

agent :rejects { … }

That would be a modal form of falsehood, that would not be as strong as log:Falsehood
by tying it to a perspective. It is modal because in a way that is what modal logic does
it moves relativists Truth and Falsehood to worlds.

Mmm, but how much negation would you need to do meaningful reasoning with your examples. Is it enough to have some expression for falsehood and then define rules for it?



Two that are particularly useful in computing are SHOULD and MUST,
as they are used by ietf and w3c specs. It would be nice to at least
be able to explain what kind of concepts those are. They somehow
seem related to a goal Something MUST be done - if a goal (e.g. communication)
is to be achieved.
It's an appealing notion, but could you develop it a little?

I think those two are actually quite far beyond what could be expressible in N3.
David Lewis in Counterfactuals 1973 gives an analysis of ”ought” in terms of ideal
worlds (towards the end of the text). The difference with those modalities is that
the ”actual” ideal often does not contain the world from which the agent is speaking.

Ie.

if John :believes P
then John things the actual world is an element of P.

but if John thinks one ought to P
then one cannot deduce that John thinks the actual world fits the state of affairs described by P.

Still it is worth thinking about that.

Henry



Henry Story

https://co-operating.systems<https://co-operating.systems/>
WhatsApp, Signal, Tel: +33 6 38 32 69 84‬
Twitter: @bblfish


<OpenPGP_0x9D1EDAEEEF98D438.asc>

Henry Story

https://co-operating.systems<https://co-operating.systems/>
WhatsApp, Signal, Tel: +33 6 38 32 69 84‬
Twitter: @bblfish

As you see, we did not work much on modal logic with N3 yet, but we could give it a try if you want. If so, I would like to have a starting point such that we can write down some rules and play with them as I did above (followed by a proper theory of course).

Kind regards,
Dörthe