🚀 go-pugleaf

In article <BtyBLw.42q@dcs.glasgow.ac.uk> areid@dcs.glasgow.ac.uk (Alastair
Reid) writes:
>I'm looking for a paper I skimmed a few months ago but failed to take
>a proper note of its location. I thought it was published in a recent
>volume of LNCS but checking likely candidates for the last five years
>failed to refind it.
>
>The paper suggested a slightly different definition of "valuations."
>
>  The usual definition of a valuation is something like:
>
>    A valuation v:X->A is a family of indexed functions v_s : X_s -> A_s
>    which assign a value from A_s (the set of values of sort s in an
>    algebra A) to variable symbols taken from X_s.
>
>  If A_s is empty, no value can be assigned to variables from X_s and
>  (assuming X_s to be non-empty), no valuation exists.
>
>  From memory, the definition in the paper differed as follows:
>
>    Instead of requiring that v_s(x) (the value assigned to a variable
>    x of sort s by a valuation v : X -> A) must always be defined, the
>    paper required that:
>
>      v_s(x) is undefined,  if A_s is empty; and
>      v_s(x) \in A_s,       if A_s is non-empty.
>
>  This second definition ensures that valuations v : X -> A exist even
>  if A does have empty carrier sets and avoids the need for a lot of
>  shenanigans in the definition of evaluation of a term, satisfaction
>  of a formula and observational equivalence wrt a set of free
>  variables.
>
>Any help in finding this paper would be greatly appreciated.
>

I don't know the particular paper either.

The constructivists have confronted the problem of empty carriers, and I
believe the solution suggested here would not satisfy them because of the way
the definition relies on knowing whether A_s is empty or not. (Remember that
constructively you don't have excluded middle. Also, there are questions of
whether "A non-empty" means that you can explicitly give an element of A, or
you can prove that one exists, or merely that it is impossible for A not to
have any elements.)

The problems associated with empty carriers are not essentially ones of
constructivity, but all the same the constructivist solution is worth knowing
about.

They drop the idea that a valuation should try to assign values to _all_
variables; after all, any particular axiom (equation or sequent) whose
satisfaction is being checked only uses finitely many. They explicitly label
each axiom with a finite set of variables, including all those free in the
axiom but possibly also some extra unused variables, and require that the axiom
should hold for every valuation _defined on that set_.

The trick comes in the way the proof rules handle these variable sets. You are
allowed to expand the set as much as you like, but you can't in general drop
variables from the set even if some logical reasoning has lost them from the
axiom - they are then considered unused but still present.

Here is an example that I got from Harry Simmons via John Tucker.

Consider a theory with two sorts, s and t, two constants a and b of sort t, and
a unary operator f: s -> t. Consider also two axioms

  a = f(x)
  f(x) = b

A simple application of transitivity gives a = b, but this is false in the
initial model M (which has empty carrier for s and a doubleton {a,b} for t).

With the labels, however, we must write

  f(x) =_{x} a
  f(x) =_{x} b

from which transitivity gives

  a =_{x} b

You can read this as "a = b in the presence of x". In the initial model it is
vacuously true that for every valuation on {x} (there are none) we have a = b.
Unrestricted equality between a and b would be a =_{} b, which - fortunately -
we can't deduce.

I wish I had a reference for this idea, but I'm afraid I've forgotten where I
saw it - perhaps someone can help me.

Steve Vickers.