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