Re: [ontolog-forum] mKR proof of correctness

["Richard H. McCullough" <rhm@xxxxxxxxxxxxx>]

David

You're doing a good job of pinning down the meaning of my vague statements.

So let me try again.
The program/language/knowledgebase (mKE/mKR/mKB)) will never violate
the Objectivist Axioms because the entire program structure/knowledgebase
structure/run time system is built upon the foundation of the Objectivist Axioms.

The user of this program/language/knowledgebase can add propositions
to the knowledgebase which can be false.  There are some built-in
consistency checks to prevent this.  You can write your own mKR scripts
to provide additional checks.

And, perhaps unwisely, I have given the user the power to delete the
Objectivist Axioms, and replace them with his own propositions.
In that case, the mKR language remains the same, but the integration
with the Objectivist Axioms is lost.

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

---

Date: Thu, 3 Apr 2014 09:05:50 -0400
From: whitten@xxxxxxxxxx
To: rhm@xxxxxxxxxxxxx; ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] mKR proof of correctness

So to re-iterate (as I understand it):

Richard has a syntax that he claims to provide enough information to allow a program to have enough

information that it can state propositions. Pat and John have asked Richard to show that after collecting

these propositions together, that there is a step-by-step method to relate those propositions to other

propositions (which are not stated by Richard). 

There is a constraint on the step-by-step method such that from the original propositions, you cannot

relate them to new propositions that would violate the operations of some standard form of logic.

There is also a requirement that every proposition that the standard forms of logic expect to be related

to an initial set of propositions will actually be related together by Richard's method.

I have tried to not use any words like "inference" or "interpretation of model" or "semantics" or "syntax"

here.  Have I left anything out that would be necessary for Richard ?

David

713-870-3834713-870-3834

 

On Thu, Apr 3, 2014 at 7:04 AM, Richard H. McCullough <rhmccullough@xxxxxxxxx> wrote:

Well -- I knew my age would betray me eventually.
I grew up in the era when the terms were
          syntax
          semantics
and semantics was concerned with the meaning of words.
Today, I think the popular terms  are
         syntax
         semantics
         pragmatics
and semantics is concerned with transformations of propositions
and pragmatics is concerned with the meaning of words.

So I am more focused on pragmatics, and haven't thought that much
about semantics.

But old habits are hard to break, and I keep saying semantics
when I shouldn't.  I apologize for the confusion.
 
My errors in terminology do not alter the validity of the
Objectivist Axioms, or their usefulness.  I will say more about
that later -- in response to another question which was raised
here in the Ontolog Forum.

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

---

Date: Wed, 2 Apr 2014 23:26:21 -0700
From: steven@xxxxxxx
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] mKR proof of correctness

Dear Pat,

Semantics generally say nothing about the world. They are the valid rules of syntax transformation (per Carnap).

McCullough's axioms make little sense to me. Indeed, they do not appear, in fact, to be axioms.  

Regards,

Steven

On Wed, Apr 2, 2014 at 8:21 PM, Pat Hayes <phayes@xxxxxxx> wrote:

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 language 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 home
40 South Alcaniz St.            (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (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

_________________________________________________________________ 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

_________________________________________________________________
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
 

_________________________________________________________________ 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

Call

Send SMS

Add to Skype

You'll need Skype CreditFree via Skype

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