Il y a un rapport entre l'utilisation des variables en logique et en programmation.
En particulier les notions d'occurrences 'libres' et 'liées' existent dans les deux domaines.
Dans un énoncé une même variable peut apparaître plusieurs fois (en plusieurs endroits différents), on parle alors "d'occurences".
Le qualificatif 'lié' ou son contraire 'libre' s'applique à une occurrence ET à un contexte (un énoncé dans lequel la variable apparaît).
Prenons ainsi l'énoncé:
∀x aime(x,y)
Signifiant à peu près : "Tout le monde aime y".
On remarque deux choses dans un tel énoncé:
Dans un tel énoncé on dit que l'occurrence de x est liée et que l'occurrence de y est libre .

Plus généralement, dans un énoncé quantifié du genre :
∀x E(x)
où x désigne une variable et E(x) un énoncé contenant la variable x. E(x) s'appelle le 'corps' de l'énoncé (anglais: body) , un peu comme le corps d'une fonction qui exprime sa définition dans un langage de programmation procédural..
Ainsi relativement  à tout énoncé quantifié du type ∀ x E(x), toute occurrence de x dans E(x) est liée, et par définition une occurrence qui n'est pas liée est dite libre.
Ainsi dans l'énoncé:
aime(x,y) (l'individu x aime l'individu y)
x et y sont des occurrences libres
dans l'énoncé :
∀x aime(x,y) (tout le monde aime y)
x est lié et y est libre
dans l'énoncé:
∀y∀x aime(x,y) (tout le monde aime tout le monde)
x et y sont liés.

A l'intérieur d'une même formule, différentes occurrences d'une même variable peuvent être libres ou liées.
Voici un exemple:
R(x)∧∃x (¬R(x))
Cette formule signifie que x possède la propriété R mais que cette propriété n'est pas vérifiée par tous les éléments.
De fait, il y a deux variables sous-jacentes mais il advient qu'elles ont reçu le même nom. D'après la portée on doit savoir de laquelle il s'agit. En informatique nous dirions que la variable locale 'éclipse' la variable globale. Vu de cette manière on peut dire que les variables libres des énoncés correspondent aux variables globales en programmation.
Compte tenu de ce que nous avons dit, la formule ci-dessus est tout à fait équivalente à:
R(x)∧∃y (¬R(y))
qui apparaît comme plus claire.
Quel que soit le nombre des variables impliquées il est toujours possible de renommer pour parvenir à des formules où ne subsiste aucun télescopage.

Café Python

Programme exemple sur la portée des variables.

Quelques règles simples à retenir donc:

Si, depuis une fonction on veut accéder à une variable globale:

En outre, dans tous les cas:

Le respect de ces trois règles doit vous garantir l'absence de téléscopage. On force les programmeurs travaillant en équipe sur de vastes projets à utiliser des 'espaces de noms' pour les modules qu'ils rédigent. Ainsi la variable x du programmeur lambda sera reconnue comme lambda::x ou bien lambda.x au montage.