Model theory for programmers?

[[[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.org

Received on Tuesday, 22 May 2001 10:24:05 UTC