[FOM] Question about "fresh" variables/objects in logics

[A. Mani]

On Friday 25 November 2005 21:01, Divianszky Peter wrote:
> Does anybody know of a formal description of the concept of "fresh"
> variable/object in logic?
>
> This concept is used in theoretical computer science quite often, but I
> have never seen a formal description of it.
> Informally it could be descibed as:
>
> Let X be an infinite set.
> The definition
>    x in X is fresh
> means that
>    x is an element of X
>   and
>    for all y in X defined elsewhere: x not equal y
This is a  fresh composition.
All that means there are translations of partial interpretations (in the 
algebraic sense).

Fresh(x, X) iff (\forall {y}\in X)(\forall{v}\inV)(v(y)=z --->y\neq x)

V is a set of partial monic functions defined by your context  :X --> Z,
You can use the multisorted version.
On X you need a concept of notequality only.
v(y)=z means v(y) is defined.
 
Now unless you make a few relaxations, your 'fresh' will remain that way.
 
> The formal description of this concept would help me a lot. I am doing
> research in functional programming and I could use it there.
>
AFAIK if you change types of values and manipulate them...it is unique to 
functional programming. It is "one-way" in formal logic...translations are  
developed in that direction. But  ...you can make the model differently.

A. Mani
Member, Cal. Math. Soc