Dear Martin, This bit from your "E9 Move and its relationship with the origin/destination" email seems to be about P7 and spatial projections of periods rather than specifically about E9 Move, so I reply to it here:
> The FOL formalisation is NOT about publicly available place attestations. > This has not be said anywhere. Generally, the FOL statements are not > constraint by known knowledge. If you question this, or require in the FOL to > distinguish known knowledge from ontologically necessary one, we need another > issueπ. > > The spatial projection of the move is a P7. It exists regardless knowledge. My starting point was the question whether P7(x,y) β§ P89(y,z) β P7(x,z) is still regarded as true, and you said you regard that it was never true. This implies the big end of the P7 scale from small to big: phenomenal place β¦ the largest explicit attestation that we know of and still regard as P7 β¦ places that are regarded as too big to be P7 β¦ planet Earth So at this end of the scale, the P7 statements are not about being, but represent knowledge and possibly a decision by the knowledge base maintainers. How does that fit together? > Well, I do not think that the phenomenal place can never be known. Naming > another thing y as approximation for x does not mean that x is unknown. It > can be observed. It has an identity that can be used in reasoning. Fuzziness > is not ignorance. If you ask me, if the distinction does the job, I am not > sure which one. We have similar approximation questions with time-spans. Yes, "can never be known" was poor wording. I meant: For most periods the boundaries of the phenomenal place can not be exactly described in a knowledge base. Which is why you want find outer approximations. "does the job": my interpretation of the P7 statements as representing the current attested and inferrable knowledge about outer approximations of the spatial projection, and providing a set of axioms that does exactly that. > > "It doesn't mean that. The convention in the CIDOC CRM document is that > > implicit quantifiers are always "for all", not "exists". So it's more like > > "if z is the spatial projection". " > > Yes, I understand that. But if there is no spatial projection in the same > reference system, the formula you give still holds. But I wanted to say, that > it must exist. > > So, is that different or not?π For me it's not. Let me explain. First, just to be clear: you no longer regard the axiom as wrong, but only as insufficient because it doesn't include the fact that the spatial projection must exist? If you really want to express that a P7 statement is proof that a spatial projection exists, fine. If not, I don't think this axiom is the right place for that. It simply says that every P7 statement provides an outer approximation of the spatial projection in the same reference space, which we already know to exist regardless of any P7 statements. The right place to express that the spatial projection exists is, in my view, the FOL of P161. I think each FOL block should attempt to formalise what has been (explicitly or implicitly) stated in the respective scope note, and only that. With the exception "About the logical expressions used in the CIDOC CRM", see below. The P7 scope note does not say that a P7 statement causes the spatial projection to exist. On the contrary: "By the definition of P161 has spatial projection, an instance of E4 Period takes place on all its spatial projections to respective reference systems, that is, instances of E53 Place." The P161 scope note says: "The spatial projection is unique with respect to the reference system. For instance, there is exactly one spatial projection of Lord Nelson's dying relative to the ship HMS Victory". The scope note also talks about useful reference spaces. But it still seems to assume that for each spacetime volume and each reference space (not only the useful ones), a place exists that is the spatial projection. If this is wrong then the scope note should clarify this, and what the conditions are for the spatial projection to exist. Existence and uniqueness are the justification for introducing the function symbol F161, as in Place z = F161(Spacetime Volume x, Physical Thing u). So far I have taken the definition of F161 and all other function symbols as an implicit acknowledgement of the existence and uniqueness. This could be stated in the introduction section "About the logical expressions used in the CIDOC CRM". But I am also fine with making it explicit in each case. We already have an axiom that expresses the uniqueness: P161(x,y) β§ E53(z) β§ P161(x,z) β§ (βu) [E18(u) β§ P157(y,u) β§ P157(z,u)] β (z = y) We can add an explicit axiom for the existence: (βx,u) [E92(x) β§ E18(u) β (βz) [E53(z) β§ P157(z,u) β§ P161(x,z)]] Once we have established the formalisations of the existence and uniqueness of the spatial projection, the different formulations of the P7 axiom are, in fact, equivalent. (There are now at least four different names for the FOL lines: expression, statement, axiom, formula. Here I have called them axioms, and any P7(x,y) for instances x and y of P53 Place a statement.) Best, Wolfgang _______________________________________________ Crm-sig mailing list [email protected] http://lists.ics.forth.gr/mailman/listinfo/crm-sig
