ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] mKR proof of correctness

To: "Patrick J. Hayes" <phayes@xxxxxxx>
Cc: William Thomas <wthomas@xxxxxxxxxxxxxxxx>, "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>, "Richard S. Latimer" <rslatimer@xxxxxxx>, KR-language <kr-language@xxxxxxxxxxxxxxx>, David Kelley <dkelley@xxxxxxxxxxxxxxxx>
From: "Richard H. McCullough" <rhmccullough@xxxxxxxxx>
Date: Thu, 3 Apr 2014 23:40:32 -0700
Message-id: <COL129-W60A87C2FB42B30CA72B3B2CB6F0@xxxxxxx>
Pat

To put it most simply:

Yes, I take Ayn Rand's book, "Introduction to Objectivist Epistemology"
to be a true description of human epistemology.

Yes, the design and intent of the mKR language is to be able
to "say" very precisely what Rand's book says.
In the broader view, this means that mKR can express conceptual ideas
in a way that is equivalent to the way people express conceptual ideas.
 mKR is designed to be like a simplified, precise, concise natural language.

Dick McCullough
Context Knowledge Systems
mKE and the mKR language
mKR/mKE tutorial

> Subject: Re: mKR proof of correctness
> From: phayes@xxxxxxx
> Date: Thu, 3 Apr 2014 22:20:23 -0500
> CC: ontolog-forum@xxxxxxxxxxxxxxxx; sowa@xxxxxxxxxxx; kr-language@xxxxxxxxxxxxxxx; rslatimer@xxxxxxx; dkelley@xxxxxxxxxxxxxxxx; wthomas@xxxxxxxxxxxxxxxx
> To: rhm@xxxxxxxxxxxxx; rhmccullough@xxxxxxxxx
>
>
> On Apr 3, 2014, at 12:14 AM, Richard H. McCullough <rhmccullough@xxxxxxxxx> wrote:
>
> > Folks, I'm starting to get really confused about who said what to whom.
> >
> > So, I'm just going to repeat what I said to Pat,
> > because this is important.
>
> Pat is beginning to wonder why he ever got involved in this conversation, but...
>
> > The Objectivist Axioms describe the epistemology of man --
> > how he perceives and conceives the external world.
> > They are the foundation of all man's languages
> > and knowledge.
>
> Let me try to get my understanding of your position clear. Do you regard Rand's writings as in some sense foundational? So that to conform with her ideas (assuming that you can show that your notation does so conform, but let us assume that for now) constitutes, in your view, a **proof** of their objective correctness? That is, the writings of Rand constitute a kind of empirical test of objective truth?
>
> It would be useful to get this clear before delving into details.
>
> Pat
>
>
>
> >
> > Dick McCullough
> > Context Knowledge Systems
> > mKE and the mKR language
> > mKR/mKE tutorial
> >
> > > Subject: Re: mKR proof of correctness
> > > From: phayes@xxxxxxx
> > > Date: Wed, 2 Apr 2014 22:21:15 -0500
> > > CC: ontolog-forum@xxxxxxxxxxxxxxxx; sowa@xxxxxxxxxxx; kr-language@xxxxxxxxxxxxxxx; rslatimer@xxxxxxx;dkelley@xxxxxxxxxxxxxxxx; wthomas@xxxxxxxxxxxxxxxx
> > > To: rhm@xxxxxxxxxxxxx; rhmccullough@xxxxxxxxx
> > >
> > >
> > > On Apr 2, 2014, at 5:10 PM, Richard H. McCullough <rhmccullough@xxxxxxxxx> wrote:
> > >
> > > > John
> > > >
> > > > I don't want there to be any doubt about what I'm saying,
> > > > so I'm devoting one extra email to this topic.
> > > >
> >
> > > The mKR language is proved semantically correct
> > > > because the mKR run-time system guarantees
> > > > that the Objectivist Axioms are satisfied.
> > >
> > > I actually laughed out loud when I read this. First, I have no idea what you mean by proving a lan
> guage to be semantically correct, but claiming anything semantic **because some axioms are present** misses the entire point of having semantics in the first place, which is to connect formal sentences with claims about the actual world. Then again there is your conflation of semantics with a 'run-time system', which I take it means a system that performs inferences. But without an independent semantics, how does one know that these inferences are valid or complete? The general problem of proving that a program is correct is still open, of course, but any approach to even defining what this means requires that the language of the program has some kind of separate semantics. If the run-time system *Is* the semantics then 'correctness' is trivial to prove - the program does what the program does - but also trivially meaningless. But the final howler here is the idea that Ayn Rand's thoughts might have anything, even the shred of a remotest connection, to do with correctness, in any sense of that word.
> > >
> > > IF your notation had a semantic theory that would enable an objective check to be made on its validity, and IF you could then show that those axioms were satisfied AND that your run-time system preserved truth (or whatever your semantics calls it), then you might reasonably claim that mKE had a property that one might
> call Randianicity: conformity to the thoughts of Ayn Rand. But to call this property "semantic correctness" is simply farcical.
> > >
> > > Pat Hayes
> > >
> > >
> > > >
> > > > Dick McCullough
> > > > Context Knowledge Systems
> > > > mKE and the mKR language
> > > > mKR/mKE tutorial
> > >
> > > ------------------------------------------------------------
> > > IHMC (850)434 8903(850)434 8903(850)434 8903 home
> > > 40 South Alcaniz St. (850)202 4416(850)202 4416(850)202 4416 office
> > > Pensacola (850)202 4440(850)202 4440(850)202 4440 fax
> > > FL 32502 (850)291 0667(850)291 0667(850)291 0667 mobile (preferred)
> > > phayes@xxxxxxx http://www.ihmc.us/users/phayes
> > >
> > >
> > >
> > >
> > >
> > >
>
> ------------------------------------------------------------
> IHMC (850)434 8903(850)434 8903 home
> 40 South Alcaniz St. (850)202 4416(850)202 4416 office
> Pensacola (850)202 4440(850)202 4440 fax
> FL 32502 (850)291 0667(850)291 0667 mobile (preferred)
> phayes@xxxxxxx http://www.ihmc.us/users/phayes
>
>
>
>
>
>

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

<Prev in Thread] Current Thread [Next in Thread>