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


You say, "I wrote too much in my last email and thereby missed to convey my main point".

I've understood the point all along about implicit quantification, which Larry called "universal closure", and I knew that if that it was true, that I couldn't explicitly state certain formulas like I was trying to do. But you're the first one who explicitly told me that "!!" is where the quantification is occurring.

It is true that I forgot about the implicit quantification... Actually, it's becoming too much work to remember what it is I understood or didn't understand, or forgot once I went off on a tangent by treating things as unquantified propositions.

Fortunately, you thought I missed your point and went the extra step of giving me enough details to take everything from the abstract to the concrete.

You showed things several ways, but this is a very straightforward demonstration of the quantification that's occurring:

   lemma Conjecture1: "(ALL x::'a. P x) <-> P x" sorry
   lemma Conjecture1': "!! x. (ALL x::'a. P x) <-> P x" sorry

It seems to me that the documentation should point this out. A person can say that standard logic principles cover this, but it doesn't, because Isabelle/HOL is not standard logic.

Magical software is mysterious. Unless told otherwise (and substantiated), a person might be assuming the truth of "(ALL x::'a. P x) <-> P x" is being determined with a huge truth table retrieved from Google, which would allow the formula to be used in other formulas without quantification being forced on it like it is now.

This implicit quantification is all tied into schematic variables, so it appears it's not an easy subject to broach:

At the top is where Lars told me about the implicit quantification, and then Makarius says:

  But when you state lemma "!!x y. A x ==>  B y" your result is schematic "A ?x ==>  B ?y".

Your proof, using "==", shows you (probably) have to resort to meta-logic to be able to prove the equivalency without first assuming either Axiom1 or Axiom2.

Will I do that? No. For my current application, I'll stay away from the explicit use of meta-logic, if I can. Why? I don't explain that. All that would do is make this email longer.

Christian, thanks for the proof and documenting what's going on.


On 10/28/2012 11:38 PM, Christian Sternagel wrote:
Dear Gottfried,

I wrote too much in my last email and thereby missed to convey my main point. Consider the following:

  definition P :: "'a => bool" where
    "P x == undefined" -- "the exact definition of P doesn't matter"

  axiomatization where
    Axiom2: "P x" and
    Axiom2': "!!x::'a. P x"
thm Axiom2 Axiom2' -- "this shows that for Isabelle both axioms are the same"

I.e., the resulting theorem that is stored in the theorem database of Isabelle is exactly the same for Axiom2 and Axiom2', i.e., "P ?x" (where a schematic variable, the one with the question mark in front, is used to represent all-quantification, in the sense that we may substitute any term having the correct type for ?x).

By that reasoning, your Axiom2 is the same as my Axiom2'. Then in order to get a correct counterexample you would have to disprove

  -- "here is a proof that your Axiom1 is equivalent to your Axiom2"
  lemma Conjecture: "Trueprop (ALL x::'a. P x) == (!!x::'a. P x)"
    fix x::'a assume "ALL x::'a. P x" then show "P x" ..
    assume "!!x::'a. P x" then show "ALL x::'a. P x" ..
  thm Conjecture

But that is not possible, since it is a theorem. Moreover consider

  lemma Conjecture1: "(ALL x::'a. P x) <-> P x" sorry
  lemma Conjecture1': "!! x. (ALL x::'a. P x) <-> P x" sorry
  thm Conjecture1 Conjecture1'

which are two equivalent statements of your Conjecture1. This states something different from my Conjecture (just have a look at the result of the thm command).

So, everything else I said aside, your counterexample does not show what you think it does. That's my main point. Also you do not have to look into any ML code, just observe the results of the thm command ;)



On 10/28/2012 05:46 PM, Gottfried Barrow wrote:

I'm now ready to remain skeptical even though I'm safely assuming that
you're right when you say that free variables are quantified with the
"!!" operator. And somehow, my skepticism here is not the same thing as
cognitive dissonance.

If you can tell me the ML file (or ML file folder) where "!!" is used to
quantify the free variables, that would definitively put all this to
rest, I think.

So, you would be at least the third person who has told me that free
variables are implicitly quantified. I'm happy to take lessons in basic
logic, but I think part of what's been leading me astray here is that
with the examples I've been looking at, I logically get the same results
by assuming that free variables aren't implicitly quantified. At the
very least here, I could just switch all this to a question, "Do I get
the same results if I assume free variables aren't quantified?" It might
be a trivial question, with a trivial result. I don't know.

Here, I give two lemmas, one conjecture, and two axioms, which I think
are representative of what I'm doing in my THY, and which ties into your

Lemma1: (!q. P q) --> (P q)
Lemma2: (P q) --> (!q. P q)

Conjecture1: (!q. P q) <-> (P q)

Axiom1: (!q. P q)
Axiom2: (P q)

Essentially, I can get similar results as you describe below without
assuming that free variables get quantified by "!!".

Prior to Axiom1 and Axiom2 being given, Lemma1 is trivially true, and
Lemma2 is obviously false, so Conjecture 1 is obviously false.

(In this case, if I explicitly quantify Lemma1 and Lemma2 using (!q.
(!q. P q) --> (P q)) and (!q. (P q) --> (!q. P q)), I get the same
results, so it doesn't tell me I'm misguided.)

This result would be similar to my counterexample in my THY. I didn't
actually substitute the values that Nitpick gave me into my formula. If
I did the brainwork, it might show me that it would have to be the case
that "!!" is quantifying the free variables.

Assume Axiom1. Lemma1 doesn't need Axiom1 to be true. For Lemma2,
because of Axiom1, the right-hand side of Lemma2 is always true, thus
Lemma2 is true. This result represents the result of using my first locale.

Assume Axiom2. Again, Lemma1 doesn't need it. For Lemma2, we would have
the equivalent formula (True --> (!q. True)), which is true. This result
represents my result of using my second locale.

Okay, I could be saying the most stupidest of things here. Once I miss
formally learning certain basics, it's hard to find time to go back and
learn what I don't have to know.

It makes sense that free variables would be quantified by the software.
On the other hand, when no one will point me to a formal document
telling me that, I keep open the option that something different could
be going on. "Makes sense" doesn't serve me well sometimes.

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