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

[Steven Obua]

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.
>  
>
You might be interested in the work of Christian Urban. He is developing 
a system to reason about proofs in higher-order logic  that takes 
special  care of the treatment of fresh variables. This is  work  along 
the lines of the  "nominal  approach"  introduced by Andrew Pitts.

See http://www.mathematik.uni-muenchen.de/~urban/publications.html, for 
example "Nominal Reasoning Techniques in Isabelle/HOL".

Steven Obua