*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*: Sun, 28 Oct 2012 03:46:20 -0500*In-reply-to*: <508BEFEC.907@jaist.ac.jp>*References*: <508B968B.4070709@gmx.com> <508BEFEC.907@jaist.ac.jp>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Christian,

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)

*NOISE AND CLUTTER* Now on to your complaint about my creating noise and clutter in my THY.

For mathematical writing, I think there are four main components, 1) Section headings 2) Text/discussion 3) Statement of theorems, definitions, axioms, etc. 4) Proofs A big part of LaTeX is the newtheorem environment: ftp://ftp.ams.org/pub/tex/doc/amscls/amsthdoc.pdf

http://www.folklore.org/index.py

Christian, thanks for the help. Regards, GB On 10/27/2012 9:30 AM, Christian Sternagel wrote:

Dear Gottfried,first of all, the way you are using symbols in comments is rathernon-conventional and makes the THY file a bit cluttered withunnecessary noise. Since typical Isabelle users might prefer toconsult the THY file over the generated PDF file that is unfortunate.Concerning the counterexample: The theorem for which nitpick found acounterexample does not state equivalence of the two formulas.To see why, you have to know how Isabelle treats free variables: theyare implicitly all-quantified (using the all-quantifier of Pure, whichis !!). Let "P(q1,q2)" stand for the formula "(!x. x : q1 <-> x : q2)<-> (q1 = q2)", then your first axiomatization is!q1. !q2. P(q1,q2)which stays as it is, since there are no free variables. The secondone isP(q1,q2) and should be read as !!q1 q1. P(q1,q2) Now, if you write (!q1. !q2. P(q1, q2)) <-> P(q1,q2) the implicit Pure all-quantification is at the outermost position, i.e., !!q1 q2. (!q1. !q2. P(q1, q2)) <-> P(q1, q2)For this formula nitpick found a counterexample. The think is, thisformula does not state equivalence between your two axioms (since thequantifiers are at the "wrong" place).Now for your locales. Since for any Q, "!x. Q x" is logicallyequivalent to "!!x. Q x" (in HOL) the locales are equivalent (and thusmore or less identical for automated tools like blast, auto, metis).Moreover the proofs are both trivial. If we have "!q1 q2. P(q1, q2)"we can of course specialize this to arbitrary q1 and q2, i.e., "P(q1,q2)". The other direction of the biimplication, where we have "P(q1,q2)" for some arbitrary but fixed q1 and q2 and have to show "!q1 q2.P(q1, q2)" just does not have to use the assumption at all, since theonly axiom of the local is already what we have to prove.In short: both axioms are indeed equivalent and the counterexampledoes not apply since it was generated for a different statement.Take away: free variables in theorems are implicitly all-quantified. hope that helps chris On 10/27/2012 05:08 PM, Gottfried Barrow wrote:Hi, There may not be much to say about this. I'm looking for subtleties that I may not understand, about what the prover engine is doing with the free variables when I axiomatize a formula that contains free variables. I attach the THY and a PDF printout of the THY. The PDF is about 1 and a 1/2 pages long. I have two formulas: !q1.!q2.(!x. x ∈ q1 ⟷ x ∈q2) ⟷ (q1 = q2), and (!x. x ∈ q1 ⟷ x ∈q2) ⟷ (q1 = q2). First, I show they're not equivalent with a counter example. Using locales, I then show that if I axiomatize either one of them, then they're equivalent. I then axiomatize both of them, and I explain why with my last sentence. If anyone cares to comment, please do. Thanks, GB

