# Model theory for programmers?

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

(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

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 20:24:00 UTC