Welcome to SetTheoryCaml, an OCaml project dedicated to the exploration and study of the Axiom of choice and its applications in mathematics and computer science, particularly within the framework of type theory.
This project aims to provide a comprehensive study of the Axiom of choice (AC), from its origins to its implications in modern theoreitcal work. Through OCaml implementations, we explore various principles and lemmas associated with AC, diving into both mathematical logic and pratical applications.
In this section, we explore the historical development of the Axiom of Choice. Originating from Zermelo's work in the early 20th century, the Axion of Choice has been a fundamental component of set theory and an essential tool in many areas of mathematics.
- Timeline: A brief timeline of major milestones related to the Axion of Choice.
- Key Figures: Discussion of significant mathematicians like Zermelo and their contributions.
The Axiom of Choice is famously independent of the other axioms of set theory, meaning that it can neither be proved nor disproved from them.
- Independence Proofs: An overview of Cohen's work using forcing to show the independence of the Axiom of Choice.
- Consistency: How the addition of the Axiom of Choice affects the consistency of set theory.
Zorn's Lemma, which is equivalent to the Axiom of Choice, is a powerful tool in many fields of mathematics. We will discuss its formulation and implications.
- Equivalence: Proofs showing the equivalence between Zorn’s Lemma and the Axiom of Choice.
- Applications: Examples of how Zorn’s Lemma is applied in algebra and other fields.
This section demonstrates the versatility of the Axiom of Choice through various applications in analysis, topology, and more.
- Constructive Examples: How AC is used to construct various mathematical objects.
- Controversial Aspects: Discussion of the "non-constructive" nature of AC and its critics.
Exploring the relationship between the Axiom of Choice and different logical systems, focusing on its role in proofs and theorem formulation.
- Logical Frameworks: How AC fits within different logical systems.
- Implications: Impacts on logic and proof strategies.
In the supplementary document, we connect the Axiom of Choice with type theory, particularly focusing on how it influences concepts within type systems in programming languages like OCaml.
- Type Theory Basics: Introduction to type theory.
- AC in Type Systems: Exploration of how the Axiom of Choice might manifest within type systems, with theoretical and practical considerations.
We welcome contributions from both mathematical and programming communities. Whether you're interested in improving the code, adding new mathematical proofs, or expanding the documentation, your input is valuable.