theory a_sTs01_121027 imports Complex_Main begin abbreviation rhsimplhs :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixr "<--" 25) where "(x <-- y) == (y \<longrightarrow> x)" notation rhsimplhs (infixl "\<longleftarrow>" 25) --"\<^bold>\<Odot>" section{*The Axiom of Extension*} --"\<^bold>\<Oplus>" subsection{*The primitive set type and membership predicate*} --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>ZF sets is a first-order language which requires an infinite set of variables. Here I provide the HOL type for that infinite set of variables. I provide ASCII and non-ASCII notation for the type, which are sT and \<sigma>\<^isub>\<iota> respectively." --"\<^bold>T\<^bold>Y\<^bold>P\<^bold>E\<dots>\<^bold>(The primitive set type \<sigma>\<^isub>\<iota>: everything is a set.\<^bold>)" typedecl sT ("\<sigma>\<^isub>\<iota>") --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>ZF sets is specified to have one predicate, which is membership. The ASCII and non-ASCII notation for membership are inS and \<in>\<^isub>\<iota>, along with negation of membership, which is notated by niS and \<notin>\<^isub>\<iota>." --"\<^bold>P\<^bold>R\<^bold>E\<^bold>D\<^bold>I\<^bold>C\<^bold>A\<^bold>T\<^bold>E\<dots>\<^bold>(Membership predicate \<in>\<^isub>\<iota>: axiomatized by subsequent axioms.\<^bold>)" consts inS :: "\<sigma>\<^isub>\<iota> \<Rightarrow> \<sigma>\<^isub>\<iota> \<Rightarrow> bool" (infixl "inS" 55) notation inS (infixl "\<in>\<^isub>\<iota>" 55) abbreviation niS :: "\<sigma>\<^isub>\<iota> \<Rightarrow> \<sigma>\<^isub>\<iota> \<Rightarrow> bool" (infixl "niS" 55) where "x niS y == \<not>(x \<in>\<^isub>\<iota> y)" notation niS (infixl "\<notin>\<^isub>\<iota>" 55) --"\<^bold>\<Oplus>" subsection{*Axiomatizing the two forms of the Axiom of Extension*} --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>The standard Axiom of Extension is the formula \<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2). The question is whether this standard formula is equivalent to the free variable form (\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2). Naively, the following counterexample seems to indicate that, at least at this point, that they are not equivalent." --"\<^bold>C\<^bold>O\<^bold>U\<^bold>N\<^bold>T\<^bold>E\<^bold>R\<^bold>X\<dots>\<^bold>(A counterexample is found, but it does us no good.\<^bold>)" theorem "(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))" --"Nitpick found a counterexample for card \<sigma>\<^isub>\<iota> = 3: Free variables: (q\<^isub>3\<Colon>\<sigma>\<^isub>\<iota>) = s1 (q\<^isub>4\<Colon>\<sigma>\<^isub>\<iota>) = s2" oops --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>The problem is that because the prover engine implicitly quantifies all free variables in the statement of a theorem, the formula in the above counterexample is not the equivalence that we need to prove or disprove." --"\<^bold>\<Oplus>" subsection{*Moving universal quantifiers around*} --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>As stated above, free variables in any theorem are universally quantified by the prover engine. For example, if (P a) is our theorem, then we are proving (\<forall>a.P a). Because I want to use a free variable version of the Axiom of Extension, then I investigate how much freedom I have to move outermost, universal quantifiers around. This first example shows that we can sometimes move an outermost quantifier inside the original scope of the quantifier." --"\<^bold>E\<^bold>X\<^bold>A\<^bold>M\<^bold>P\<^bold>L\<^bold>E\<dots>\<^bold>(Sometimes a quantifier can be moved from outside to inside.\<^bold>)" theorem "(\<forall>b.((\<forall>a. P a) \<longrightarrow> P b)) \<longleftrightarrow> ((\<forall>a. P a) \<longrightarrow> (\<forall>b. P b))" by simp --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>With the next theorem and counterexample, for the standard and free variable forms of the Axiom of Extension, I make the implicit quantification explicit, and see what happens." --"\<^bold>T\<^bold>H\<^bold>E\<^bold>O\<^bold>R\<^bold>E\<^bold>M\<dots>\<^bold>(The conclusion is true, so the premise doesn't matter.\<^bold>)" theorem "( \<forall>q\<^isub>1 q\<^isub>2.(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> ( (\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) ) \<longrightarrow> ( (\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> (\<forall>q\<^isub>1 q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) )" by metis --"\<^bold>C\<^bold>O\<^bold>U\<^bold>N\<^bold>T\<^bold>E\<^bold>R\<^bold>X\<dots>\<^bold>(The premise is true, so it is dependent on the conclusion.\<^bold>)" theorem "( \<forall>q\<^isub>1 q\<^isub>2.(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> ( (\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) ) \<longleftarrow> ( (\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> (\<forall>q\<^isub>1 q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) )" --"nitpick[timeout=10000,verbose,user_axioms]" --"Nitpick found a counterexample for card \<sigma>\<^isub>\<iota> = 2: Skolem constants: (q\<^isub>1\<Colon>\<sigma>\<^isub>\<iota>) = s\<^bsub>1\<^esub> (q\<^isub>2\<Colon>\<sigma>\<^isub>\<iota>) = s\<^bsub>1\<^esub>" oops --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>Here, I could analyze the conclusion of the last theorem (the LHS of the implication) to figure out precisely why it must be false, but that would require me to continue thinking." --"\<^bold>\<Oplus>" subsection{*Showing that axiomatizing either results in their equivalence*} --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>The following locale and theorem show that if we axiomatize the standard formula of the Axiom of Extension, then the standard form and the free variable form are equivalent." --"\<^bold>L\<^bold>O\<^bold>C\<^bold>A\<^bold>L\<^bold>E\<dots>\<^bold>(Assumes the standard Axiom of Extension.\<^bold>)" locale standard\<^isub>'extension = assumes standard\<^isub>'axiom: "\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)" --"\<^bold>T\<^bold>H\<^bold>E\<^bold>O\<^bold>R\<^bold>E\<^bold>M\<dots>\<^bold>(Standard axiom gives the desired equivalence.\<^bold>)" theorem (in standard\<^isub>'extension) "(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))" by (metis standard\<^isub>'axiom) --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>Likewise, the following locale and theorem show that if we axiomatize the free variable form of the Axiom of Extension, then the free variable form is equivalent to the standard form of the Axiom of Extension." --"\<^bold>L\<^bold>O\<^bold>C\<^bold>A\<^bold>L\<^bold>E\<dots>\<^bold>(Assumes the free variable Axiom of Extension.\<^bold>)" locale free\<^isub>'variable\<^isub>'extension = assumes free\<^isub>'variable\<^isub>'axiom: "(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)" --"\<^bold>T\<^bold>H\<^bold>E\<^bold>O\<^bold>R\<^bold>E\<^bold>M\<dots>\<^bold>(Free variable axiom gives the desired equivalence.\<^bold>)" theorem (in free\<^isub>'variable\<^isub>'extension) "(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow> ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))" by (metis free\<^isub>'variable\<^isub>'axiom) --"\<^bold>T\<^bold>E\<^bold>X\<^bold>T\<dots>Because we can axiomatize either form, I axiomatize both. The Ax\<^isub>'x\<^isup>N\<^isup>u axiom will be used, whenever possible, for theorems with no free variables. The Ax\<^isub>'x\<^isup>N\<^isup>f axiom will be used for theorems which contain free variables. This allows the possibility of separating the axioms and theorems with free variables from the axioms and theorems which contain no free variables." --"\<^bold>A\<^bold>X\<^bold>I\<^bold>O\<^bold>M\<dots>\<^bold>(The Axiom of Extension: set equality.\<^bold>)" axiomatization where Ax\<^isub>'x\<^isup>N\<^isup>u: "\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)" and Ax\<^isub>'x\<^isup>N\<^isup>f: "(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)" --"\<^bold>\<Odot>" section{*Are free variables implicitly quantified?*} --"\<^bold>\<Oplus>" subsection{*A general, simple case*} --"\<^bold>L\<^bold>E\<^bold>M\<^bold>M\<^bold>A\<dots>\<^bold>(If it's true for every q, then it's true for fixed q\<^isub>1.\<^bold>)" lemma "(!q. P q) \<longrightarrow> (P q\<^isub>1)" by simp --"\<^bold>L\<^bold>E\<^bold>M\<^bold>M\<^bold>A\<dots>\<^bold>(But not vice-versa.\<^bold>)" theorem "(P q\<^isub>1) \<longrightarrow> (!q. P q)" --"nitpick[timeout=10000,verbose,user_axioms]" --"Nitpick found a counterexample for card 'a = 4: Free variables: (P\<Colon>('a \<Rightarrow> bool)) = ((\<lambda>(x\<Colon>'a). _)(a\<^bsub>1\<^esub> := False, a\<^bsub>2\<^esub> := False, a\<^bsub>3\<^esub> := False, a\<^bsub>4\<^esub> := True)) (q\<Colon>'a) = a\<^bsub>4\<^esub> Skolem constant: (q\<Colon>'a) = a\<^bsub>3\<^esub>" oops --"\<^bold>C\<^bold>O\<^bold>N\<^bold>J\<^bold>E\<^bold>C\<^bold>T\<^bold>U\<^bold>R\<^bold>E\<dots>\<^bold>(It won't work because the second lemma above fails.\<^bold>)" theorem "(!q. P q) \<longleftrightarrow> (P q\<^isub>1)" oops --"\<^bold>T\<^bold>H\<^bold>E\<^bold>O\<^bold>R\<^bold>E\<^bold>M\<dots>\<^bold>(However, with (P q\<^isub>1) as an axiom, it would be this.\<^bold>)" theorem "(!q. True) \<longleftrightarrow> True" by simp theorem "!q. (!q. P q) \<longrightarrow> (P q)" by simp theorem "!q. (P q) \<longrightarrow> (!q. P q)" --"nitpick[timeout=10000,verbose,user_axioms]" oops end

**Follow-Ups**:**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:*Christian Sternagel

**References**:

- Previous by Date: [isabelle] bdd formalization
- Next by Date: Re: [isabelle] mergesort
- Previous by Thread: [isabelle] Friendly THY [was, 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