Issue 607: formal representation of FOL axioms in CRM

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 (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 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/1OyRrIAIZ52QrLrgABW3sqfzaQXKcvE9c8CHW...

See you  next week,

Christian-Emil