Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized

Dear Gottfried,

first of all, the way you are using symbols in comments is rather non-conventional and makes the THY file a bit cluttered with unnecessary noise. Since typical Isabelle users might prefer to consult the THY file over the generated PDF file that is unfortunate.

Concerning the counterexample: The theorem for which nitpick found a counterexample does not state equivalence of the two formulas.

To see why, you have to know how Isabelle treats free variables: they are implicitly all-quantified (using the all-quantifier of Pure, which is !!). Let "P(q1,q2)" stand for the formula "(!x. x : q1 <-> x : q2) <-> (q1 = q2)", then your first axiomatization is

  !q1. !q2. P(q1,q2)

which stays as it is, since there are no free variables. The second one is


and should be read as

  !!q1 q1. P(q1,q2)

Now, if you write

  (!q1. !q2. P(q1, q2)) <-> P(q1,q2)

the implicit Pure all-quantification is at the outermost position, i.e.,

  !!q1 q2. (!q1. !q2. P(q1, q2)) <-> P(q1, q2)

For this formula nitpick found a counterexample. The think is, this formula does not state equivalence between your two axioms (since the quantifiers are at the "wrong" place).

Now for your locales. Since for any Q, "!x. Q x" is logically equivalent to "!!x. Q x" (in HOL) the locales are equivalent (and thus more or less identical for automated tools like blast, auto, metis).

Moreover the proofs are both trivial. If we have "!q1 q2. P(q1, q2)" we can of course specialize this to arbitrary q1 and q2, i.e., "P(q1, q2)". The other direction of the biimplication, where we have "P(q1, q2)" for some arbitrary but fixed q1 and q2 and have to show "!q1 q2. P(q1, q2)" just does not have to use the assumption at all, since the only axiom of the local is already what we have to prove.

In short: both axioms are indeed equivalent and the counterexample does not apply since it was generated for a different statement.

Take away: free variables in theorems are implicitly all-quantified.

hope that helps


On 10/27/2012 05:08 PM, Gottfried Barrow wrote:

There may not be much to say about this. I'm looking for subtleties that
I may not understand, about what the prover engine is doing with the
free variables when I axiomatize a formula that contains free variables.

I attach the THY and a PDF printout of the THY. The PDF is about 1 and a
1/2 pages long.

I have two formulas:

!q1.!q2.(!x. x ∈ q1 ⟷ x ∈q2) ⟷ (q1 = q2), and
(!x. x ∈ q1 ⟷ x ∈q2) ⟷ (q1 = q2).

First, I show they're not equivalent with a counter example.

Using locales, I then show that if I axiomatize either one of them, then
they're equivalent.

I then axiomatize both of them, and I explain why with my last sentence.

If anyone cares to comment, please do.


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