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

[Andrej Bauer]

Divianszky Peter wrote:
> Does anybody know of a formal description of the concept of "fresh"
> variable/object in logic?

You'd be better off asking computer scientists about this :-)

I believe you are looking for "nu calculus", which was (correct me if I
am wrong) proposed by A. Pitts and J. Gabbay. The paper I am aware of is

  A New Approach to Abstract Syntax Involving Binders (1999)
  Murdoch Gabbay, Andrew Pitts (LICS'99)
  http://citeseer.ist.psu.edu/gabbay99new.html

but there is probably an earlier one (it would be best to hear from
horse's mouth). They use permutation models of set theory to establish
their results. You may also look at the related work

  Marcelo Fiore, Gordon Plotkin and Daniele Turi
  Abstract Syntax and Variable Binding
  http://homepages.inf.ed.ac.uk/gdp/publications/Abstract_Syn.pdf

For games semantics of nu calculus, search for "nominal games" by
S. Abramsky, D. Ghica, A. Murawski, L. Ong and I. Stark.

Depending on what you want to do, Aleksandar Nanevski's Ph.D. thesis
"Functional Programming with Names and Necessity" may also be of
interest, see http://www.eecs.harvard.edu/~aleks/thesis/thesis.ps
(references [PG00] and [Pit01] therein refer to Pitt's and Gabbay's
other relevant work).

Andrej Bauer