Re: Antoine's semantics as a model theory. (Was: Re: Islands (ACTION-148))


We two have a different heritage with respect to our relationship with
logics.  For that reason, I tend to write things in a form that is in
line with common practices in the Semantic Web KR community.  But the
fact that I do not use the same form as Mr. Tarski to define a model
theory does not mean it is an illegitimate MT.
In particular, you say that I must define what I(D) is for a dataset D.
I claim that I do not need to, and description logicians do not do that
in general. In, DL, we do not say what I(T) is for a DL theory T.  We
simply define the satisfaction relation instead.  And we know we can do
that because it is trivially equivalent.  Similarly, contextual logics
often define a "multi-contextual" interpretation as a set of "local"
interpretations.  Again, this is perfectly legitimate as we know we can
equally well express it as if it was a single interpretation on
"contextualised terms", from which you can define interpretations in the
spirit of Tarski, from the ground up.  But again, I do not need to do so
because it is clear how to go from one form to the other, and no
absolute law says that a logic must be written in Tarski's style.

The only thing which is not kosher in my definitions is "entailment",
which is, I admit, at odds with all kinds of model theory that I know. I 
want to change this, but I'd like to change some other things too.

In any case, if you prefer to rewrite the proposal in a different form
that you find more suitable, I have no objection, especially if it can
advance the discussions on these topics.

In fact, your formalisation below suits my taste too, and if you do not 
update the wiki yourself, I'll reformulate the dataset semantics using 
your proposition.

few comments below.

