7.0 preparation - CRMbase review for inconsistencies

In the 46th joint meeting of the CIDOC CRM SIG and ISO/TC46/SC4/WG9; 39th FRBR - CIDOC CRM Harmonization meeting; The sig accepted   all additions of *instance(s) of* prior to identifiers for classes across the document and  reviewed the proposed comments suggested by CEO.  Notes were kept during the meeting in the CEO's copy file. The minutes on this issue can be found here.

Also the crm-sig, concerning the  Examples missing from definitions of classes and properties, decided that they have to be filled before the next CRM sig meeting. They are either to be treated in a separate issue or as part of this one. 
CRM-sig asked CB shared with the sig a list of the classes and properties lacking examples and assigned HW to MD and SS to provide with examples. 

Athens, February 2020

Posted by Martin on 1/4/2020

Checking the minutes:

"E4 Period

DECISION: the paragraph below, was marked *to be deleted*. The sig decided to delete it for the moment, and assigned MD [HW] to check if it was alright to delete it after all.

Consequently, an instance of E4 Period may occupy a number of disjoint spacetime volumes, however there must not be a discontinuity in the timespan covered by these spacetime volumes. This means that an instance of E4 Period must be contiguous in time. If it has ended in all areas, it has ended as a whole. However, it may end in one area before another, such as in the Polynesian migration, and it continues as long as it is ongoing in at least one area"

I encounter the following problem:

An STV is allowed to be a finite set of contiguous volumes. That allows Periods, such as France, to spread over separate Places, as intended.

E53 Place does not define it to be contiguous. No problem, but it could cause ambiguity, is a spatial projection is one or more places.

STV however in not defined contiguous in time, but has a contiguous temporal projection. That can be understood indirectly to require contiguity in time, and Periods to be contiguous in time as required.

We allow intersections of STVs with places and STVs to be STVs. That can create STVs that are not contiguous in time. Whereas intersections of STVs contiguous in time with time-spans = Presence, must be contiguous in time.

Solution:

Forbid in scope note of STV the intersections with STV and Place.

Make explicit that an instance of E53 Place can be a finite set of contiguous areas.

Make explicit in E4 Period that they are contiguous in time.

OR: Require that E4 Period are STVs which are contiguous in time. That would mean that intersections of Periods are STVs but not Periods. That should be OK, and can be noted in the scope note of E4.

Then, temporal projections of STV may be sets of time-spans. Is increasing cardinality OK? How to express incomplete knowledge in this case?

Posted by Martin on 8/4/2020

Dear All,

I hope this finds you all well!

Here my rewriting of P121, P122. Since the temporal overlap properties disappeared, I stressed the the fact that the Roman Empire overlaps with the Federal Republic of Germany, which scholars may object to, confusing STV with E53 Place.

I changed one example of P121, to stress the case of one country occupying an area of another one, which causes a spatial overlap.

Posted by Martin 15/4/2020

Dear All,

Here my analysis of transitivity.
 

Posted by editorial team of the version 7.0 on 30/4/2020

The editorial team of crm-sig for the version 7.0 collected scattered comments and forgotten colored marked text of the version CIDOC CRM v.6.2.9 that were not parts of particular issues for review. The list of scattered can be found here.

The team worked on this and prepared proposals for discussing in the next sig. 

30/4/2020

Posted by Martin on 4/5/2020

P102 has title (is title of)

Domain:              E71 Human-Made Thing

Range:                E35 Title

Subproperty of:   E1 CRM Entity. P1 is identified by (identifies): E41 Appellation

Quantification:    many to many (0,n:0,n)

Scope note:         This property associates an instance of E35 Title has been applied to an instance of E71 Human-Made Thing.

The P102.1 has type property of the P102 has title (is title of) property enables the relationship between the title and the thing to be further clarified, for example, if the title was a given title, a supplied title etc.

It allows any human-made material or immaterial thing to be given a title. It is possible to imagine a title being created without a specific object in mind.

Examples:          

§  the first book of the Old Testament (E33) has title “Genesis” (E35)

has type translated (E55)

        NEW examples:     

§  Monet’s painting from 1868-1869 held by Musée d'Orsay, Paris, under inventory number RF 1984 164 (E24) has title “La Pie” (E35)

has type creator’s title (E55)

Posted by Martin on 5/5/2020

Dear All,

