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