*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 29 Oct 2012 11:15:35 -0500*In-reply-to*: <508E0855.9080006@jaist.ac.jp>*References*: <508B968B.4070709@gmx.com> <508BEFEC.907@jaist.ac.jp> <508CF0DC.8030301@gmx.com> <508E0855.9080006@jaist.ac.jp>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Christian,

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

http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/5396

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

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 mainpoint. 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 arethe same"I.e., the resulting theorem that is stored in the theorem database ofIsabelle 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 maysubstitute any term having the correct type for ?x).By that reasoning, your Axiom2 is the same as my Axiom2'. Then inorder 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 statessomething different from my Conjecture (just have a look at the resultof the thm command).So, everything else I said aside, your counterexample does not showwhat you think it does. That's my main point. Also you do not have tolook 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 firstlocale.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.

**References**:**[isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized***From:*Gottfried Barrow

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

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

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

- Previous by Date: Re: [isabelle] isabelle mailing lists
- Next by Date: Re: [isabelle] bdd formalization
- Previous by Thread: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Next by Thread: Re: [isabelle] Free variable dead horse beat; getting two equiv formulas after either one is axiomatized
- Cl-isabelle-users October 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list