Topology Database, Version 0.1

The creative process of mathematics, both historically and individually, may be described as a counterpoint between theorems and examples.

— L.A. Steen and J.A. Seebach, Jr. in Counterexamples in Topology

An encyclopedic reference of examples in point-set topology called Counterexamples in Topology was published 1970. It contains over one hundred different examples which clarify the subtle differences between the dozens of definitions that make up the subject. This website is an attempt to rigorously recreate and extend this book with a database of theorems and counterexamples, a wiki-like version control scheme, and an automated reasoning system to work out the mundane tautological facts.


A picture of Alexander's Horned Sphere

The topics covered here fall under the subject of point-set topology, a mathematical theory that describes the geometric properties of topological spaces that are unaffected by continuous deformations. Much of the subject is defining various adjectives to the word space and then proving which combinations of these adjectives logically imply other adjectives. For example, one might want to know if a metrizable space implies a hausdorff space, or maybe if you have a connected, compact, t3 space could it possibly be separable? At this website, users can enter theorems with proof but then answer other questions with those theorems that are implied simply by the present theorems. Additionally users can enter counterexamples and prove properties of those counterexamples, in order to disprove other questions.

To begin collaborating with the other users on this site, you need some prerequisite knowledge. Namely, you must know exactly what a topological space is.

Definition: A topological space (or just space for short) is a pair of sets (X, T). T is a set of subsets of X such that
  1. T contains both X and the empty set,
  2. the union of any number of sets in T is a set in T, and
  3. the intersection of any two sets in T is a set in T.

If you haven't encountered this definition before, it may take a bit of time to understand it. (If you're as slow as I am, that bit of time is about three months.) I recommend picking up a copy of Munkres's Topology and doing some exercises. However, once you understand this definition you have enough knowledge to start exploring the website. Start at the "adjectives", the axioms, then make your way over to the theorem search or space table, and begin exploring.

Project Goals

While studying for an exam in my topology course, I made a simple chart of the implications between different spaces to post above my desk for reference. The complexity of the web of arrows intrigued me and I wondered which absent arrows could be added.


My implication graph. (a larger version)

I built this website so that internet users could answer that question for me. I want to know what implication arrows are missing; that is, I want a list of the unknown theorems so that I can sit down and try to prove them.

Internet mathematics is lacking something (MathML?) and that deficiency seems to push interesting discussions offline. This site is an experiment in collaborative internet mathematics, I want to see what works and what doesn't work.

Finally, perhaps this website can be resource for students studying point-set topology.

DNF and Resolution

Although the interface of this website presents all the theorems as implications, they are actually stored in the database as logical clauses in disjunctive normal form. For example, an implication like

A ∧ ¬ B → C

would be stored as the disjunction of literals

¬ A ∨ B ∨ C.

Clauses can queried directly by URL. The above clause could be accessed at

http://topology.tinyclouds.org/clause/not_A/B/C/

Only true and unknown clauses are stored in the database. False clauses can be disproved quickly with the counterexample database.

All logical inference on this site is done using logical resolution: if two clauses are known with an atom in common but with different signs, then you may resolve the two clauses to infer a new clause. For example

¬ A ∨ B ∨ C and A ∨ ¬ D ∨ E

imply a new clause with the common literal removed

B ∨ C ∨ ¬ D ∨ E

Algorithms

The basic inference task takes as input a number of literals (axioms with a sign) and outputs a list of all the literals which can be inferred from those. The algorithm works as follows

Input: A finite list of literals, a1, ... , an and all the clauses (theorems) in the database.

Output: A contradiction error or finite list of literals,

a1, ..., an, b1, ... , bm

that can be concluded from the input.

  1. Mark all of the input literals as KNOWN.
  2. Check if there is a clause
    α1 ∨ ... ∨ αr
    (where each αi is a literal: that is, it could have a positive or negative sign, like αi = ¬ A)
    such that there are r-1 literals of opposite signs already marked as KNOWN. If so, mark the remaining literal from the clause as KNOWN. If it happens a clause has r-1 literals matching the KNOWN literals, and the remaining literal is already marked but of the wrong sign then return a contradiction.
  3. Repeat step 2 until while the number of marked literals is growing.
  4. Return the marked literals.
(Add more here.)

Issues

First of all, this code is very young and there are many bugs hidden in these pages. There are issues with every feature.

Although I encourage users to enter latex formulas into the proofs and descriptions, there is no code yet to display this in HTML. It seems there is no reasonable way to do this and I'm reluctant to implement this feature—perhaps MathML will be okay since usually the formulas won't be too complex.

I think that this system should scale fairly well but maybe not. Inference can be done in linear time with respect to the number of stored theorems, so unless there are tons of theorems the site should be mildly responsive. If this is not the case (which is likely since resolution is NP-hard), then some sort of task queue would need to be setup to do inference.

I'd like some more features: allow users to mark important theorems or spaces for later review (like gmail's star feature). A list of the most marked unsolved theorems. Custom counterexample tables.

Licenses and Development

This website is free software and is released under Version 2 of the GNU General Public License. It is copyright in 2006 by Ryan Dahl (coldredlemur@gmail.com, tinyclouds.org). The website was written in the Ruby programming language using the Ruby on Rails website development framework.

As you may have noticed, this website is far from complete. Errors lurk everywhere, obviously desirable features are missing, and the design is really boring. I appreciate any bug fixes, feature enhancements, or other help that the users of the website could furnish.

(link to source code)