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



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

Attachment: a_sTs01_121027.pdf
Description: Adobe PDF document

theory a_sTs01_121027 imports Complex_Main begin

--"\<^bold>\<Sqinter>"section{*The Axiom of Extension*}

--"\<^bold>\<Prod>"subsection{*The primitive set type and membership predicate*}

--"\<^bold>\<T>\<^bold>\<Y>\<^bold>\<P>\<^bold>\<E>" typedecl--"The primitive set type \<sigma>\<^isub>\<iota>: everything is a set."
  sT ("\<sigma>\<^isub>\<iota>")

--"\<^bold>\<P>\<^bold>\<R>\<^bold>\<E>\<^bold>\<D>" consts--"Membership predicate \<in>\<^isub>\<iota>: axiomatized by subsequent axioms."
  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>\<Prod>"subsection{*Axiomatizing two forms of the Axiom of Extension*}

--"\<^isub>'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 proposition

      (\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2).

At this point, the following counterexample shows that it is not."

--"\<^bold>\<C>\<^bold>\<N>\<^bold>\<T>\<^bold>\<X>" theorem--"The two forms are not equivalent."
  "(\<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[user_axioms]"
--"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

--"\<^isub>'However, 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>\<L>" locale standard\<^isub>'axiom\<^isub>'of\<^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>\<R>\<^bold>\<M>" theorem (in standard\<^isub>'axiom\<^isub>'of\<^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)

--"\<^isub>'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 Axiom of Extension."

--"\<^bold>\<L>\<^bold>\<O>\<^bold>\<C>\<^bold>\<L>" locale free\<^isub>'variable\<^isub>'axiom\<^isub>'of\<^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>\<R>\<^bold>\<M>" theorem (in free\<^isub>'variable\<^isub>'axiom\<^isub>'of\<^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)

--"\<^isub>'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>\<M>" axiomatization--"The Axiom of Extension: set equality." 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)"


end


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