Codex is my personal math journal.
Structure
Codex pages are organized according to their branches (e.g. Set Theory, Analysis) and topics (e.g. Functions, Series). Each page discusses a specific concept within a topic (e.g. Inverse Function from the topic Functions).
Codex is mostly made of entries. They look like this:
Blablablabla…
Each entry is either an axiom, a definition, a proposition or a remark (the entry’s type), labeled in the following format:
<concept>#<type>(-<tag1>-<tag2>-<...>)
-
All labels contain only uppercase letters, (maybe) numbers, and dashes.
-
<concept>is the abbreviation for the discussed concept on a page (e.g. Subset 🠆 SUB). It is also the code name of the page. The choice of this abbreviation is arbitrary. -
<type>is the abbreviation of the entry’s type:- Axiom 🠆 AX
- Definition 🠆 DEF
- Proposition 🠆 PROP
- Remark 🠆 REM
In Codex, proposition is a generalized term for mathematical results (theorems, lemmas, etc.). Every result, regardless of its role or importance, is labeled as a proposition.
-
<tag1>-<tag2>-<...>are optional tags used to further identify the entry. Usually only one tag is needed. Sometimes there is no tag at all, especially when the entry is the primary definition of a concept (e.g. SUB#DEF is the definition of subset). The choice of these tags is arbitrary.
Why?
Why not use the conventional format (“Definition 3.12”, “Theorem 5.4”)?
The more familiar system, which labels entries based on the order of their occurrences, works well for static texts. However, Codex is dynamic by its nature, meaning that entries are expected to be added, removed and rearranged every now and then. With the conventional system, such changes would require a lot of renumbering.
Using individual, symbolic labels avoids the problem, as the order doesn’t matter. Another advantage is that they are more descriptive, making them easier to remember (“Definition 5.1” vs. “DEF-SUB”).
Notes
-
By default, we work in $\ZF$ or $\ZFC$.
-
[$\limp\AC$] means a result or a definition relies on $\AC$.
[$\rimp\AC$] means a result implies $\AC$.
[$\lrimp\AC$] means a result is equivalent to $\AC$.