Archive for October, 2007

Compact sets and the Axiom of Choice

October 19, 2007

The first iteration of the tool for extracting blog-postable view from Isabelle/ZF source is ready. The post below is the result of processing the Topology_ZF_1b.thy theory file, to be included on the next release of IsarMathLib. The tool just does a bunch of context-sensitive text substitutions. The next iteration will hopefully do something closer to real parsing of the Isar source.

theory Topology_ZF_1b imports Topology_ZF_1

begin

One of the facts demonstrated in every class on General Topology is that in a T_2 (Hausdorff) topological space compact sets are closed. Formalizing the proof of this fact gave me an interesting insight into the role of the Axiom of Choice (AC) in many informal proofs.
A typical informal proof of this fact goes like this: we want to show that the complement of K is open. To do this, choose an arbitrary point y\in K^c. Since X is T_2, for every point x\in K we can find an open set U_x such that y\notin \overline{U_x}. Obviously \{U_x\}_{x\in K} covers K, so select a finite subcollection that covers K, and so on. I had never realized that such reasoning requires the Axiom of Choice. Namely, suppose we have a lemma that states “In T_2 spaces, if x\neq y, then there is an open set U such that x\in U and y\notin \overline{U}” (like our lemma T2_cl_open_sep below). This only states that the set of such open sets U is not empty. To get the collection \{U_x \}_{x\in K} in this proof we have to select one such set among many for every x\in K and this is where we use the Axiom of Choice. Probably in 99/100 cases when an informal calculus proof states something like \forall \varepsilon \exists \delta_\varepsilon \cdots the proof uses AC. Most of the time the use of AC in such proofs can be avoided. This is also the case for the fact that in a T_2 space compact sets are closed.

Compact sets are closed - no need for AC

In this section we show that in a T_2 topological space compact sets are closed.

First we prove a lemma that in a T_2 space two points can be separated by the closure of an open set.


lemma (in topology0) T2_cl_open_sep:
  assumes A1: T \text{ is}\ T_2 \   and A2: x \in  \bigcup T  y \in  \bigcup T   x\neq y
  shows \exists U\in T.\ (x\in U \wedge  y \notin  \text{cl}(U))
proof -
  from A1 A2 have \exists U\in T.\ \exists V\in T.\ x\in U \wedge  y\in V \wedge  U\cap V=0
    using isT2_def
  then obtain U V where U\in T  V\in T  x\in U  y\in V  U\cap V=0
  then have U\in T \wedge  x\in U \wedge  y\in  V \wedge  \text{cl}(U) \cap  V = 0 using open_disj_cl_disj
  thus \exists U\in T.\ (x\in U \wedge  y \notin  \text{cl}(U))
qed

AC-free proof that in a Hausdorff space compact sets are closed. To understand the notation recall that in Isabelle/ZF Pow(A) is the powerset (the set of subsets) of A and Fin(A) is the set of finite subsets of A.


theorem (in topology0) in_t2_compact_is_cl:
  assumes A1: T \text{ is}\ T_2 \  and A2: K \text{ is compact in}\  T
  shows K \text{ is closed in}\  T
