semantics of local constants - followup

Earlier I wrote:
>
> Jos wrote:
>
> > This looks a bit like universal quantification, which is not something 
> > we want to have, I think.
> > 
> > Consider a rule set R with one atom and one import statement:
> > p^^iri(a^^local)
> > Directive(Import(i))
> > 
> > and the rule set identified by i:
> > p^^iri(a^^local)
> > 
> > Consider a structure I such that p^^iri(a^^local) is true, so there is 
> > an element k in the set denoted by p.
> > Consider now any structure I* that is like I such that I*_C(a^^local)=l; 
> > if I* is a model of i, then l is necessarily in the set denoted by p. 
> > Since i must be satisfied by every such I*, it is necessarily the case 
> > that if I is a model of R, the set denoted by p includes all elements in 
> > D_ind, so
> > Forall ?x (p^^iri(?x)) must be satisfied.
> 
> I think you are committing a subtle logical fallacy.
> 
> Note that I* is required to be a model of contents(iri) only, not of the
> entire set of rules.
> 
> If p(l) is true in *some* I*, it does not mean that p(l) must be true in I.
> For different I*'s, different l's will be in p. But for none of them p(l)
> needs to be in I.


Sorry, the logical fallacy was mine. I tried to simplify things, confused
myself, and came up with a broken definition.

But a proper definition is not that difficult -- just have to stick to the
basic outline of the Roman framework. Define multidocument semantic structures
as follows.

Suppose you have documents d1, ..., dn. A semantic structure, I, for
d1,...,dn is a tuple of semantic structures (I1,...,In) such that

I1 |= contents(d1)
...
In |= contents(dn)

Then you start gluing those semantic structures. For general modules it is
slightly more involved, but for imports it is simple:

For every statement

Import(di)

which appears in dj, the following must hold:

Ii must coincide with Ij except that Ii_C, Ii_F, and Ii_CF can 
differ from Ij_C, Ij_F, and Ij_CF on the local symbols.


	--michael

Received on Saturday, 12 April 2008 18:05:46 UTC