*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*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Mon, 29 Oct 2012 13:38:45 +0900*In-reply-to*: <508CF0DC.8030301@gmx.com>*References*: <508B968B.4070709@gmx.com> <508BEFEC.907@jaist.ac.jp> <508CF0DC.8030301@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121016 Thunderbird/16.0.1

Dear Gottfried,

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"

-- "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'

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, 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.

**Follow-Ups**:

**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

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