Attached my homework on E33 Lingustic Object. I found it necessary to harmonize with P165 as well.

Best,

Martin 

Posted by Martin on 6/5/2020

Dear All,

Here my proposals for better examples of titles. I kindly ask our colleagues from IFLA to check or correct the terms I have used for the P102.1 property. Please comment.

Best,

Martin

P102 has title (is title of)

Domain:              E71 Human-Made Thing

Range:                E35 Title

Subproperty of:   E1 CRM Entity. P1 is identified by (identifies): E41 Appellation

Quantification:    many to many (0,n:0,n)

Scope note:         This property associates an instance of E35 Title has been applied to an instance of E71 Human-Made Thing.

The P102.1 has type property of the P102 has title (is title of) property enables the relationship between the title and the thing to be further clarified, for example, if the title was a given title, a supplied title etc.

It allows any human-made material or immaterial thing to be given a title. It is possible to imagine a title being created without a specific object in mind.

Examples:          

• the first book of the Old Testament (E33) has title “Genesis” (E35)

has type translated (E55)

    NEW:         

• Monet’s painting from 1868-1869 held by Musée d'Orsay, Paris, under inventory number RF 1984 164 (E24) has title “La Pie” (E35)

has type creator’s title (E55)

• Monet’s painting from 1868-1869 held by Musée d'Orsay, Paris, under inventory number RF 1984 164 (E24) has title “The Magpie” (E35)

has type translation of creator’s title (E55)

• The science fiction film directed by Ridley Scott from 1982 based on the novel “Do Androids Dream of Electric Sheep?” by Philip K. Dick (E73) has title “Blade Runner” (E35)

has type creator’s title (E55)  [Michael Deeley, the producer, bought the title for “a nominal fee,” from William Burroughs, who had written a book called Blade Runner (https://www.vulture.com/2017/10/why-is-blade-runner-the-title-of-blade-runner.html)]

• The painting by Matthias Grünewald from 1516AD, permanently exhibited in the church Mariä Krönung in Stuppach, 97980 Bad Mergentheim, Germany (E24) has title “Die Stuppacher Madonna” (E35)

has type vernacular, popular title (E55) [The work has no known title from the artist. It is currently named              after its current place of exhibition]

Posted by Martin on 6/5/2020

Dear All,

Here my attempt to harmonize E33 Linguistic Object with P190 and P165.

Obviously, the question of how to define a symbolic specificity for the identity of some symbolic object different from that of one of its representative resources has not been solved sufficiently.

Please comment.

Sent it by Christian Emil to editorial team of CRM version 7.0  on 12/5/2020

Dear all,
 These are the operators I would prefer. 

                A satisfies ¬φ if and only if A does not satisfy φ
                A satisfies (φ ∧ ψ) if and only if A satisfies both φ and ψ
                A satisfies (φ ∨ ψ) if and only if A satisfies at least one of either φ or ψ
                A satisfies (φ → ψ) if and only if it is not the case that A satisfies φ but not ψ
                A satisfies (φ ↔ ψ) if and only if A satisfies both φ and ψ or satisfies neither one of them

In FOL we also have the existential and universal quantifiers:
∃ and ∀

The axiom for P52 being a short cut will then be (font: cambria math)

P52(x,y)  ← (∃z)[E(8) ˄ P24i(x,z) ˄ P22(z,y) ]

with implicit universal quantifiers for x,y since they are unbound variables.

Personally, I think this is the clearest notation and I suggest we use it.  It is not in harmony with the Martin&Carlo-paper where the unfamiliar ⊂  is used. 

By the way, ∃ and ∀ look like E mirrored and A upside down. The origin for ∃ and ∀​ is said to be that the logicians used typewriters, To type the quantifiers they typed the text and then insertet the sheet of paper upside down and typed the quantifiers.

Posted by CEO on 21/5/2020

Dear all,
Please find attached my homework on transitivity. I have also uploaded the document to the folder issues to be discussed.
 

Sent it  by Christian Emil  to the editorial team of the version 7.0 on 21/5/2020

I have rewritten the section 'About the logical expressions of the CIDOC CRM'  as a part of my homework. 
The main change is that ³ is replaced with the more common arrow → and  ≣  is replaced with ↔

E13(x) ³ E7(x) becomes E13(x) → E7(x) 

Show transitivity be added to the FOL expression?

The document is attached and loaded into the general issue google folder.
https://docs.google.com/document/d/12AKFscYuIIumiP9jEy4V8QTM4wwqG__M/ed…

sent it  by Martin to the editorial team of the version 7.0 on 21/5/2020

Good text! Should we insert a reference (see also) to the terminology section wrt classes and properties?
 

sent it  by George to the editorial team of the version 7.0 on 25/5/2020

Dear all,

Aesthetically, I prefer the horse shoe for 'if' and the triple bar for 'if and only if', but just because that's how I learned symbolic logic. This version looks good too. Two questions about the truth table though:

1. why do we have two 'reads' columns?

2. are the truth value translations in the right order? I think conjunction has been defined in relation to negation, disjunction as conjunction and negation as disjunction? 

sent it by Christian Emil to the editorial team of the version 7.0 on 25/5/2020

1) It may be better and sufficient with one read column.

2) It is possible to define disjunction in terms of conjunction and negation and conjunction in terms of disjunction and negation. Implication in terms of disjunction and negation: 

