From: Graham Klyne <GK@ninebynine.org>

Date: Tue, 22 May 2001 14:11:58 +0100

Message-Id: <5.0.2.1.2.20010522135548.03743cf0@joy.songbird.com>

To: RDF core WG <w3c-rdfcore-wg@w3.org>

Date: Tue, 22 May 2001 14:11:58 +0100

Message-Id: <5.0.2.1.2.20010522135548.03743cf0@joy.songbird.com>

To: RDF core WG <w3c-rdfcore-wg@w3.org>

[[[My attempt to explain model theory. This message is sent to accompany another message which makes reference to "semantics". Many logicians equate semantics with a model theory: interpreting statements in some domain of discourse so that they are determined to be true or false. Withou semantics there is no truth or falsity. For folks who already understand this, please: (a) skip this message, or (b) tell me if/where I've got it wrong - #g]]] For someone coming from a programming/system implementation background, I think it is important to ditch, or at least suspend, any view of semantics as defined by or related to some algorithm or process. The model theoretic approach is almost exactly the opposite of this: it is concerned with what is considered to be true or false without regard for how such truth is obtained or processed. (The associated proof theory deals with how such truths may be deduced.) Model theory inherits from the *mathematical* view of a function: a function is defined mathematically as a set of pairs drawn from some range and domain -- without reference to the computational process that might be used to find a member in its range corresponding to some member in its domain. For example, the successor function on positive integers would be: { <0,1>, <1,2>, <2,3>, ... etc } Or a function sometimes known as integer addition: { <<0,0>,0>, <<0,1>,1>, ... <<1,0>,1>, <<1,1>,2>, ... etc } If two different mechanisms happen to relate the same domain values to the same range values, they compute the exact same mathematical function. In similar fashion, semantics concerns itself with sets of values drawn from a domain of discourse that are considered to be true for some interpretation of a function. Again, this truth is without reference to any mechanism... it just is. As computer programers, we have been taught to view most of what we do as constructing a process. It was a long time ago, but I recall some vague cognitive dissonnance when first faced with the idea of, say: X = X+1 The whole learning of programming was a training in how to construct processes that compute some desired result. In dealing with semantics, we need to suspend all that ingrained training: we want to match statements in some language (symbols+grammar) to ideas that are held to be true in some domain of discourse (without regard for how those truths might be discovered). Model theory does this. Of course, without a means of computation this would be of limited value. This is where the other part of logic (specifically, for our purposes, first order logic) comes in to play: deductive apparatus, or proof systems. Unlike model theory semantics, this provides us with a framework for using axioms and rules of inference to deduce new statements (theorems). The sequence of steps thus followed constitutes a "proof". The really clever bit in all this is the work that has been done, much of it over the past 100 years or so, that establishes that for certain classes of logic system, model theoretic truths and deducible theorems coincide (consistency,completeness). One particularly important such system is First Order Logic (FOL). So what we have is this: Language / \ / \ Model Proof theory theory | | true deducible statements statements and we are interested in whether or not the true statements are the same set as the deducible statements. For example, we have the following truths (under the intended interpretation of common arithmetic and decimal notation): 2+2=4 1234+4321=2222+3333 1000+1=1001 and these are truths (in this interpretation) regardless of any process that may be used to compute the sum of two numbers (or to compare the results). Of course, in practice, we seek algorithms that preserve these truths, or for which we know the exact conditions under which the truths are preserved. In summary: (Model theoretic) semantics is about binding statements in some language to truths in some domain of discourse. Just that. Proof theory, when properly aligned with the semantics, allows us to generate statements which are truths under some interpretation, or class of interpretations. #g ------------ Graham Klyne GK@NineByNine.orgReceived on Tuesday, 22 May 2001 10:24:05 EDT

*
This archive was generated by hypermail pre-2.1.9
: Wednesday, 3 September 2003 09:35:50 EDT
*