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


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.


Now on to your complaint about my creating noise and clutter in my THY.

Working on trying to better reduce noise and clutter is half of what I got out of sending off this email. The other half is learning about the usefulness of locales to do some preliminary proofs without globally injecting all the overhead into the THY.

Back to noise and clutter, the challenge is to find a way to mark up THYs in a way that is reasonably readable, and which can also be processed with scripts to generate other THY and TEX files to give people options on how they want to absorb the information.

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:

I'm trying to duplicate a decent imitation of the newtheorem environment in the THY file, without creating too much clutter and noise, and not fall prey to the "gaudy web page syndrome".

It's not obvious how to use a limited set of tools to get something better than the traditional way of doing things.

Sometimes you don't get something better. There was Xerox. And there was Apple. It's the story of Apple taking new ideas and refining the new ideas in significant ways, and doing it with hardware limitations.

I attach my newest attempt to edit my THY so that I can convert my cheap newtheorem imitations into the real thing with a script, among other processing. The source code of a marked up language isn't meant for public consumption, but if the public can consume the source code, that's a good thing, because then it means you can probably read your own source code.

Christian, thanks for the help.


On 10/27/2012 9:30 AM, Christian Sternagel wrote:
Dear Gottfried,

first of all, the way you are using symbols in comments is rather non-conventional and makes the THY file a bit cluttered with unnecessary noise. Since typical Isabelle users might prefer to consult the THY file over the generated PDF file that is unfortunate.

Concerning the counterexample: The theorem for which nitpick found a counterexample does not state equivalence of the two formulas.

To see why, you have to know how Isabelle treats free variables: they are implicitly all-quantified (using the all-quantifier of Pure, which is !!). 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 second one is


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, this formula does not state equivalence between your two axioms (since the quantifiers are at the "wrong" place).

Now for your locales. Since for any Q, "!x. Q x" is logically equivalent to "!!x. Q x" (in HOL) the locales are equivalent (and thus more 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 the only axiom of the local is already what we have to prove.

In short: both axioms are indeed equivalent and the counterexample does not apply since it was generated for a different statement.

Take away: free variables in theorems are implicitly all-quantified.

hope that helps


On 10/27/2012 05:08 PM, Gottfried Barrow wrote:

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.


theory a_sTs01_121027 imports Complex_Main begin

  rhsimplhs :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixr "<--" 25)
               where "(x <-- y) == (y \<longrightarrow> x)"
  notation rhsimplhs                  (infixl "\<longleftarrow>" 25)

section{*The Axiom of Extension*}

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)
    inS                         (infixl "\<in>\<^isub>\<iota>"  55)
    niS :: "\<sigma>\<^isub>\<iota> \<Rightarrow> \<sigma>\<^isub>\<iota> \<Rightarrow> bool"    (infixl "niS" 55) where "x niS y == \<not>(x \<in>\<^isub>\<iota> y)"
    niS                         (infixl "\<notin>\<^isub>\<iota>"  55)

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>)"
  "(\<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."

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

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>)"
  "(\<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>)"
  "( \<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)) )
   (        (\<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>)"
  "( \<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)) )
   (        (\<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 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."

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

section{*Are free variables implicitly quantified?*}

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>)"
  "(!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>)"
  "(P q\<^isub>1) \<longrightarrow> (!q. P q)"
--"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>"

--"\<^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>)"
  "(!q. P q) \<longleftrightarrow> (P q\<^isub>1)"

--"\<^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>)"
  "(!q. True) \<longleftrightarrow> True" 
  by simp
  "!q. (!q. P q) \<longrightarrow> (P q)" 
  by simp  
  "!q. (P q) \<longrightarrow> (!q. P q)" 


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.