Issue 483: 7.0 preparation - CRMbase review for inconsistencies

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 15/4/2020

Dear All,

Here my analysis of transitivity.
 

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 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]

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.

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/edit#

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 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 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 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 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

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]