proof -
  let X = \bigcup T
  have \forall y \in  X - K.\ \exists U\in T.\ y\in U \wedge  U \subseteq X - K
  proof -
    { fix y assume A3: y \in  X  y\notin K
      have \exists U\in T.\ y\in U \wedge  U \subseteq X - K
      proof -
	let B = \bigcup x\in K.\ \{V\in T.\ x\in V \wedge  y \notin  \text{cl}(V)\}
	have I: B \in  \text{Pow}(T)  \text{Fin}(B) \subseteq \text{Pow}(B)
	  using Fin.dom_subset
	from A2 A3 have \forall x\in K.\ x \in  X \wedge  y \in  X \wedge  x\neq y
	  using IsCompact_def
	with A1 have \forall x\in K.\ \{V\in T.\ x\in V \wedge  y \notin  \text{cl}(V)\} \neq  0
	  using T2_cl_open_sep
	hence K \subseteq \bigcup B
	with A2 I have \exists N \in  \text{Fin}(B).\ K \subseteq \bigcup N using IsCompact_def
	then obtain N where D1: N \in  \text{Fin}(B)  K \subseteq \bigcup N
	with I have N \subseteq B
	hence II: \forall V\in N.\ V\in B
	let M = \{\text{cl}(V).\ V\in N\}
	let C = \{D \in  \text{Pow}(X).\ D \text{ is closed in}\  T\}
	from topSpaceAssum have
	  \forall V\in B.\ (\text{cl}(V) \text{ is closed in}\  T)
	  \forall V\in B.\ (\text{cl}(V) \in  \text{Pow}(X))
	  using IsATopology_def cl_is_closed IsClosed_def
	hence \forall V\in B.\ \text{cl}(V) \in  C
	moreover from D1 have N \in  \text{Fin}(B)
	ultimately have M \in  \text{Fin}(C) by (rule fin_image_fin)
	then have X - \bigcup M \in  T using Top_3_L6 IsClosed_def
	moreover from A3 II have y \in  X - \bigcup M
	moreover have X - \bigcup M \subseteq X - K
	proof -
	  from II have \bigcup N \subseteq \bigcup M using cl_contains_set
	  with D1 show X - \bigcup M \subseteq X - K
	qed
 	ultimately have \exists U.\ U\in T \wedge  y \in  U \wedge  U \subseteq X - K
	thus \exists U\in T.\ y\in U \wedge  U \subseteq X - K
      qed
     } thus \forall y \in  X - K.\ \exists U\in T.\ y\in U \wedge  U \subseteq X - K
  qed
  with A2 show K \text{ is closed in}\  T
    using open_neigh_open IsCompact_def IsClosed_def
qed


end

This blog post has been generated from IsarMathLib’s Topology_ZF_1b.thy theory file, see the relevant pages of the IsarMathLib proof document.

See also TiddlyWiki rendering of this post.

Tags:
Posted in Proofs | No Comments »

Groups and neutral elements

October 8, 2007

This is my first experiment in presenting formalized mathematics in a blog post. Ideally, such presentation should be generated by the theorem proving environment from machine-verified sources. Since the software for converting Isabelle theory files to WordPress postable HTML is not ready yet, the post below is a result of conversion done by hand.


theory Group_ZF_1 imports Group_ZF
begin

In a typical textbook a group is defined as a set G with an associative operation such that two conditions hold:

A: there is an element e\in G such that for all g\in G we have e\cdot g = g and g\cdot e =g. We call this element a “unit” or a “neutral element” of the group.

B: for every a\in G there exists a b\in G such that a\cdot b = e, where e is the element of G whose existence is guaranteed by A.

The validity of this definition is rather dubious to me, as condition A does not define any specific element e that can be referred to in condition B - it merely states that a set of such units is not empty. Of course it does work out in the end as we can prove that the set of units has exactly one element, but still the definition by itself is not valid. You just can’t reference a variable bound by a quantifier outside of the scope of that quantifier.

One way around this is to first use condition A to define the notion of a monoid, then prove the uniqueness of e and then use the condition B to define groups.

Another way is to write conditions A and B together as follows:

\exists_{e \in G} (\forall_{g \in G} e\cdot g = g \wedge g\cdot e = g) \wedge (\forall_{a\in G}\exists_{b\in G} a\cdot b = e).

This is rather ugly.

The third way that I want to talk about is an amusing way to define groups directly without any reference to the neutral elements. Namely, we can define a group as a non-empty set G with an associative operation “\cdot ” such that

C: for every a,b\in G the equations a\cdot x = b and y\cdot a = b can be solved in G.

This blog post aims at proving the equivalence of this alternative definition with the usual definition of the group, as formulated in IsarMathLib’s Group_ZF.thy. The informal proofs come from an Aug. 14, 2005 post by buli on the matematyka.org forum.

An alternative definition of a group

