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

On Fri, 4 Jan 2013, Alfio Martini wrote:

`However, it was a kind of provocative attempt to bring the topic again.
``The answers were all there, spread through a number of different posts
``(and flames). Maybe I secretly wanted to begin this new year with a nice
``summary of that discussion.
`

`This thread is again in danger of getting long, so here are just some
``quick jokes from the Isabelle repertoire:
`
* Free variables are "fixed" (in a local context).
This terminology is stemming from Mizar and used in Isar as well, but
is actually an oxymoron. Such variables are not variable at all.
* Schematic variables are "arbitrary" (after having left the context).
This is a useful formal device to make the variability of variables
formally clear.

`So a properly fixed local variable acts like a local context that becomes
``arbitrary after leaving it. In Isar this reads like this:
`
{
fix x :: 'a
have "B x" sorry
}
note `B a`
note `B b`
note `B c`

`In fact we can make this arbitrariness stronger within the logical
``framework:
`
{
fix x :: 'a
have "B x" sorry
}
note `⋀x. B x`

`Here it now looks as if the system would insert that postulated implicit
``quantifier, but it is actually not there, and bypassed in the internal
``reasoning. These are just two ways to specify the same result: inspecting
``the machine state in the Output window, you will see schematic variables,
``not quantifiers.
`

`Next joke: What about a free variable that is not properly "fixed"?
``Answer: it is an illegal immigrant into the logical context, without legal
``papers. Practically it acts like an unspecified global constant, and can
``usually not be used productively in a proof.
`

`This is the reason why Isar merely prints undeclared free variables with
``certain markup, but does not reject them: they are useful in
``pseudo-proofs, i.e. proof patterns like above. The variables B, a, b, c
``are all been illegal immigrants, without anybody getting confused.
`

`Here is one of the rare proofs where a totally undeclared formal entity
``can be used in a productively:
`
theorem Drinker's_Principle: "∃x. drunk x ⟶ (∀x. drunk x)"
proof cases
assume "∀x. drunk x"
then have "drunk alien ⟶ (∀x. drunk x)" ..
then show ?thesis ..
next
assume "¬ (∀x. drunk x)"
then obtain a where a: "¬ drunk a" by blast
have "drunk a ⟶ (∀x. drunk x)"
proof
assume "drunk a"
with a show "∀x. drunk x" by contradiction
qed
then show ?thesis ..
qed

`The alien does not need formal declaration at the custom's office, but I
``usually prefer to put a 'fix' in the proper spot nonetheless.
`
Makarius

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