A and B:  not (not A or not B) 

A or B:     not (not A and not B)

A implies B: not A or B

A iff B:          A implies B and B implies A

​In the table I just sketched the operators.

I have no strong opinion about horseshoe, single arrow or double arrow. I am used to => for implication and  <=> for equivalence, and  single arrow -> from lambda calculus and type theory. The horseshoe is the least familiar one to me. 

sent it  by Martin to the editorial team of the version 7.0 on 25/5/2020

Dear All,

I prefer as few "NOT" as possible. A "NOT NOT" will confuse anybody not trained in logic.

I prefer the two reads.

I am used to I am used to => for implication and  <=> for equivalence, may be German tradition. I have seen the horse shoe first time from Carlo, and find it least intuitive.

sent it  by George to the editorial team of the version 7.0 on 25/5/2020

Dear Christian Emil et al.,

I didn't mean to ignite a debate over the formalism. What is proposed looks fine. As long as it is consistently applied across the text, it works for me. It was a comment on personal stylistic preference (the horseshoe symbol is a very common one, the one with which I was trained). The symbols, however, are arbitrary and the formalism proposed works very nicely. 

Re the definition, I understand that formal logical statements can be defined in relation to one another, but in the version I was reading, I just thought that the definitions of the truth value had slipped to the wrong lines. 

It's looking great.

sent it  by Martin to the editorial team of the version 7.0 on 25/5/2020

Dear George,

Well, I think it is always interesting, if there are several identifiable communities with different traditions we could mention in the text.

I refer to my studies in mathematics in Germany.

Personally, the horseshoe confused me, because it is opposite to the subclass of. 

As such, I think another symbol is definitely better, but I have no idea in which schools the horseshoe is popular

sent it by Martin to the editorial team of the version 7.0 on 27/5/2020

Again here the E4 issue. I suggest my second solution. Do not delete the phrase. Increase cardinality of temporal projection.
 

sent it by Christian Emil to the editorial team of the version 7.0 on 28/5/2020

Dear all,

I have checked my old books in logic etc.  I also found a definition site

https://en.wikipedia.org/wiki/Logical_connective

clearly written by a computer scientist.  This page has a partial history copied in at the bottom

In many of the books I consulted ↔, ⇔ are symbols for bidirectional implication (equivalence), while ≡ is (in the same texts) used as a definition operator. In my opinion we should use ≡ only for defintions and ↔ or ⇔ for bidirectional implications, so the defintion of ⇔  can be written as: 

A ⇔ B ≡ A ⇒ B ∧  B ⇒ A

In modern (higher order) type theory/ category theory and lambda calculus it seems to be a tendency to use ⇔ and ⇒ since →  (arrow) is used in the definition of functions, eg. f: A→ B, f is a function with A as domain and B as range. The ⇒ is then used in proofs.

I, personally, will prefer ⇒.  We can ask Mark and Günther(?) what they would prefer

History of notations

...