We will use the multiplicative notation for the group operation. To do this, we define a context (locale) that tells Isabelle to interpret a\cdot b as the value of function P on the pair \langle a,b \rangle.


locale group2 =
  fixes P
  fixes dot (infixl \cdot 70)
  defines dot_def [simp]: a \cdot b \equiv P\langle a,b \rangle

The next theorem states that a set G with an associative operation that satisfies condition C is a group, as defined in IsarMathLib’s Group_ZF theory.


theorem (in group2) altgroup_is_group:
  assumes A1: G\neq 0 and A2: P \{\text{is associative on}\} G
  and A3: \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b
  and A4: \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b
  shows \text{IsAgroup}(G,P)
proof -
  from A1 obtain a where D1: a\in G
  with A3 obtain x where D2: x\in G and D3: a\cdot x = a
  from D1 A4 obtain y where D4: y\in G and D5: y\cdot a = a
  have T1: \forall b\in G.\ b = b\cdot x \wedge b = y\cdot b
  proof
    fix b assume A5: b\in G
    with D1 A4 obtain yb where D6: y_b \in G
      and D7: y_b\cdot a = b
    from A5 D1 A3 obtain xb where D8: x_b\in G
      and D9: a\cdot x_b = b
    from D7 D3 D9 D5 have
      b = y_b\cdot (a\cdot x)  and b = (y\cdot a)\cdot x_b
    moreover from D1 D2 D4 D8 D6 A2 have
      (y\cdot a)\cdot x_b = y\cdot (a\cdot x_b) and y_b\cdot (a\cdot x) = (y_b\cdot a)\cdot x
      using IsAssociative_def
    moreover from D7 D9 have
      (y_b\cdot a)\cdot x = b\cdot x  and  y\cdot (a\cdot x_b) = y\cdot b
    ultimately show b = b\cdot x \wedge  b = y\cdot b
  qed
  moreover have x = y
  proof -
     from D2 T1 have x = y\cdot x
     also from D4 T1 have y\cdot x = y
    finally show x = y
  qed
  ultimately have \forall b\in G.\ b\cdot x = b \wedge  x\cdot b = b
  with D2 A2 have \text{IsAmonoid}(G,P) using IsAmonoid_def
  with A3 show  \text{IsAgroup}(G,P)
    using monoid0_def monoid0.unit_is_neutral IsAgroup_def
qed

The converse of theorem altgroup_is_group: in every (classically defined) group the condition C holds.
In informal mathematics we can say “Obviously condition C holds in any group.” In formalized mathematics the word “obviously” is not in the language. The next theorem is proven in the context called group0 defined in IsarMathLib’s theory Group_ZF.thy. Similarly to group2 that context defines a\cdot b as P\langle a,b\rangle, where P: G\times G\rightarrow G is the group operation. It also defines notation related to the group inverse and adds the assumption that the pair (G,P) is a group to all its theorems. This is why in the next theorem we don’t explicitely assume that (G,P) is a group - this assumption is implicit in the group0 context.


theorem (in group0) group_is_altgroup: shows
  \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b and \forall a\in G.\forall b\in G.\ \exists y\in G.\ y\cdot a = b
proof -
  { fix a b assume A1: a\in G  b\in G
    let x = a^{-1} \cdot  b
    let y = b\cdot a^{-1} 
    from A1 have
      x \in  G  y \in  G and a\cdot x = b  y\cdot a = b
      using inverse_in_group group_op_closed inv_cancel_two
    hence \exists x\in G.\ a\cdot x = b and \exists y\in G.\ y\cdot a = b
  } thus
      \forall a\in G.\forall b\in G.\ \exists x\in G.\ a\cdot x = b and
      \forall a\in G.\forall b\in G.\ \exists y\in G.\ y\cdot a = b
qed


end

This blog post has been generated from IsarMathLib’s Group_ZF_1.thy theory file, see the relevant pages of IsarMathLib proof document.

See also the TiddlyWiki rendering of this post.

Tags:
Posted in Proofs | No Comments »