Christian,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" sorryIt 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:
http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/5396At 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. Regards, GB 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)" proof fix x::'a assume "ALL x::'a. P x" then show "P x" .. next assume "!!x::'a. P x" then show "ALL x::'a. P x" .. qed 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 ;)cheers chris On 10/28/2012 05:46 PM, Gottfried Barrow wrote:Christian, 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 reply. 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, thusLemma2 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.