in

The ORM Foundation

Get the facts!

Hilbert's Program and the Formalisation of ORM

Last post 09-03-2008 15:46 by VictorMorgante. 17 replies.
Page 1 of 2 (18 items) 1 2 Next >
Sort Posts: Previous Next
  • 08-22-2008 4:27

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

  • 08-22-2008 12:42 In reply to

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

  • 08-22-2008 14:46 In reply to

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

     

     

  • 08-27-2008 14:51 In reply to

    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

  • 08-27-2008 15:27 In reply to

    Re: Hilbert's Program and the Formalisation of ORM

    Hi Terry,

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

    Best regds
    Victor

  • 08-27-2008 15:44 In reply to

    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

  • 08-27-2008 16:19 In reply to

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

  • 08-27-2008 16:30 In reply to

    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
  • 08-27-2008 16:50 In reply to

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

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

  • 08-29-2008 10:18 In reply to

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

  • 08-29-2008 23:33 In reply to

    Re: Hilbert's Program and the Formalisation of ORM

    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.

    You may have seen in another post where I made the analogy of Dr Halpin's thesis acting like a Rosetta Stone. In many ways it does. The truely beautiful thing about the Rosetta Stone is that it provided the means by which the first accurate interpretation of the graphical language, 'Hieroglyphics', was achieved. Nothing new there. But let's look deeper into that. The stone has the same decree in three languages, Hieroglyphics, Greek and Demotic, where Heiroglyphics is a graphically written language, and written Greek and Demotic are written as linear symbolic arrangements of symbols. Of course, the graphics of Hieroglyphics are 'symbols' too, but nobody alive knew what they meant until the first successful translation was performed. Even then, the translation was an incredible feat of cryptoanalytics. The gentleman who eventually cracked the heiroglyphic 'code', Champollion, studied for many years how to read ancient Greek, Demotic, and ancient Coptic. Up until the first successful translation, it was thought by many that each hieroglyph was an entire word, or idioms of an idiomatic language like written Chinese. It took a flash of inspiration to realise that each hieroglyph represented a sound, and it must have been amazing the first time someone stood in front of hieroglyphics and sounded out ancient Coptic for the first time in well over 1000 years. It turns out that heiroglyphics spells out ancient Coptic (See Simon Singh's 'Code Book' for a good read on that).

    Why tell that story? The cryptoanalytic nature of 'cracking' that code (Heiroglyphics and ancient Coptic), relied on finding an 'isomorphism' between the two languages. As an interesting task, search the internet for 'Cryptography Isomorphism'...they are tied together in a science. So the art of translating 'languages' may be reduced to serious mathematical concepts in that regard. Once that isomorphism was established between heiroglyphics and ancient Coptic, it opened up a tremendous wealth of opportunity to study and understand the intrinsic meaning behind the arrangement of hieroglyphs.

    There are actually two important analogies in that one story. The first is that Dr Hapin's PHD thesis is the result of an intuitive step of being able to 'formalise' ORM by mapping an isomorphism from Naim/ORM to formal logic by way of the first-order-logical theory, 'KL'. The second is that the 'decree' written in 3 languages on the Rosetta Stone (i.e. the 'message'), is the 'same' decree. Otherwise we may still be scratching our heads at heiroglyphics.

    To answer your 'triangle' question by way of analogy, let's look at a lot less obvious example..and another take on 'sameness'.

    Archimedes provided the proof that the area of a circle is the area of a right angle triangle with a base equal to the circumference, and the height equal to the radius of the circle. Imagine that! How many times do you look at a circle, and think of a triangle? i.e. When you think of isomorphisms, the two systems under analysis may 'look' completely different, and yet there is a bridge between them. You can study one, and know for certain that you know truths about the other. And, importantly, the bridge can be crossed both ways.

    In the same way, isomorphisms provide a bridge between different areas of mathematics. If you can solve a problem using the tools of one branch of mathematics, and if you know that there exists an isomomorphic bridge to another branch of mathematics...then you can solve the problem in the branch that is most easy for you to work in...and then 'flip' the result over to the other branch of mathematics.

    Dr Halpin didn't just formalise ORM. That's easy...you can create any-old-graphical-language, give it a set of axioms and inference rules and call it 'formalised' (if you wanted to).

    What Dr Halpin did was prove the isomorphism between Niam (ORM) and a first order logical theory, KL...a 1:1 correspondence between the two (like heiroglyphics and ancient Coptic). That is the real value of Dr Halpin's work to my mind. Because before then, there was no basis for hard-core mathematicians to access ORM and trust it as a robust language capable of formal first-order-logic. i.e. When we say 'formalisation of ORM', I always think of 'formalised logic' and the relationship between ORM and KL...rather than the relatively simple task of 'creating a language'.

    So, this thread started out by saying "if ORM is a formal logic, with a 1:1 correspondence with a FOL, then I should be able to do proofs in ORM (as you can in a language of FOL like KL)."

    In a second post/response post to your question, I'll give you a few demos of that using ORM and KL.

    I hope this is a worth while introduction to isomorphism, Terry's work and of some value to the ORM community.

    NB Notice that in none of this did we speak of 'Relational Databases' or 'Transformation Rules'. What an odd thing that is!
    i.e. To some, ORM is a means of getting the most consise, accurate and practicle relational table designs possible, while to others ORM is a means to access formal logic. There will always be that dichotomy I guess, and that is another bridge, or isomorphism (relational databases to formal logic), that you may think about. Of course, that too is covered in Dr Halpins thesis and with reference to Codd and the work of Nijssen etc.

  • 08-31-2008 16:16 In reply to

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

     

  • 09-01-2008 5:50 In reply to

    Re: Hilbert's Program and the Formalisation of ORM

    Hi Brian,
     
    You and I share enough mails off-line for me to know that if you just wanted the answer, you'd ask me off-line. So, in fear of being led around by socratic method, let me flip this in a way that only an Aussie would and say that because I started this thread...I kinda get to be the one to play Socrates.
     
    In reading your response in leiu of a thank you, I remain a little unconvinced. i.e. If you know enough about isomorphism, you wouldn't need an example.
     
    I am sure that you would agree that it is one thing to read of Champollion and another to understand what he did, it is one thing to read of Turin cracking the enigma code and it is another thing to understand how he did it, it is one thing to apprecate that two geometric shapes have the same area...and another entirely to understand the reason 'why'.
     
    I am not the teacher Brian, so I will only offer this by way of quote to the Gospel of Thomas:
     
    "Whoever has ears to hear, let him hear." (Gospel of Thomas, 8)
     
    1. When you perform 45432454509 * 13452356727 on paper in pencil, do you consider your 'working' in the answer, or do you consider 611173585038267632043 (the answer)?
    The answer to that is the answer to your question.
     
    2. When you consider '611173585038267632043' as a 'message', then '45432454509 * 13452356727' is a valid 'interpretation' of that message.
     
    3. The following is a theorem in ORM and a set of 'theorems' in KL. A 'proof' is a set of theorems. As a hint, please note that nORMa is smart enough to tell that something is up, and raises a little red flag  (see picture).
     
    ORM-KL-Isomorphism
     
    NB For the student: Has nORMa interpreted the 'message'? If so, what does that 'interpretation' look like when you write it in KL? If you were to take that interpretation in KL and draw it as an ORM diagram....what would it look like?
     
     
    It is worth noting that there are PHDs who would argue that you can't do proofs in ORM. The following are quotes from PHDs.... and it is worth nothing that they are the same ones reading and assessing your (the audience) papers for the ORM conference. There's nothing person there, because I don't know who they are.
     
    Before I provide them...let me repeat the message "Whoever has ears to hear, let him hear".....
    A warning...the following may be hard to take for lovers of ORM, Godel and Proof Theory...

    "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.'
     
    and more...

    [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].
     
    I'll leave it there Brian. I remain yours,
     
    Best regds
    Victor

  • 09-01-2008 11:59 In reply to

    Re: Hilbert's Program and the Formalisation of ORM

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

  • 09-01-2008 15:33 In reply to

    Re: Hilbert's Program and the Formalisation of ORM

    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

     

     


     

Page 1 of 2 (18 items) 1 2 Next >
© 2008-2014 The ORM Foundation: A UK not-for-profit organisation -------------- Terms of Service