Implication: the symbol → can be seen in Hilbert in 1917;[8] ³ was used by Russell in 1908[4] (compare to Peano's inverted C notation); ⇒ was used in Vax.[9]

Biconditional: the symbol ≡ was used at least by Russell in 1908;[4] ↔ was used at least by Tarski in 1940;[10] ⇔ was used in Vax; other symbols appeared punctually in the history such as ³⊂ in Gentzen,[11] ~ in Schönfinkel[6] or ⊂³ in Chazal.[12]

...

sent it by Martin to the editorial team of the version 7.0 on 30/5/2020

Dear Christian-Emil,

Is there any kind of standard associated with that? I share your preference for the double arrows.

sent it by Christian Emil to the editorial team of the version 7.0 on 30 /5/2020

Dear Martin,

I don't think there is a standard. ³ I will consider old fashion and historical. Peano was Italian, maybe that is why Carlo prefer it.

⇒ and →: Since → is also used to denote the type of functions e.g. A →B and rewriting,  I would prefer ⇒. See the attachments (1) (2). 

On the other hand → is widely used as the implication sign.

As long as we give the sign we will use a definition in the introduction the choice is ours

sent it by Martin  to the editorial team of the version 7.0 on 1 /6/2020

Dear All,

Following the last discussion of the CRM editing team, I propose a change of scope note for P139:

OLD

P139 has alternative form

Domain:              E41 Appellation

Range:                E41 Appellation

Quantification:    many to many (0,n:0,n)

Scope note:         This property establishes a relationship of equivalence between two instances of E41 Appellation independent from any item identified by them. It is a dynamic asymmetric relationship, where the range expresses the derivative, if such a direction can be established. Otherwise, the relationship is symmetric. The relationship is not transitive.

The equivalence applies to all cases of use of an instance of E41 Appellation. Multiple names assigned to an object, which are not equivalent for all things identified with a specific instance of E41 Appellation, should be modelled as repeated values of P1 is identified by (identifies).

P139.1 has type allows the type of derivation, such as “transliteration from Latin 1 to ASCII” be refined..

Examples:          

• • "Martin Doerr" (E41) has alternative form "Martin Dörr" (E41) has type Alternate spelling (E55)
  • "Гончарова, Наталья Сергеевна" (E41) has alternative form "Gončarova, Natal´â Sergeevna" (E41) has type ISO 9:1995 transliteration (E55)
  • “Αθήνα” has alternative form “Athina” has type transcription.

NEW

Scope note:         This property associates an instances of E41 Appellation with another instances of E41 Appellation that constitutes a derivative or variant of the former and that may also be used for identifying items identified by the former, in suitable contexts, independent from the particular item to be identified. This property should not be confused with additional variants of names used characteristically for a single, particular item, such as individual nick names. It is a dynamic asymmetric relationship, where the range expresses the derivative, if such a direction can be established. Otherwise, the relationship is symmetric. The relationship is not transitive.

The equivalence applies to all cases of use of an instance of E41 Appellation. Multiple names assigned to an object, which are not equivalent for all things identified with a specific instance of E41 Appellation, should be modelled as repeated values of P1 is identified by (identifies).

P139.1 has type allows the type of derivation, such as “transliteration from Latin 1 to ASCII” be refined..

On virtual meeting of CIDOC CRM editorial team for version 7.0 2/6/2020 

The editorial team reviewed the  decision of the 46th sig meeting during the next virtual meeting and decided  to NOT delete the following paragraph

"Consequently, an instance of E4 Period may occupy a number of disjoint spacetime volumes, however there must not be a discontinuity in the timespan covered by these spacetime volumes. This means that an instance of E4 Period must be contiguous in time. If it has ended in all areas, it has ended as a whole. However, it may end in one area before another, such as in the Polynesian migration, and it continues as long as it is ongoing in at least one area"

NEW ISSUE(s)

• make clear that the scope note of E53 can be sets of contiguous areas
• Change the cardinality of the temporal projection property of STV → P160 [it’s one to one and has to change]

Posted by George Bruseker on 9/6/2020

Dear all,

In the course of doing editorial work for CRM base version 7.0 a discussion was launched on the symbols used in the FOL representation of CRM, particularly the characters for implication and for equivalence / if and only if. 

They have until now been represented as:

implication  ³

equivalence / if and only if ≡

It is now proposed that they be represented as: 

implication  ⇒

equivalence / if and only if ⇔

Both forms of notation are used in different communities. The argument for making this change is that the horseshoe confuses people who work in set theory, and the proposed new symbols are well known and do not clash with other symbol sets.

In order to vote on this issue, please use the following form. 

https://forms.gle/QzvH9qEHYJTrNsAK9

Please vote by June 19th.