ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] mKR proof of correctness

To: Steven Ericsson-Zenith <steven@xxxxxxx>
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Pat Hayes <phayes@xxxxxxx>
Date: Thu, 3 Apr 2014 22:11:41 -0500
Message-id: <EAA04712-F3FC-486D-A5D2-DF37F00C2B25@xxxxxxx>

On Apr 3, 2014, at 1:26 AM, Steven Ericsson-Zenith <steven@xxxxxxx> wrote:    (01)

> Dear Pat,
> 
> Semantics generally say nothing about the world. They are the valid rules of 
>syntax transformation (per Carnap).    (02)

I take semantics here to be a model theory. This is the exact description of 
how the truthvalues of sentences are determined by the denotations of the names 
in those sentences, per Tarski. Put another way: the description of how the 
referents of larger expressions are determined by those of smaller expressions, 
using recursion on the grammar of the language. And the referents are things in 
the (more exactly, in *a*) world. The semantics cannot even be begun without 
some account of the structure of these worlds: for Tarski, a relational 
algebra; for Kripke, add a modal alternativeness relation, etc..     (03)

Valid syntax transformations are proof theory, but the very idea of 'valid' is 
only meaningful when there is a model-theoretic semantics to determine validity 
(=df. preservation of truth in all possible interpretations.)     (04)

Pat    (05)

> 
> 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    (06)

------------------------------------------------------------
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    (07)







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

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