The ORM Foundation

Hi all,

At the turn of the last century and with the burgening of formal theories in mathematics, Hilbert lay down a challenge to mathematicians the world over to find solutions to the most pressing and challenging unsolved problems in mathematics.

Among those problems was proving the consistency of the formal theories, the 'toolboxes' if you will, used by mathematicians as the very basis for proofs, especially within (also burgening) proof theory.

In what became known as 'Hilbert's Program' it was evident, from the outset, that if you are going to prove the consistency of a formal theory...it needs to be proven within the precepts of the theory itself. The reason for this is that "If you prove consistency of theory A using the tools of theory B...then how can you be absolutely sure that theory B is consistent?" (Nagel & Newman, 2001, p. 24-44).

Godel has the distinction of proving the consistency of first order logic (FOL) and the incompleteness of a set of theories based on higher order logic (HOL). Within each set of proofs, he stuck to the tenet of Hilbert's program and worked within the precepts of the formal theories under analysis.

With Dr Halpin's doctoral thesis, and the formalisation of ORM, we are led to the consistency of ORM (Niam) under the tenets of the isomorphic relationship between ORM and KL (a FOL formulated within the paper). i.e. The paper 'proves' the consistency of ORM (a formal theory) under the precepts of another formal theory (KL).

So, I have a few questions. What is it about this one paper that allows it to seemingly break from the tenets of Hilbert's program? What is it about the isomorphism of ORM and KL that leads us to believe that there is absolutely no doubt that we can take the consistency of KL as proof of the consistency of ORM? Is it that we are saying (and indeed accepting) that ORM and KL are 100% isomorphic?

If ORM and KL are isomorphic, then why does the paper question the work of Leung who tried to prove the consistency of ORM using ORM (Halpin, 1989, p. '3-9')? If KL and ORM are 100% isomorphic, then if you do proofs in KL...you do proofs in ORM. Isomorphism doesn't work only one way....it works both ways.

Best regds
Victor

