Dear Martin,
Thinking about your last comment again, would it be acceptable to you to add
notes to certain FOL axioms? For example, one note in the P89 FOL and two notes
in the P7 FOL:
P89 FOL:
domain, range
P89(x,x)
P89(x,y) ∧ P89(y,z) ⇒ P89(x,z)
Note: Typically, a knowledge base will not infer all possible P89(x,z)
statements but may create a directed graph that can be traversed for reasoning.
(P89(x,y) also implies that x and y share the reference space. How this is done
is a separate issue.)
P121 FOL:
domain, range
P121(x,y) ⇒ P121(y,x)
P121(x,x)
P121(x,y,z) ⇒ P121(x,y) ∧ E53(z)
(in the scope note: This symmetric property associates an instance of E53 Place
with another instance of E53 Place geometrically overlapping it. The overlap
defines a third instance of P53 Place that is taken as the third value in a
ternary relation.)
P121(x,y,z) ⇒ P89(z,x) ∧ P89(z,y)
P121(x,y,z) ∧ E53(v) ∧ P89(v,x) ∧ P89(v,y) ⇒ P89(v,z)
(the usual properties of an intersection, applied to instances of P53 Place)
P161 FOL:
domain, range
P161(x,y,u) ⇔ P161(x,y) ∧ E18(u) ∧ P157(y,u)
(∀x,u) [E92(x) ∧ E18(u) ⇒ (∃y) [E53(y) ∧ P161(x,y,u)]]
P161(x,y,u) ∧ P161(x,z,u) ⇒ y = z
(existence and uniqueness of the spatial projection)
(P161(x,y) ∧ E4(x) ⇒ P7(x,y) has moved to the P7 FOL because it isn't mentioned
in the P161 scope note)
P7 FOL:
domain, range
P7(x,y) ∧ E18(u) ∧ P157(y,u) ∧ E53(z) ∧ P161(y,z,u) ⇒ P89(z,y)
P7(x,y) ∧ P7(x,z) ∧ E53(v) ∧ P89(y,v) ∧ P89(v,z) ⇒ P7(x,v)
(This is the version with P7(x,z) instead of P161(x,z). The version with
P161(x,z) follows from P7(x,y) ⇐ E4(x) ∧ P161(x,y).)
P7(x,y) ∧ P7(x,z) ∧ (∃u) [E18(u) ∧ P157(y,u) ∧ P157(z,u)] ⇒ P121(y,z)
(This additional axiom is needed to rule out Caesar's murder on the Forum Romanum, unless
we add "otherwise z is the empty place" in the definition of P121(x,y,z).)
P7(x,y) ∧ P7(x,z) ∧ E53(v) ∧ P121(y,z,v) ⇒ P7(x,v)
(the intersection of two P7 places is also a P7 place)
P7(x,y) ⇐ E4(x) ∧ P161(x,y)
Note: A knowledge base may choose to leave out this axiom and reserve P7
statements for places whose known extent provides an outer approximation of the
spatial projection.
P7(x,y) ⇒ (∃z) [E53(z) ∧ P89(y,z) ∧ ¬P7(x,z)]
(this is the negation of "for any given period x and place y, P7(x,y) ∧ P89(y,z) ⇒
P7(x,z) is not true")
Note: A knowledge base may not contain any instance z of P53 Place with
P89(y,z) ∧ ¬P7(x,z). In this case, the axiom should not be read as an
instruction for adding one.
Best,
Wolfgang
Am 03.11.2022 um 08:55 schrieb Wolfgang Schmidle via
Crm-sig<[email protected]>:
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
_______________________________________________
Crm-sig mailing list
[email protected]
http://lists.ics.forth.gr/mailman/listinfo/crm-sig
