In the 54th CIDOC CRM & 47th FRBR/LRMoo SIG Meeting, upon discussing the redefinition of P7 took place at (issue 606), the SIG decided to start a new issue concerning how to set up the FOL axioms found in the CRM specification document.
Things to be considered:
- allowing the use of as many free variables as possible in FOL axioms (understood as having an implicit universal reading) instead of adding unnecessary existential quantifiers;
- whether free variables can they appear within the scope of another quantifier (f.i., the axiom for P7)
- (∃u) [E4(x) ˄ E18(u) ˄ E53(y) ˄ P157(y,u) ˄ E53(z) ˄ P157(z,u) ˄ E53(v) ˄ P157(v,u) ˄ P7(x,y) ˄ P161(x,z) ˄ P89(z,v) ˄ P89(v,y) ] ⇒ P7(x,v)
- whether free variables can they appear within the scope of another quantifier (f.i., the axiom for P7)
could be rendered as:
-
-
- (E4(x) ˄ E53(y) ˄ E53(z) ˄ E53(v) ˄ (∃u) (E18(u) ˄ (P157(y,u) ˄ P157(z,u) ˄ P157(v,u)))˄ P7(x,y) ˄ P161(x,z) ˄ P89(z,v) ˄ P89(v,y)) ⇒ P7(x,v)
- Or in a set-theoretical notation:
E4(x) ˄ E53(y) ˄ E53(z) ˄ E53(v) ˄ ((∃u ∈ E18) [P157(y,u) ˄ P157(z,u) ˄ P157(v,u)]) ˄ P7(x,y) ˄ P161(x,z) ˄ P89(z,v) ˄ P89(v,y) ⇒ P7(x,v) - also, set theoretical notation in class declarations helps to better understand the axioms or is it considered overall cumbersome?
-
- the concept of equality btw instances of classes that has been assumed for P161 is a newly introduced one. Before resorting to using it in an ad hoc manner, the SIG should consider what the implications of declaring equality among individual instances of classes are.
- (∃u) [E92(x) ˄ E53(y) ˄ E53(z) ˄ E18(u) ˄ P157(y,u) ˄ P157(z,u) ˄ P161(x,y) ˄ P161(x,z) ] ⇒ (z = y)
- prior knowledge to be rewritten in the definition of axioms or is there any other way to represent background assumptions (should they be represented somehow)?
- Possibility of minimising FOL statements to the absolutely necessary inferences or keep whatever has been added in the FOL sections in the specification document?
The basis for the FOL definitions (except for the logical constants used throughout the CRM specification document though) should be:
Meghini, C. and Doerr, M. (2018). ‘A first-order logic expression of the CIDOC conceptual reference model’, International Journal of Metadata, Semantics and Ontologies, 13(2), pp. 131–149. doi: 10.1504/IJMSO.2018.098393.
HW: CEO, WS, MD to collaborate on that. Contact CM as well.
Rome, September 2022
Post by Wolfgang Schmidle (17 October 2022)
Dear All,
Some phenomenal or unique declarative thingies behave like functions and can be more clearly described as such. This would make many "∃" in the FOL descriptions superfluous. Therefore I propose to introduce function symbols in the FOL. Some examples are given below.
Best,
Wolfgang
Example 1: E93 Presence as a function of a Physical Thing or STV and a Time-Span
E18 Physical Thing x P46 is composed of E18 Physical Thing y
implies that there is a E52 Time-Span z with:
x P195i had presence E93 Presence u P164 is temporally specified by z
y P195i had presence E93 Presence w P164 is temporally specified by z
w P10 falls within u
P46(x,y) ⇒ (∃z,u,w) [E52(z) ∧ E93(u) ∧ P195i (x,u) ∧ P164(u,z) ∧ E93(w) ∧ P195i (y,w) ∧ P164(w,z) ∧ P10(w,u)]
While the (∃z) is fine, the (∃u,w) is grating. Although not wrong, it doesn't catch the fact that a Presence is uniquely determined by any Physical Thing or STV plus any Time-Span.
To express this, we can introduce an additional function symbol "F93" in the FOL for E93:
u = F93(x,z) ⇒ E93(u) ∧ [E18(x) ∨ E92(x)] ∧ E52(z)
u = F93(x,z) ⇔ [P195(u,x) ∨ P166(u,x)] ∧ P164(u,z)
(E93 and F93 are not more repetitive than e.g. P14 and P14.1.)
And then in the FOL for P46, we can write:
P46(x,y) ⇒ (∃z) [ P10(F93(y,z), F93(x,z)) ]
Example 2: P161 has spatial projection, as a function of an STV and a Physical Thing as reference space
P7 took place at:
E4 Period x P7 took place at E53 Place y
implies that there is an E18 Physical Thing u with:
y is at rest relative to u, and the spatial projection z of x relative to u is contained in y
P7(x,y) ⇒ (∃u,z) [E18(u) ∧ P157(y,u) ∧ E53(z) ∧ P161(x,z) ∧ P157(z,u) ∧ P89(z,y) ]
Since the spatial projection of a STV is unique if a reference space is specified, one can introduce a function symbol F161:
z = F161(x,u) ⇒ E53(z) ∧ E92(x) ∧ E18(u)
z = F161(x,u) ⇔ P161(x,z) ∧ P157(z,u)
Then the statement above becomes
P7(x,y) ⇔ (∃u) [P157(y,u) ∧ P89(F161(x,u), y)]
And if one adds a property P7.1 "relative to":
P7.1(x,y,u) ⇔ P7(x,y) ∧ P157(y,u)
then one can write is as
P7.1(x,y,u) ⇔ P89( F161(x,u), y)
P167 was within:
E93 Presence x P167 was within E53 Place y
E93 Presence x P161 has spatial projection E53 Place z P89 falls within E53 Place y
P167(x,y) ⇔ (∃z) [E53(z) ∧ P161(x,z) ∧ P89(z,y)]
If one includes the reference space:
P167(x,y) ⇔ (∃z,u) [E53(z) ∧ E18(u) ∧ P157(y,u) ∧ P161(x,z) ∧ P157(z,u) ∧ P89(z,y)]
This can be written as
P167(x,y) ⇔ (∃u) [P157(y,u) ∧ P89(F161(x,u), y)]
(However, this might change according to the results of issue 606.)
Example 3: P156 occupies, P196 defines
E18 Physical Thing x P156 occupies E53 Place y
define y = F156(x)
E18 Physical Thing x P196 defines E92 Spacetime Volume y
define y = F196(x)
(E4 Period, before it became a subclass of E92 Spacetime Volume, would have been similar.)
From the P156 scope note:
This property implies the fully developed path from E18 Physical Thing through P196 defines, E92 Spacetime Volume, P161 has spatial projection to E53 Place. However, in contrast to P156 occupies, the property P161 has spatial projection does not constrain the reference space of the referred instance of E53 Place.
P156(x,y) ⇔ (∃z) [E18(x) ∧ E53(y) ∧ P196(x,z) ∧ P161(z,y) ∧ P157(y,x)]
This can be written as
F156(x) = F161(F196(x), x)
P8 took place on or within:
E4 Period x P8 took place on or within E18 Physical Thing y
E4 Period through x P7 took place at E53 Place z P156i is occupied by E18 Physical Thing y
P8(x,y) ⇐ (∃z) [E53(z) ∧ P7(x,z) ∧ P156(y,z)]
P8(x,y) ⇐ P7(x, F156(y))
P195 was a presence of:
E93 Presence x P195 was a presence of E18 Physical Thing y
E93 Presence x P166 was presence of E92 Spacetime Volume z P196i is defined by E18 Physical Thing y
P195(x,y) ⇔ (∃z)[E92(z) ∧ P166(x,z) ∧ P196i(z,y)]
(in the scope note the shortcut is given in the wrong direction, and typo "P166(z,x)" corrected)
P195(x,y) ⇔ P166(x, F196(y))
Example 4: P168 place is defined by
E53 Place z P168 place is defined by E94 Space Primitive y
define z = F168(y)
P171 at some place within:
E53 Place x P171 at some place within E94 Space Primitive y
E53 Place x P89 falls within E53 Place z P168 place is defined by E94 Space Primitive y
through a declarative Place z that is not explicitly documented
P171(x,y) ⇔ (∃z) [E53(z) ∧ P89(x,z) ∧ P168(z,y)]
P171(x,y) ⇔ P89(x, F168(y))
P172 contains:
E53 Place P172 contains E94 Space Primitive
P172(x,y) ⇔ (∃z) [E53(z) ∧ P89i(x,z) ∧ P168(z,y)]
P172(x,y) ⇔ P89(F168(y), x)
Post by Wolfgang Schmidle (18 October 2022)
One more thing: Often one is not really interested in naming a Physical Thing that creates the shared reference space between two places. Thus, if it hasn't been done yet, I propose a new property:
Pn "shares reference space with", with domain and range E53 Place
Pn(x,y) would be a (strong) shortcut for (∃u) [E18(u) ∧ P157(x,u) ∧ P157(y,u)]. P89 "falls within" would be a subproperty of Pn. Probably P121 "overlaps with" and P122 "borders with" as well. (P189 "approximates" would technically be another candidate but I don't understand it well enough to have an opinion.)
If we introduce function symbols, one can additionally define:
F161a: spatial projection relative to the reference space of
z = F161a(x,y) ⇒ E53(z) ∧ E92(x) ∧ E53(y)
z = F161a(x,y) ⇔ (∃u) [E18(u) ∧ P157(y,u) ∧ z = F161(x,u)] ⇔ Pn(y,z) ∧ P161(x,z)
(the second "⇔" by definition of F161, minimising scope of u and definition of Pn)
And yes, the tentative naming scheme for the function symbols is not ideal.
Continuation of Example 2:
P7 took place at:
P7(x,y) ⇒ (∃u,z) [E18(u) ∧ P157(y,u) ∧ E53(z) ∧ P161(x,z) ∧ P157(z,u) ∧ P89(z,y) ]
new:
P7(x,y) ⇒ (∃z) [E53(z) ∧ Pn(y,z) ∧ P161(x,z) ∧ P89(z,y) ]
or even
P7(x,y) ⇒ (∃z) [E53(z) ∧ P161(x,z) ∧ P89(z,y) ]
P7(x,y) ⇔ (∃u) [E18(u) ∧ P157(y,u) ∧ P89(F161(x,u), y)]
new:
P7(x,y) ⇔ P89(F161a(x,y), y)
And one last thing: I realised that the right-hand side is exactly the same for P7 and P167 "was within":
P167(x,y) ⇔ (∃z,u) [E53(z) ∧ E18(u) ∧ P157(y,u) ∧ P161(x,z) ∧ P157(z,u) ∧ P89(z,y)]
The only difference is:
P7(x,y) ⇒ E4(x)
P167(x,y) ⇒ E93(x)
(and ⇒ for P7 versus ⇔ for P167, but I guess this can be rectified)
F161a(x,y) works for both because x is an E92 Spacetime Volume.
Which reminds me of something I had written to Christian-Emil about issue 606:
P7 cannot be a superproperty of P161 because of the E4 / E92 domains.
Why don't you simply declare it a "quasi subproperty", i.e. the P161(x,y) ∧ E4(x) ⇒ P7(x,y) in your new P161 FOL description, and then stop?
Or why don't you extend the domain of P7 (or P167) to E92? I don't see anything in the P7 / P167 scope notes that wouldn't be applicable to any STV. The label "took place at (witnessed)" would be slightly awkward, but that's it.
But it is easily possible that I have overlooked something here.
Post by Wolfgang Schmidle (19 October 2022)
Now that Carlo has entered the conversation, I have another one:
The .1 properties are called e.g. P14(x,y,z) in the FOL expressions. However, everywhere else they are called e.g. P14.1:
* Introduction, "About the logical expressions used in the CIDOC CRM": "we use P14.1 as the ternary predicate symbol corresponding to property P14.1 in the role of"
* The scope notes use the P14.1 notation
* Meghini & Doerr 2018 call them P14.1 (or rather, P14.x)
I don't see a reason why they should be named differently in the FOL.
Best,
Wolfgang
Post by Carlo Meghini (19 October 2022)
Hello,
I don't see a reason why they should be named differently in the FOL.
Neither do I, I forgot why we did not use the ".1" notation in FOL. Maybe because it's a bit unconventional, but then, we can do what we want ...
Carlo
Post by Christian-Emil Ore (2 December 2022)
Dear all,
I have written a short document about the FOL in the axioms. Wolfgang has sent a few emails to the list regarding the issue. You will find links and my HW in https://docs.google.com/document/d/1OyRrIAIZ52QrLrgABW3sqfzaQXKcvE9c8CH…;
See you next week,
Christian-Emil