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.