Sign in | Join | help in Philosophy How to ORM (Entire Site)

# The ORM Foundation

Get the facts!

## Hilbert's Program and the Formalisation of ORM

Last post Wed, Sep 3 2008 15:46 by VictorMorgante. 17 replies.
 Page 1 of 2 (18 items) 1 2 Next > Sort Posts: Oldest to newest Newest to oldest Previous Next

#### Hilbert's Program and the Formalisation of ORM

 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 regdsVictor 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-orientedperspective (PHD Thesis).

#### Re: Hilbert's Program and the Formalisation of ORM

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

#### Re: Hilbert's Program and the Formalisation of ORM

 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 regdsVictor

#### Re: Hilbert's Program and the Formalisation of ORM

 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

#### Re: Hilbert's Program and the Formalisation of ORM

 Hi Terry, Thank you. Unfortunately, for me that just restates and reaffirms the question. Best regdsVictor

#### Re: Hilbert's Program and the Formalisation of ORM

 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

#### Re: Hilbert's Program and the Formalisation of ORM

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

#### Re: Hilbert's Program and the Formalisation of ORM

 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.  I agree with you that ORM's rich graphical language makes it easy to "see" many proofs directly using diagrams. For that reason, I have often described ORM as "visual logic". At one stage, we even thought of using this term for a series of conferences, but unfortunately that term is already trademarked by a company. CheersTerry

#### Re: Hilbert's Program and the Formalisation of ORM

 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 regdsVictorPS I've still got the question, "what else is isomorphic with ORM?" but perhaps that is another thread.

#### Re: Hilbert's Program and the Formalisation of ORM

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

#### Re: Hilbert's Program and the Formalisation of ORM

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