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) = {, }
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