References (I've had requests to expand on references made in this post):

Nagel E. & Newman J. 2001, Gödel’s Proof. rev. ed. New York University Press.

Halpin T. A. 1989, A Logical Analysis of Information Systems: static aspects of the data-oriented
perspective (PHD Thesis).

 Hi Victor,

Is your question about the legitimacy of the proof of Object Role Modeling?  From your post I read: Godel proves FOL.  KL is a FOL (so proven by Godel). KL proves ORM.  

Regarding the implications and limitations of isomorphism, I'm out of my depth.  My assumption is that there is a distinction between isomorphism and complete equivalence = identity (as it is for similarity in geometry - triangles having equal angles, but not equal sides; therefore similar, but not identical).  Can the isomorphic aspects of KL/ORM allow the proof of ORM from the proven FOL (KL), yet allow distinctions between KL and ORM?  If so, I can see where accepting KL as a proof of ORM would be acceptable, where accepting ORM as a proof of ORM would not.

Am I getting close?

BRN..

Hi Brian,

Thank you for contributing and please forgive me, if you want to start a new thread on isomorphism in general, then i'm happy to answer your question there. The appropriate answer to my question may answer yours.

Best regds
Victor

Hi Victor,

In my PhD thesis I defined a formal system, KS, that comprised not just a language (KL) but also axioms and inference rules. It is these additions to the language that enabled me to provide both a model theory and a proof theory for NIAM (a precursor to ORM), enabling formal proofs of theorems such as whether one specific ORM schema is logically equivalent to another. The thesis also provided an algorithm for mapping a NIAM schema to a set of logical formulae, which I assume underlies the isomorphism that you are talking about. In my thesis I mentioned the work of others such as Leung, but did not disparage them in any way, instead merely pointing out that they did not go all the way in providing a rigorous model theory and proof theory for NIAM.

Hope this clarifies the issues you raised

Terry

Hi Terry,

Thank you. Unfortunately, for me that just restates and reaffirms the question.

Best regds
Victor

Hi Victor

Apparently, I don't understand your original question. In my proofs, I make use of logical inference rules such as Modus Ponens and Substitutivity of Indenticals. I do not find such rules in the ORM language itself, so I'm not sure what you mean by doing proofs in ORM.

Cheers

Terry

Hi Terry,

I just found that when I read your paper, it maps the isomorphism between Niam (ORM) and the formal theory used to do the proofs so well that when I see the Niam models, I see the proof of the formal theory.

When I couple this with the fact that I learned Niam well before reading the paper, I had already accepted Niam as a formal theory, with axioms and inference rules. In fact we were taught that Niam came with a set of (effective) axioms and (definitely) inference rules.

So, now (some 13 years later), as I start to build an(other) ORM based modeling tool, I'm thinking...I bet you my bottom dollar I can get an ORM model to generate it's own proof of inconsistency/mal-formedness in KL. i.e. work the isomorphism the other way...from ORM to KL. i.e. redo all the proofs in the paper...in ORM!

In that way, I see 'proofs' done in ORM. Which I feel makes sense...because if we want to accept ORM as a formal theory (and speak of 'axioms of orm', 'well formed theorems in ORM' etc), then at some stage we are going to have to accept that you can do proofs in ORM.

i.e. How is it that we can possibly reject that Hilbert's program says that if we want to prove the consistency of a formal theory, we need to do it in the formal theory under analysis, without rejecting Godels completeness theorem and 1st,2nd incompleteness theorems...the very basis on which ORM is founded?

In that way, I see the paper opening up proof theory to graphical notations that are accepted within the mathematical community as 'formal theories'.

Hi Victor

I’m OK with doing some formal proofs directly and visually in the ORM graphical language, such as using some of the schema transform theorems that I proved in my thesis, but this is justified because I have shown that such proofs can be algorithmically transformed into proofs in a logical system such as KS.

Hi Terry,

Oh...Okay. Well that's pretty cool. I would never have known that from the literature that I've read.

Thank you Dr, I think that opens up some fairly interesting possibilities in ORM research.

Best regds
Victor

PS I've still got the question, "what else is isomorphic with ORM?" but perhaps that is another thread.

 Hi Victor,

I see you received some clarification from Dr. Halpin, in the exchange.  There is, apparently, agreement that ORM can provide "proofs."  Could you provide an example, so that I can put this thread into context.  I'm unclear as to what type of ORM model is said to provide such proofs (all syntactically correct ORM models, or only self referencing ORM meta-models).  Is it that whatever an ORM model depicts is said to be proven as a theory, therm, axiom - even if that theory's only application is that of the target domain of the model?

To some extent, when you talk about "visual" logic, are we getting back to a parallel (appropriate linguistic device), with geometrical analogies I put forward concerning similar triangles?  You began with isomorphism (same form).  I can see where two ORM models (each of a unique application domain), that have the same diagrammatic elements, with the same connections between elements, would be isomorphic - even if the displayed elements differed in their placement, names, reference modes, etc....  From that, I could take that the two models are logically equivalent, yet semantically distinct.  This is part of the thinking I'm including on an article about degrees of ORM correctness.  However, I'm not at all sure this is what you are talking about in this thread.

Please do provide a couple of examples to help me see the context of your question/assertion.  Also, please be specific indicating the terms: ORM theory, a theory derived from ORM theory, from an ORM model, etc....  I'd like to better understand the your questions and assertions.  Thanks,

BRN..

Hi Brian,

Well, you've set me a bit of a task there, as I operate best as a student. But if you allow me to provide examples by way of a teachers lot in life...that of always being a student, then no problem..I am more than happy to share what I know.

I'll provide a few analogies and examples of isomorphism first, to work up to the examples. Also, I can't actually do a better job than Dr Halpin, so with Dr Halpin's indulgence, I'll use examples from Dr Halpin's PHD thesis.

 Hi Victor,

You put together a pretty good narrative.  I think it would make the basis of a worthwhile article, that you can post here, or elsewhere.  It should make a good introduction of the mathematical liniage and links between FOL, KL, KS and ORM theory.

As it happens, I know a fair bit about Champollion's use of "cartouches" (pharaohnic name rings - referring to the same instance of the same Object Type -King), in each of the three scripts.  I've also had an interest in cryptanalysis, and the breaking of codes (ciphers, actually), such as the "Ultra" (Enigma), Purple and JN2 (Imperial Japaneses diplomatic and navel codes).  Working with ORM, I've often considered the analysis that's done as part of the ORM methodology, and the work of those like Allen Turing, William Friedman and others.  There certainly are deeply rooted connections.  There are other subject areas and diciplines that resonate with ORM ideas - Rodger Penrose and his work on tiling comes to mind.  I also have a general appreciation of the concept of isomorphism; how a tea cup and a doughnut are of the same basic surface area type - just squeezed an stretched indifferent ways.

What I was really asking for was an explicit example of an ORM model, what that model "proves" and some annotation about the correspondence between the ORM model elements, and that which is proved.  As you said such an example will be provided, I'll keep an eye out for that - interesting stuff!

I know your primary personal interest in ORM is in this area of translation, transposition, isomorphism and similar conceptually powerful tools.  I hope that you don't overlook the significance of the Relational Model.  It may seem that the process of creating highly compliant databases is a rather pedestrian endeavor; but I think the significance goes far beyond the practical utility of the resulting databases themselves.  There actually are some direct connections between the central ideas of the Relational Model and cryptography, information governance and other important subject areas.  Sure, you don't have  to understand much of anything about the RM to use a tool, or apply an algorithm to fashion one - you might even hit on one by chance.  However, I think an appreciation of the well considered basis for the RM can only help.  I don't think I'd do a very good job at all, of creating RM compliant schema, without a tool like nORMa, or the directives and constraints of the ORM methodology.  I'm not good at doing things by route; I have to have a sense of the ideas behind the methods.  I'm still learning more about the RM and its implications; but have already done enough to give it, and the resulting data structures due credit.

Look forward to your ORM visual proof examples - another perspective always helps.

BRN..

"the fact that in ORM one can only represent facts, whereas in theories like KL and PM one not only represents facts but also the PROOFS of properties of facts."

 

"One could also say that KL is complemenetary to ORM in the sense that ORM provides the facilities to represent facts, whereas KL offers the extra facility to also REASON about these facts."

 

"KL offers deduction rules (a la Gentzen, and/or semantic tableaus a la Beth) and provides facilities to actually do proofs about properties of ORM  models. You do the proofs in KL, and not in ORM."

 

"In [formal theories like KL and PM] you also do the actual proofs (of, e.g. the property 1+1 = 2) [,you can't do proofs in ORM]"

 

"Godel introduced an ingenious coding of not only facts but also proofs of properties of facts as numbers in number theory. [you can't do isomorphic proofs in ORM]"

 

"Inspection of [an ORM diagram] shows no representation of logic (in the sense of deduction rules and proofs), hence an important part of a formal system a la KL [..] is lacking." 

"the main reason for introducing KL was the additional facility to REASON about properties of ORM models in a formal setting.'

[The proof above in KL is] obviously [..] an intensional proof of contradiction [..] and at least verifiably correct and complete) while the "Population Table" [(in the ORM diagram above)] is unnecessary and therefore confusing extensional interpretation. It does not [provide an isomorphic interpretation of the theorems of KL] but at most -trivially!- "illustrates" the proof for people not able to read [KL].

 Hi Victor,

