ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Role of definitions (Remember the poor human)

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 13 Feb 2007 13:12:21 -0600
Message-id: <0CC687C5-439D-4FDD-9C26-A65F20768037@xxxxxxxx>
On Feb 13, 2007, at 11:54 AM, Adrian Walker wrote:
> Hi Chris --
>
> [Adrian]
> >   * Semantics2   Specifies what inferences should be made from
> > any collection of rules and facts -- usually based on a model
> > theory, e.g. as in [3].
>
> [Chris]
> That's what is usually called *proof theory* in logic.  As you note,
> a proof theory is indeed typically *based on* a model theory, but the
> whole point of soundness and completeness theorems in logic is
> precisely to prove that the inferences that can be made from a
> collection of assumptions ("facts") according to a proof theory
> ("rules" (roughly)) are in fact sanctioned by the model theory
> (a.k.a., the formal semantics) given for the language of the proof
> theory.  It seems to me to be very unwise (and certainly not in
> keeping with standard terminology in mathematical logic) to call
> proof theory a sort of semantics
>
> [Adrian]  I think if you read the following again
>
> >   * Semantics2   Specifies what an inferences should be made from
> > any collection of rules and facts -- usually based on a model
> > theory, e.g. as in [3].
>
> (and if you have time to look at the paper), you'll see that we are  
> in complete agreement.    (01)

Great!  That "usually" there is what threw me -- if we are to be in  
complete agreement, then "usually" has to be replaced with "always".   
And there is still a (fairly large) nit to pick:  Even after changing  
"usually" to "always", I think it is potentially confusing, and at  
the least out of keeping with standard usage in logic, to call  
anything proof theoretic "semantics".  I would therefore propose  
revising Semantics2 to something like    (02)

   Specifies a model theory for some class of formal languages
   that serves as the basis for a proof theory that determines
   what inferences can be made in those languages from any
   given collection of assumptions    (03)

or the like.    (04)

> The essential point is to have a model theory as a gold standard to  
> which programmers must adhere when implementing an engine.    (05)

We are definitely in agreement there!    (06)

-chris    (07)



_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: 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 Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (08)

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