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/ontologforum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (08)
