🚀 go-pugleaf

In article <BtyBLw.42q@dcs.glasgow.ac.uk> areid@dcs.glasgow.ac.uk
(Alastair Reid) writes:

   [Problem: with the usual definition of valuation, there are no
   valuations if a carrier of a many-sorted algebra is empty]

This problem can be solved quite elegantly by requiring a valuation to
be defined on the free variables of a term or formula, rather than on
all variables.

In a recent paper (available by FTP, see below), I used the following
definitions:

   (The notation ``\dom f'' denotes the domain, ``\ran f'' the range
   of a function, ``FV(t)'' the set of freee variables of a term or
   formula.  By convention, S is the set of sorts of a signature
   \Sigma)

   Definition (assignment)

   Let a signature \Sigma and a \Sigma-algebra A be given.  An
   \em{assignment} into A is an S-sorted mapping a that satisfies 
   \ran a_s \subset A_s for all s \in S.  If X is an S-sorted set such
   that X_s \subset \dom a_s for all s \in S, we write ``a: X ~~> A''.
 
   Definition (evaluation of terms)

   Let \Sigma be a signature and let A be a \Sigma-algebra.  By
   induction on \Sigma-terms, we define for each term t an
   \df{evaluation function}

      t_A: { a: FV(t) ~~> A } --> A_s,   where s is the sort of t:

   (follows the usual definition)

   Definition (satisfaction of formulas)

   Let \Sigma be a signature and let M be a \Sigma-algebra.  The
   notation ``M \sat \phi[a]'' will mean that M \em{satisfies} the
   formula \phi under the assignment a: FV(\phi) ~~> M.  The
   satisfaction relation is defined inductively:

   (follows the usual definition)

This way, closed formulas get the right semantics, even if they
involve quantification over empty carriers.  I have not thought about
proof systems.  My feeling is that empty carriers should be accepted
as natural and not be shied away from.

The paper from which this is taken does not deal specifically with
empty carriers, but shows that first-order logic cannot specify
behavioural equivalence classes of algebras:

  ``Two Impossibility Theorems on Behaviour Specification of Abstract
  Data Types''

  (to appear in Acta Informatica)

  available by anonymous FTP from 
  flop.informatik.tu-muenchen.de (131.159.8.35)

        798  Aug 28 15:01  /pub/theory/schoett/README
      67393  Aug 21 11:35  /pub/theory/schoett/imposs.dvi.Z
     120179  Aug 21 11:39  /pub/theory/schoett/imposs.ps.Z


Oliver Schoett     Inst. f. Informatik (H2), Technische Univ. M"unchen
                   Postfach 20 24 20,     8000 M"unchen 2,     Germany
schoett@informatik.tu-muenchen.de    phone +49 89 2105-2399  fax -8207