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