What 'model' means in the formal systems literature
  (for details, see http://www.w3.org/XML/9711theory/
   esp http://www.w3.org/XML/9711theory/FormalSystem)

term ::= constantI
       | variable
       | constantF(term, term, ...)

atom ::= constantP(term, term, ...)

formula ::= atom
        |   forumula AND formula
        |   formula  OR formula
        |   NOT fomula
        |   FORALL(variable) formula
        |   THEREEXISTS(variable) formula



An _interpretation_ is
  -- a set of _objects_, often called the domain, D
  -- a mapping of constantI's to D
  -- a mapping of constantF's to (DxDxDx...)->D i.e. functions over D
  -- a mapping of constantP's to DxDxDxDx... i.e. relations over D

e.g.
     D = { objDan, objTim, objUs }
     constantI(Dan) = objDan
     constantI(Tim) = objTim
     constantI(Us) = objUs, i.e. ... the set of folks in the room...
     constantP(in) =  {<objDan,objUs>, <objTim, objUs>}

   so... in(Dan, Us) is interpreted as true.

a formula is satisfyable if there are _objects_ from D
 that (to paraphrase) can be plugged into the formula in the
 right places to make it work out.

and interpretation is a _model_ for a set of formulas
  if each of the formulas is satisfyable in that interpretation.

folks specify logics by specifying what constitutes a model;
i.e. which formulas should be regarded as true.

$Log: formalSys.txt,v $
Revision 1.2  2001/04/09 16:34:49  connolly
fixed a few typos and
refined the 'see also' link