Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
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
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