Fundamental Predicates and Axioms
Identity and Naming
\[\forall e : \text{Entity}(e) \rightarrow \exists \text{id}, \text{name} : \text{HasID}(e, \text{id}) \land \text{HasName}(e, \text{name})\]
where \(\text{HasID}(e, \text{id})\) means entity \(e\) has unique identifier \(\text{id}\), and \(\text{HasName}(e, \text{name})\) means entity \(e\) has name \(\text{name}\).
\[\forall e_1, e_2 : \text{Entity}(e_1) \land \text{Entity}(e_2) \land \text{HasID}(e_1, \text{id}) \land \text{HasID}(e_2, \text{id}) \rightarrow e_1 = e_2\]
Identity is functionally determined by ID.
RecordType Structure
\[\begin{split}\forall r : \text{RecordType}(r) \rightarrow \exists \text{props}, \text{parents} : \\
\text{HasProperties}(r, \text{props}) \land \text{HasParents}(r, \text{parents}) \land (\text{parents} \neq \emptyset \lor r \text{ is root})\end{split}\]
\[\begin{split}\forall r : \text{RecordType}(r) \land \text{HasParents}(r, \text{parents}) \land r' \in \text{parents} \rightarrow \\
\text{RecordType}(r') \land (r' \neq r)\end{split}\]
Parents must be distinct RecordTypes; this prevents self-inheritance.
\[\forall r : \text{RecordType}(r) \rightarrow \exists p : \text{HasProperties}(r, p)\]
RecordTypes can have zero or more Properties attached.
Property Definition and Attachment
\[\begin{split}\forall p : \text{Property}(p) \rightarrow \exists \text{dtype}, \text{unit}, \text{desc} : \\
\text{HasDataType}(p, \text{dtype}) \land \text{HasUnit}(p, \text{unit}) \land \text{HasDescription}(p, \text{desc})\end{split}\]
\[\forall p : \text{Property}(p) \land \text{HasDataType}(p, \text{dtype}) \rightarrow \text{DataType}(\text{dtype})\]
\[\begin{split}\forall r : \text{RecordType}(r) \land p \in \text{HasProperties}(r) \rightarrow \\
\exists \text{imp} : \text{HasImportance}(p, \text{imp}) \land (\text{imp} \in \{\text{obligatory}, \text{recommended}, \text{suggested}\})\end{split}\]
Properties attached to RecordTypes have an importance level.
\[\begin{split}\forall r : \text{RecordType}(r) \land \text{HasProperties}(r, p_1) \land \text{HasProperties}(r, p_2) \land p_1 \neq p_2 \rightarrow \\
\neg \exists \text{name} : \text{HasName}(p_1, \text{name}) \land \text{HasName}(p_2, \text{name})\end{split}\]
A RecordType cannot have duplicate property names.
Record Instantiation
\[\forall x : \text{Record}(x) \rightarrow \exists rt : \text{HasRecordType}(x, rt) \land \text{RecordType}(rt) \land rt \neq \emptyset\]
Every Record must have at least one RecordType.
\[\begin{split}\forall x : \text{Record}(x) \land \text{HasRecordType}(x, rt) \rightarrow \\
\forall p \in \text{HasProperties}(rt) : \text{HasImportance}(p, \text{obligatory}) \rightarrow \\
\exists \text{val} : \text{HasPropertyValue}(x, p, \text{val}) \land \text{val} \neq \text{null}\end{split}\]
Records must provide values for all obligatory properties of their RecordTypes.
\[\begin{split}\forall x : \text{Record}(x) \land \text{HasRecordType}(x, rt_1) \land \text{HasRecordType}(x, rt_2) \land rt_1 \neq rt_2 \rightarrow \\
\neg(\exists \text{conf} : \text{ConflictingProperties}(rt_1, rt_2, \text{conf}))\end{split}\]
Multiple RecordType membership is allowed unless properties conflict.
\[\begin{split}\forall x : \text{Record}(x) \rightarrow \forall p : \text{HasPropertyValue}(x, p, \text{val}) \rightarrow \\
\exists rt : \text{HasRecordType}(x, rt) \land p \in \text{HasProperties}(rt)\end{split}\]
A Record can only have values for properties defined in its RecordTypes.
Property Values and DataTypes
\[\begin{split}\forall x : \text{Record}(x) \land p : \text{Property} \land \text{val} : \\
\text{HasPropertyValue}(x, p, \text{val}) \land \text{HasDataType}(p, \text{dtype}) \rightarrow \\
\text{MatchesType}(\text{val}, \text{dtype})\end{split}\]
Property values must conform to their declared datatype.
\[\begin{split}\forall \text{dtype} : \text{DataType}(\text{dtype}) \rightarrow \\
(\text{dtype} = \text{TEXT} \lor \text{dtype} = \text{INTEGER} \lor \text{dtype} = \text{DOUBLE} \lor \\
\text{dtype} = \text{DATETIME} \lor \text{dtype} = \text{FILE} \lor \text{dtype} = \text{BOOLEAN} \lor \\
\exists rt : \text{dtype} = \text{REFERENCE}(rt))\end{split}\]
\[\begin{split}\forall \text{dtype}, \text{element\_dtype} : \text{DataType}(\text{dtype}) \land \text{dtype} = \text{LIST}(\text{element\_dtype}) \rightarrow \\
\text{DataType}(\text{element\_dtype})\end{split}\]
LIST is a parameterized container type.
\[\begin{split}\forall x : \text{Record}(x) \land p : \text{Property} \land \text{HasDataType}(p, \text{REFERENCE}(rt)) \land \\
\text{HasPropertyValue}(x, p, \text{val}) \rightarrow \text{Record}(\text{val}) \land \text{HasRecordType}(\text{val}, rt)\end{split}\]
Reference properties point to Records of a specific RecordType.
Inheritance and Property Propagation
\[\begin{split}\forall r : \text{RecordType}(r) \land \text{HasParents}(r, \{r_1, r_2, \ldots, r_n\}) \rightarrow \\
\forall r_i \in \{r_1, \ldots, r_n\} : \forall p_i \in \text{HasProperties}(r_i) : \\
p_i \in \text{HasProperties}(r)\end{split}\]
Inherited properties are not duplicated.
\[\begin{split}\forall r : \text{RecordType}(r) \land \text{HasParents}(r, \text{parents}) \land \\
\text{parent\_props} = \bigcup\{\text{HasProperties}(r_p) \mid r_p \in \text{parents}\} \rightarrow \\
\text{HasProperties}(r) \supseteq \text{parent\_props}\end{split}\]
A RecordType inherits all properties from all parents.
\[\begin{split}\forall x : \text{Record}(x) \land \text{HasRecordType}(x, rt) \land \text{HasParents}(rt, \text{parents}) \rightarrow \\
\forall \text{parent} \in \text{parents} : \text{HasRecordType}(x, \text{parent})\end{split}\]
Records implicitly satisfy parent RecordTypes (virtual inheritance).
File References
\[\forall f : \text{File}(f) \rightarrow \exists \text{path} : \text{FilePath}(f, \text{path}) \land \text{path is valid}\]
\[\forall f : \text{File}(f) \rightarrow \exists x : \text{Record}(x) \land \text{LinkedTo}(x, f)\]
Files can be linked to Records.
\[\begin{split}\forall f : \text{File}(f) \land \text{LinkedTo}(x, f) \rightarrow \\
\forall p \in \text{CustomProperties}(x, f) : \text{Property}(p) \land \text{HasPropertyValue}(x, p, \text{val})\end{split}\]
Files linked to Records can have custom properties.
Identifiability (for Data Synchronization)
\[\begin{split}\forall rt : \text{RecordType}(rt) \rightarrow \exists \text{id\_props} : \\
\text{IsIdentifiable}(rt, \text{id\_props}) \land \text{id\_props} \subseteq \text{HasProperties}(rt)\end{split}\]
\[\begin{split}\forall x_1, x_2 : \text{Record}(x_1) \land \text{Record}(x_2) \land \text{HasRecordType}(x_1, rt) \land \\
\text{HasRecordType}(x_2, rt) \land \text{IsIdentifiable}(rt, \text{id\_props}) \rightarrow \\
\left(\forall p \in \text{id\_props} : \text{HasPropertyValue}(x_1, p, v) \land \text{HasPropertyValue}(x_2, p, v)\right) \\
\leftrightarrow x_1 = x_2\end{split}\]
Identifiable properties uniquely determine record equality.
Derived Predicates and Constraints
Type Hierarchy Consistency
\[\forall r : \text{RecordType}(r) \rightarrow \neg(\exists \text{cycle} : r \in \text{Parents}^*(r))\]
No circular inheritance allowed; \(\text{Parents}^*\) is the transitive closure.
\[\text{Ancestors}(r) := \{r' \mid \exists n \geq 0 : r' \in \text{Parents}^n(r)\}\]
Ancestors includes the type itself and all parent hierarchy.
Data Integrity Constraints
\[\begin{split}\forall x : \text{Record}(x) \rightarrow \\
(\exists \text{val} : \text{HasPropertyValue}(x, p, \text{val}) \land \text{val} \neq \text{null}) \lor \\
(\exists rt : \text{HasRecordType}(x, rt) \land p \in \text{HasProperties}(rt) \land \\
\neg(\text{HasImportance}(p, \text{obligatory})))\end{split}\]
Every Record has values only for required or defined optional properties.
\[\begin{split}\forall p : \text{Property}(p) \rightarrow \neg(\exists r_1, r_2 : \\
\text{HasProperties}(r_1, p) \land \text{HasProperties}(r_2, p) \land \\
\text{HasDataType}(p, d_1) \land \text{HasDataType}(p, d_2) \land d_1 \neq d_2)\end{split}\]
A Property globally has exactly one datatype across all uses.
Importance-Based Property Requirements
\[\begin{split}\forall x : \text{Record}(x) \land rt : \text{HasRecordType}(x, rt) \rightarrow \\
\forall p \in \text{AllProperties}(rt) : \\
(\text{HasImportance}(p, \text{obligatory}) \rightarrow \text{HasPropertyValue}(x, p) \neq \text{null}) \land \\
(\text{HasImportance}(p, \text{recommended}) \rightarrow \text{optional}) \land \\
(\text{HasImportance}(p, \text{suggested}) \rightarrow \text{optional})\end{split}\]
\[\begin{split}\text{AllProperties}(rt) := \text{HasProperties}(rt) \cup \\
\bigcup\{\text{HasProperties}(r_p) \mid r_p \in \text{Ancestors}(rt)\}\end{split}\]
Collect all properties including inherited ones.
