Logic

-About the axiom of choice:

• Schechter's home page: about the axiom of choice.
• Howard and Rubin's book: links between various consquences of the axiom of choice.
• Choiceless Grapher: Diagram creator for consequences of the axiom of choice.

-Foundations of mathematics:

• Metamath: A proof checker which allows you to define your formal system, and to code your proofs inside this formal system. There is also a big file for set-theory (set.mm), with mechanised proofs of first theorems in set-theory. The program also gives the list of the axioms which are needed in the proofs that are checked. So, if you run this program with the file set.mm, your computer will tell you when the axiom of choice is used in the file set.mm. For example, your computer will show you that the following things are provable in ZF (set-theory without choice): existence of uncountable ordinals, construction of the real numbers, transfinite recursion, ...

 
 
• Sylvain Poirier's home page: Set Theory and Foundations of Mathematics.
• Serge Burckel's home page: Works in Mathematics and Computer science.

-Logic in general:

• Mathematical Logic around the world: Some pointers in mathematical logic.

Analysis:

• Topology Atlas (Preprint server)
• Banach space bulletin board (Preprint server)

General interest:

• ZentralBlatt (Abstracts of mathematical papers)
• arxiv.org (Preprint server)

---

Marianne Morillon