Philosophyhttps://www.ormfoundation.org:443/forums/62.aspxThis forum is for discussing the philosophy and history of ORMenCommunityServer 2007.1 (Build: 20917.1142)Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1264.aspxWed, 03 Sep 2008 14:46:16 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1264VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1264.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1264<p>Hi Brian,</p>
<p>The example is quoted almost verbatim from Dr Halpin's thesis (See Proof 1, p. 'A-4' of Dr Halpin's thesis).<br /><br />Perhaps you may dignify this forum by adding commentary on your comments "In the image you attached to the post, it looks like the sample population table entries are not sufficient to indicate the choice of constraints used. Beside the [ a ][ b ], [ a ][ c ], I think you'd need [ d ][ b ] (at least) to complete the constraints for that Fact Type. Is that an oversight, a truncation of the image, or something else?"</p>
<p>Or is it that we reserve dignity exclusively for ourselves, and not others?</p>
<p>There's not, but this forum is available to a potential audience of billions of people. Forgive me if I chose to leave my post with "Oh...that's cool.... Thank you Dr, I think that opens up some fairly interesting possibilities in ORM research.".</p>
<p>Best regds<br />Victor</p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1258.aspxMon, 01 Sep 2008 17:40:37 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1258VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1258.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1258<p>Hi Brian,<br /><br />Thank you for participating. If you want to ask questions about isomorphism in general, you might like to start a different thread. Answers to my questions may answer yours.</p><p>Is there an echo in here?<br /><br />An answer fitting to the quality of that question...</p>
<p>I used to have a wheelbarrow like that...but the wheels fell off! It was just the darndest thing...<br />OR<br />'no, neither, you need to read more books'. None of which are probably the answer you wee looking for. I am sorry, I said I don't want to discuss it any further.<br /><br />For further research, see p. 'A-4' of DR Halpin's thesis, and ponder "<font size="2" face="Arial">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)? </font><font size="2" face="Arial">The answer to that is the answer to your question."</font><br /><br />Best regds<br />Victor</p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1257.aspxMon, 01 Sep 2008 17:01:33 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1257Brian Nalewajek0https://www.ormfoundation.org:443/forums/thread/1257.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1257<p> Hi Victor, <br /></p><p>I think there's a question I can ask of you that I trust will lend itself to a simple answer (if it's a trick question,or has transcendental implications, I sure don't see it that way). In the image you attached to the post, it looks like the sample population table entries are not sufficient to indicate the choice of constraints used. Beside the [ a ][ b ], [ a ][ c ], I think you'd need [ d ][ b ] (at least) to complete the constraints for that Fact Type. Is that an oversight, a truncation of the image, or something else?</p><p>BRN.. <br /></p><p> </p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1256.aspxMon, 01 Sep 2008 14:33:49 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1256VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1256.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1256<p>Hi Brian,</p>
<p>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. </p>
<p>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.<br /></p>
<p>I chose the passage, in part poetic and cryptic...because it was found in 'Coptic'.</p>
<p>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.</p>
<p>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.<br />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.<br /><br />Best regds<br />Victor<br /></p>
<p> </p>
<p> </p>
<p><br /></p>
<p> </p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1255.aspxMon, 01 Sep 2008 10:59:36 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1255Brian Nalewajek0https://www.ormfoundation.org:443/forums/thread/1255.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1255<p> Hi Victor,</p><p>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?</p><p>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.</p><p>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)?</p><p>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. </p><p>BRN.. <br /></p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1253.aspxMon, 01 Sep 2008 04:50:05 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1253VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1253.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1253<div><font size="2" face="Arial">Hi Brian,</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">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.</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">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.</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">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'.</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">I am not the teacher Brian, so I will only offer this by way of quote to the Gospel of Thomas:</font></div>
<div><font size="2" face="Arial"></font> </div>
<div>"Whoever has ears to hear, let him hear." (Gospel of Thomas, 8)</div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">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)?</font></div>
<div><font size="2" face="Arial">The answer to that is the answer to your question.</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">2. When you consider '611173585038267632043' as a 'message', then '45432454509 * 13452356727' is a valid 'interpretation' of that message.</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">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).</font></div>
<div><font size="2" face="Arial"></font> </div>
<div><img src="http://www.ormfoundation.org/forums/ORM-KL-Isomorphism.png" alt="ORM-KL-Isomorphism" align="middle" border="0" width="801" height="375" /></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial"><b>NB</b> 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?</font></div>
<div><font size="2" face="Arial"></font> </div>
<div> </div>
<div><font size="2" face="Arial">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.<br /></font></div>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">Before I provide them...let me repeat the message "Whoever has ears to hear, let him hear".....</font></div>
<div><font size="2" face="Arial">A warning...the following may be hard to take for lovers of ORM, Godel and Proof Theory...</font></div><font size="2" face="Arial"></font>
<blockquote>
<div><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><br />"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."</div>
<div> </div>
<div>"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."</div>
<div> </div>
<div>"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."</div>
<div> </div>
<div>"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]"</div>
<div> </div>
<div>"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]"</div>
<div> </div>
<div>"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." </div>
<div><br />"the main reason for introducing KL was the additional facility to REASON about properties of ORM models in a formal setting.'</div></blockquote>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">and more...<br /></font></div><font size="2" face="Arial"></font>
<blockquote>
<div><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><font size="2" face="Arial"></font><br />[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].</div></blockquote>
<div><font size="2" face="Arial"></font> </div>
<div><font size="2" face="Arial">I'll leave it there Brian. I remain yours,</font></div><div> </div>
<div><font size="2" face="Arial">Best regds</font></div>
<div><font size="2" face="Arial">Victor</font></div>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1251.aspxSun, 31 Aug 2008 15:16:13 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1251Brian Nalewajek0https://www.ormfoundation.org:443/forums/thread/1251.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1251<p> Hi Victor,</p><p>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.</p><p>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.</p><p>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!</p><p>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.</p><p>Look forward to your ORM visual proof examples - another perspective always helps.</p><p>BRN.. <br /></p><p> <br /></p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1250.aspxFri, 29 Aug 2008 22:33:46 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1250VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1250.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1250<font size="2">
</font><p><font size="2">Hi Brian,</font><font face="Times New Roman"><font size="3"> </font></font></p><font face="Times New Roman"></font><font size="2">
</font><p><font size="2">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.</font><font face="Times New Roman"><font size="3"> </font></font></p><font face="Times New Roman"></font><font size="2">
</font><p><font size="2">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.</font><font face="Times New Roman"><font size="3"> </font></font></p><font face="Times New Roman"></font><font size="2">
<p>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). </p>
<p>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. </p>
<p>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. </p>
<p>To answer your 'triangle' question by way of analogy, let's look at a lot less obvious example..and another take on 'sameness'. </p>
<p>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 <i>both</i> ways. </p>
<p>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. </p>
<p>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). </p>
<p>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'.</p>
<p>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)." </p>
<p>In a second post/response post to your question, I'll give you a few demos of that using ORM and KL. </p>
<p>I hope this is a worth while introduction to isomorphism, Terry's work and of some value to the ORM community. </p>
<p><b>NB</b> Notice that in none of this did we speak of 'Relational Databases' or 'Transformation Rules'. What an odd thing that is! <br />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.<br /></p></font><font size="2"></font>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1249.aspxFri, 29 Aug 2008 09:18:45 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1249Brian Nalewajek0https://www.ormfoundation.org:443/forums/thread/1249.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1249<p> Hi Victor,</p><p>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?</p><p>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.</p><p>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,<br /></p><p>BRN.. <br /></p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1248.aspxWed, 27 Aug 2008 15:50:58 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1248VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1248.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1248<p>Hi Terry,</p>
<p>Oh...Okay. Well that's pretty cool. I would never have known that from the literature that I've read.</p>
<p>Thank you Dr, I think that opens up some fairly interesting possibilities in ORM research.<br /><br />Best regds<br />Victor<br /><br />PS I've still got the question, "what else is isomorphic with ORM?" but perhaps that is another thread.</p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1247.aspxWed, 27 Aug 2008 15:30:10 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1247Terry Halpin0https://www.ormfoundation.org:443/forums/thread/1247.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1247<p class="MsoNormal" style="MARGIN:0in 0in 0pt;"><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';">Hi Victor</span></p>
<p class="MsoNormal" style="MARGIN:0in 0in 0pt;"><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';"></span> </p>
<p class="MsoNormal" style="MARGIN:0in 0in 0pt;"><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';">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.</span></p>
<p class="MsoNormal" style="MARGIN:0in 0in 0pt;"><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';"></span> </p><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';">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.</span><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';"> </span><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';">Cheers</span><span style="FONT-SIZE:11pt;COLOR:#1f497d;FONT-FAMILY:'Calibri','sans-serif';">Terry</span>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1246.aspxWed, 27 Aug 2008 15:19:51 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1246VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1246.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1246<p>Hi Terry,</p>
<p>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.</p>
<p>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.</p>
<p>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!</p>
<p>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.</p>
<p>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?</p>
<p>In that way, I see the paper opening up proof theory to graphical notations that are accepted within the mathematical community as 'formal theories'.</p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1245.aspxWed, 27 Aug 2008 14:44:14 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1245Terry Halpin0https://www.ormfoundation.org:443/forums/thread/1245.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1245<p>Hi Victor</p>
<p>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. </p>
<p>Cheers</p>
<p>Terry</p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1244.aspxWed, 27 Aug 2008 14:27:13 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1244VictorMorgante0https://www.ormfoundation.org:443/forums/thread/1244.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1244<p>Hi Terry,</p>
<p>Thank you. Unfortunately, for me that just restates and reaffirms the question.</p>
<p>Best regds<br />Victor</p>Re: Hilbert's Program and the Formalisation of ORMhttps://www.ormfoundation.org:443/forums/thread/1243.aspxWed, 27 Aug 2008 13:51:44 GMT9d039735-a311-4a8d-9c49-a0bb2572af9e:1243Terry Halpin0https://www.ormfoundation.org:443/forums/thread/1243.aspxhttps://www.ormfoundation.org:443/forums/commentrss.aspx?SectionID=62&PostID=1243<p>Hi Victor,</p>
<p>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.</p>
<p>Hope this clarifies the issues you raised</p>
<p>Terry</p>