Le 01/03/2012 17:48, Pat Hayes a écrit :
> On Feb 29, 2012, at 5:28 AM, Antoine Zimmermann wrote:
>> Le 29/02/2012 04:51, Pat Hayes a écrit :
>>> On Feb 28, 2012, at 11:39 AM, Antoine Zimmermann wrote:
>>>> ....
>>>>> If I put two copies of a graph into a single trig document
>>>>> with two different lables, one of the copies does not entail
>>>>> the other, even though they are the same graph.
>>>> Again, no, the RDF graphs entail each others. It's the pairs
>>>> (n1,g), (n2,g) that do not entail each others. Which is
>>>> exactly what I would like to have. Otherwise, I would not have
>>>> made two copies in the first place.
>>> So the added label *changes the meaning* of the graph it is
>>> attached to. (It must do so, since otherwise the graph must
>>> entail itself, trivially.)
>> No and no. g entails g. (n1,g) does not entail (n2,g)
> Entailment is defined by the dictionary. A entails B when every
> interpretation which makes A true, makes B true. So, you are telling
> me that there is an interpretation (in your sense) which makes (n1,
> g) true but makes (n2, g) false. Please expand on how exactly that
> happens. (Actually, dont bother, as I have already worked it out, see
> below.)
>> It does not change at all the meaning of g. The meaning of g is not
>> the meaning of (n1,g), just like the meaning of a quad is not the
>> meaning of a triple.
> Well, not *just* like that, but OK.
>> So, the natural question to ask is, how does the meaning
>>> change? That is, where in the semantics of these graph/name
>>> pairs, is there something that makes it mean something different
>>> from what the bare graph would mean? One wants to see a
>>> specification of an interpretation structure (like the INT/EXT
>>> mappings in the RDF semantics, but probably involving the labels
>>> in some way) which assigns meanings to the basic symbols, and
>>> then precisely given truth conditions which specify, given such a
>>> structure, what the larger syntactic objects - triples, graphs,
>>> named graphs and datasets - mean in that structure. So far I dont
>>> see that in your proposal.
>> It's a complete model theory for datasets.
> Actually its not a model theory at all, but that can be fixed. A
> model theory is a formal specification of truth in an interpretation.
> It defines interpretation structures and truth conditions in enough
> detail to specify the truthvalue (usually eiher true or false) of
> sentences in a given interpretation. (Tarski's original paper
> defining the subject had the title "A theory of truth for formalized
> languages") All the other notions - entailment, consistency - then
> *follow* from the basic definition of truth. One does not get to
> stipulate what "entailment" means by adding little extra conditions
> on the side.
>> Given any dataset, consistency is fully specified, entailment is
>> fully specified, and interpretations are fully specified. What is
>> missing?
> See above.
>> If you don't like the fact that I do not define what I(D) means for
>> a dataset D, this is another matter. I(D) can be trivially defined,
>> but does not need to.
> But it does need to, in order to be an honest model theory and to be
> properly compared to alternatives. So, in the spirit of cooperation,
> let me re-write your wiki proposal as a Tarskian model-theoretic
> semantics. The key point is that the assignment of RDFinterpretations
> to graph labels is fixed, and entailment relies upon this mapping. So
> it should be defined as part of the truth conditions rather than
> hidden in a subscript convention. Here goes.
> An RDFinterpretation is an interpretation of RDF graphs as defined in
> the 2004 semantics.
> Given a vocabulary V, let K be the set of all RDFinterpretations on
> V. An<it>AZinterpretation</it>  (on V) is a pair<I, CON>  where I is
> an RDFinterpretation (of V) and CON is a mapping (which we can call
> the context mapping) from V to K, ie an assignment of an
> RDFinterpretation to each element of the vocabulary. (Question:
> should these RDFinterpretations all have the same universe??). Then a
> dataset (D, (n1, D1)...(nm, Dm)) is true in the AZinterpretation<I,
> CON>  just when I(D)=true and for each j in 1...m, CON(nj)(Dj)=true;
> otherwise it is false.

Thanks, I like it.

> This makes the standard definition of entailment match up with your
> definition: A entails B just when every AZinterpretation which makes
> A true, also makes B true. (To get stronger entailment regimes, just
> say that K is the set of RDFS/D-/OWL/OWL2 -interpretations of V
> rather than RDFinterpretations.  BTW, when I was trashing your
> semantics, I was using the standard notion of entailment with your
> truthconditions as stated, which in effect allows the CON mapping to
> change between the antecedent and the conclusion, which makes
> entailment almost always fail.)

True. The non standard definition of entailment was a mistake, I agree.

> This is not exactly equivalent to the quads proposal. Intuitively,
> the quads allows the interpretations of properties to change, while
> this allows *anything* to change, depending on the context. I dont
> think this construction can be expressed using quads, in fact.

Well, it can as quads transform to datasets and vice-versa, but 
expressing it with quads would be completely unnatural.

> FWIW, this is actually rather similar to a simplified modal logic
> semantics in which the contexts are 'possible worlds'. So one could
> view this as treating a graph with a label as saying "possibly G"
> where G is what the graph would say if you were to assert it
> directly, which is kind of cute.

Yes. I hope that this way of seeing things makes you more tolerant to 
the proposal.

> The CON mapping is distinguished from the I mapping of an RDF
> interpretation, so the graph labels do not denote or refer to a graph
> in any RDF triples, according to these semantics. So metadata using
> the graph labels cannot be expressed in RDF in a datastore, unless we
> extend the semantics in some way.

Great, we are in agreement.

> OK, given this, I will try to summarize the various pros and cons of
> the three semantic ideas we now seem to have (the third being
> Sandro's reification idea). This will take a while.

Good. Maybe, to have something to bite in the meantime, could you make a 
wiki page defining the quad-based proposal alone?  I could make one 
myself, but I'm not sure I would define it exactly like what you had in 


> Pat
> ------------------------------------------------------------ IHMC
> (850)434 8903 or (650)494 3973 40 South Alcaniz St.
> (850)202 4416   office Pensacola                            (850)202
> 4440   fax FL 32502                              (850)291 0667
> mobile

Antoine Zimmermann
ISCOD / LSTI - Institut Henri Fayol
École Nationale Supérieure des Mines de Saint-Étienne
158 cours Fauriel
42023 Saint-Étienne Cedex 2
Tél:+33(0)4 77 42 83 36
Fax:+33(0)4 77 42 66 66

Received on Friday, 2 March 2012 15:09:30 UTC