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

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.