# Re: [isabelle] Happy New Year with Free/Bound Variables

```On Fri, 4 Jan 2013, Christian Sternagel wrote:

```
```lemma "P x"

```
where "P" is some formula with the free variable "x". In this context, a helpful answer is that free variables are implicitly universally quantified. A more cautious answer would be something like:
```
```
When writing a top-level lemma statement like 'lemma "P x"' Isabelle behaves as if the free variable "x" was universally quantified at the meta-level for almost all purposes ;)
```
I am not yet fully satisfied.

My preferred example is:

lemma "x = x"

```
When you write that in a context with undeclared x and (and its implicitly inferred most general type 'a with undeclared 'a), the system will implicitly augment the proof context by fix x :: 'a (and fix type 'a beforehand as well).
```
```
['a::TYPE, x::'a] is the so-called "Eigen-context" of the statement. There are two sides of this valuable coin:
```
(1) The proof context has its elements are fixed.

(2) The result (after export from the context) has makes them arbitrary.

```
The example above includes the situation for types as well, since it hints at the important principle of implicit polymorphism in the manner of Hindley-Milner. The type language does not even have quantifiers, so there is no danger of claiming that they are introduced and eliminated somewhere in the belly of the logic -- they are simply not there.
```
```
Nonetheless, there is a slight difference in free term variables and free type variables: terms need to be fixed explicitly if meant to be universal in the end, but types are fixed implicitly according to the possibilities of the syntactic context.
```

lemma "!!x :: 'a. x = x"

```
you will have to fix the element in the proof before getting to the same proof context as before:
```
proof -
fix x :: 'a
...
qed

This is called "formal noise" in Isar terminology.  Here is the well-known
explicit way to avoid it:

lemma
fixes x :: 'a
shows "x = x"
proof -
...
qed

```
So you build up a context with fixed x, then you state "x = x", in the end you get arbitrary "?x::?'a = ?x".
```

Makarius

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.