Should I take it as significant that you quoted an apocryphal book, rather than choosing a near identical quote from one of the canonical gospels?

While I have considered connections and implications for a number of the subject areas you mentioned; I haven't come close to looking at KL, KS, and the literature on derivations and parallels with FOL, to the degree that you obviously have.  I hadn't seen (or thought to look for), "authoritative" pronouncements on the ability or suitability of using ORM diagrams as proofs.  Even if I had, that would be only the first step in considering the validity of those statements - and I'm guessing you've gone a few steps beyond that.

I would like to ask you a question in earnest (that may be better to branch off as a separate thread): Are the sample population aspects of the ORM methodology, an intrinsic part of formal ORM theory?   (bringing in the mention of the feature in the last of your quotes into play) In some other ORM tools, you could use sample populations to suggest or determine internal uniqueness constraint assignments (given a significant sample).  If one folows inevitably from the other, they both can't be essential.  As far as KL, KS, and a formal assessment of ORM are concerned, do you start with constraints or sample populations? Are formal proofs in ORM possible without the concept of sample populations?  Does at least that part of the quote have validity (the condescending tone, not withstanding)?

I've taken the sample population feature of the ORM methodology as being part of several steps; but especially of use in verification of the model with domain experts/ knowledge workers.  Given that few of them would be well versed in KL symbolic language, its expressive power is hardly trivial.  I just haven't done the work to be able to say one way or another; I figured you might.

BRN..

Hi Brian,

No problem. I think that in the quality of your questions it shows that you have almost made the leap without me, if you haven't by the time I write this.

The master is TH on this one, and for me to say any more would be to re-write the thesis in question. I don't want to say any more.

I chose the passage, in part poetic and cryptic...because it was found in 'Coptic'.

Not really, it's just that I read the classics to find inspiration. It's kinda funny, though, how that ties back to the Rossetta Stone.

The analogy is that to understand many of the agnostic 'sayings', you need to make your own intuitive leap to what it is they are talking about.
i.e. You answered your own question within the question...if you don't include the Fact Table...it does not translate to it's own proof in KL.

Best regds
Victor