The 'Comment on formalities' is a plain text that adds everything that keeps the definition above to be fully formal. The “Elaboration” puts the definition into words. The “Discussion” is more informal as it tried to capture the motivation for the definition itself, and says explains the moral behind it.

Each entry starts with a title (Entry structure here) followed by the type of article (Meta here). At the moment there are the entry types

Meta, Note,

Framework, Collection, Type,

Haskell, Haskell class

Set, Function, Category, Functor, Natural transformation, Tuple

The entries end in lists of edges to other entries. The formal content of the edge tags depends on the entry type (e.g. for two connected Set entries, the tag “Subset” means the related entry defined as subset for but I might overload that word for other types too, if the meaning is sufficiently close).

See Template entry

Remarks: We don't find 'rule' in Set.

The root of the graph contains discussions on all sorts of notation used, but here is a short overview of the primitive symbols - the ones which aren't introduced in terms of previously defined ones. (E.g. the symbol for function definition $:=$ is primitive, while the symbol for function concatenation $\circ$ is defined in the context of set- or category theory.)

I uses letters and words using the common alphabets ($a,b$ etc. and $\alpha,\beta$ etc.) and indices.

For formal expressions, I use connectives and quantifiers from first order logic ($\land, \lor, \forall, \exists, \neg, (, ), =$) and the notation necessary for type judgements and definitions ($\frac{P}{Q}, \prod, \sum$).

The symbol $\dots$ is used either for a continuation (as in $a,b,\dots$) or to denote “is a”, as in ${\bf C}\dots\mathrm{Category}$, while the word 'in' denotes informal membership. The symbol $\in$ is introduced axiomatically.

$\mathrm{it}$

New symbols beyond the this language are introduced throughout the wiki (e.g. $\circ$). The symbol $\equiv$ is used in predicate definitions. The symbol $:=$ is used for function definitions, usually in connection with argument brackets and arrows $\to$ and $\mapsto$.

Every entry has one of the following key words associated with it. They can be considered part of the meta logic of the wiki.

Meta: This is the type of some entries at the root of the graph (like this one), and their content is completely informal.

Note: Literally just notes I take

Framework: Notes on mathematical frameworks close to foundation. Some of those are more or less formally specified within another framework, but some could also either be written down quite differently, or even taken as starting point

Set: This is the most common type of entry. It denotes that the mathematical object defined in the entry is a set in all the common set theories, see Set theory.

Function: This type Function denotes a function in the set theory, together with domain and codomain.

Type: Entries with heading Type denote types as introduced in Type theory.

Category: This one denotes categories as given in the typed definition in Category theory. Note that some categories will be small enough to model them as a set.

(old, probably not to be used at all: Object: The type Object denotes an object of some category. These will also be set s sometimes.)

Collection: This is used to enable us to speak about large mathematical objects without getting in trouble with paradoxes and without formally introducing a new type within our type theory. Our law here is the following: An entity $X$ defined by an entry of type Collection can nowhere in the wiki be used on the right hand side of $\in$. Assigning an entry the type Collection is really just a safety mechanism and doesn’t necessitate that it wouldn't be possible to give it one of the other types.

todo: call those “sort” to be less confusing.

The graph contains vertices $A,B,C,\dots$ with a type (Set, Category, Theorem,…) and arrows $A\mapsto_f B, A\mapsto_h B, B\mapsto_g C, \dots $ with a type (Subset of, Context, Related,…). Each vertex $B$ corresponds to an entry in the wiki and the text contains in a distinguished section

1. Its own name
2. Its vertex type
3. A list of arrow types, each followed by the names of source vertices $A_1, B_2, \dots$

The latter list gives us collections of typed arrows $A_1\mapsto B, A_2\mapsto B, \dots$.

Most entries contain definitions of mathematical objects in terms of axioms (although a few only state theorems). Specifically, they generally specify collections of objects $x$ by predicates $P(x)$ in the sense of $X_B=\{x|P_B(x,X_B)\}$ (although a few are proper classes as well as categories or objects). Now the description of how the entries are structured:

1. Each entry $B$ start with its name, followed by its type.
2. Then a required context is declared (blue), which is a list of mathematical objects needed for the definition that's following. E.g. “let $G\in\mathrm{Group}$ be a group, let $n\in\mathbb N$ be a natural number and let $\log$ denote the logarithm”. Note that formalizing the context let's one “level up” certain objects. E.g. if $a\in A$ is in the context of the definiton of a function $f:B\to C$, then one is lead to consider is the function $\bar f:A\times B\to C$ makes sense as well, etc.
3. Then the name of the defined object is stated (orange)
4. Then the axioms are given (green, possibly preceded by temporal context declarations in blue)
5. Then comes the informal Discussion section
6. then we have the Parents section with is a list of types, each containing names of other entries, see next section

The types of arrows $A\mapsto B$ carry mathematical information about the entries. Here are the details:

• Subset of

For this arrow, both source and target must represent a set, or more generally a category. The vertex $B$ can be obtained from $A$ by keeping $A$'s context and adding axioms $P_\mathrm{new}$ to $P_A'$. For sets we find $X_B=\{x|P_A(x,X_A)\land P_\mathrm{new}(x)\}=\{x|x\in X_A\land P_\mathrm{new}(x)\}\subset X_A$.

Note: As discussed in the Discussion section of this entry below, formally the above specification is executed only up to isomorphism. Of course, this implies that all (unstructured) sets contain all sets of same or smaller cardinality, but I'm not attempting to point out all subset relations anyway, only those with purpose for doing mathematics. Moreover, some entries are structured sets $X:=\langle A,B,C,...\rangle$ (e.g. in set theory, a group $\langle G,*\rangle$ formally is a set $G$ and a map $*:G\times G\to G$), and so for not to have to introduce “Subgroup of” and “Subfield of” etc. etc., we extend “Subset of”-edges for lists to mean the first entries (like $\pi_1(X)=A$) have the subset relation and the structure is carries over simply by restriction.

Subset of for Collection: If a is of type A, and we form the collection of A's, then the pair <a,b>, <a,<b,c»,etc. are also in it. This formalizes the notion of object with structure.

• Element of

The $X_B$ is an element of $X_A$.

• Context

Here we find the names of the entries which are used in the context. Note: As also discussed in the Discussion section of this entry below, for readability I don't necessarily always specify the full context.

Theorem entries can't be rRequirements for sets or other entries. This is because the specification of sets doesn't depend on the truth of other sentences, only their within a particular theory at hand does.

• Restriction of

Function restriction. So in the set theoretic model of functions as set of pairs, this is a special case of subset of - here this is a special case of Subset.

• Refinement of

141025 - exists (formulaic) functions f from it (of the lower (refined) entry) to it (of the higher entry) as well the higher context. See Metric space and Hausdorff space.

150121 - this should include partially evaluated functions. E.g. $f(x,y):=x^2+y^3$, then $g(y):=9+y^3$ is a refinement of it.

• Equivalent to

The is a “bijection of information” to be pointed out. Both entries define object which can be directly read of from one another. (This should be the same as Refinement of in both directions.)

• Related

This is the informal arrow, connecting to entries which are conceptually related.

• 'some sort of functional relation arrow'

“Specification of” is elements of the context are fixed.

“Structure of” $A\leftarrow \langle A,\dots\rangle$, as in $\langle\mathbb{R},+_\mathbb{R},\cdot_\mathbb{R}\rangle$ is a structure of $\mathbb{R}$.

“Language” or “Vocabolary” would be a good idea (e.g. for things like $\log$, see discussion above), in addition to “Context”, which I now treat more specific.

todo: rewrite/update this

All the entries start with a Definition section in which the object is defined, which the entry represents. The information of what and how that thing is defined is highlighted in green color, with necessary complementary information in blue. Similarly, I will use yellow and orange when making predicate definitions in the Ramification section.

Color scheme

Below the boxes, there might also be explainatory text. In the informal discussion I use ^, as in

What the use of the boxes does is to export information about the objects (sets) to the separate blue boxes. This way I need more lines, but the definitional expression are more clearer and without potential ballast. Besides general declaration of types, what is nice is that it decomposes expressions of the form $\forall x\ (P(x)\implies Q(x))$ and $\exists x\ (P(x)\land Q(x))$ into two parts respectively. Such a restricted quantification is also discussed in the entry set theory. At the same time, I use the boxes to decompose the set-builder notation $X:=\{f(x)|P(x)\}$. In the entry set theory, there is also a section dedicated to the set-builder notation.

Why do I do this? I want to talk about mathematical objects and their special cases. When I started to write down the relation between differential equations, like for example “$y'(x)=a(x)y(x)+b(x)$” and “$y'(x)=\sin(x)y(x)$,” I realized that I would have to quantify the function spaces for $a$ and $b$, and it would be madness to do this in one line. If I wanted to restrict the domain of interest, I would actually even have to write the initial function as “$\forall x\in \mathbb R\ (y'(x)=a(x)y(x)+b(x))$.” Or, even a little more formally “$\forall x\ [x\in \mathbb R\implies y'(x)=a(x)y(x)+b(x)]$.” So what I do is to specify the domain of all our variables! Notice however that I will still write down formulas implies universal closure: We might drop the all-quantors before every-day equations and post them I free variables, e.g. we write “$(n+1)^2=n^2+2n+1$”, and not “$\forall n\ ((n+1)^2=n^2+2n+1)$”.

Now follow some examples in full formallity. Firstly, a motivating example. Axiom of choice:

What it meas in words: We consider any nonempty sets $X$ which contain smaller sets $x$. Now by the axiom we always have a function $f$ for $X$, which can reach into the small sets, i.e. for all $x$, the value $f(x)$ is a chosen element from that $x$.

In standard notation without the external “blue box quantification”, this reads on Wikipedia

“$\forall X\ \left[ \emptyset \notin X \implies \exists f: X \to \bigcup X : \forall A \in X \, ( f(A) \in A ) \right].$”

which itself uses some abbreviations to express

“$\forall X\ \left[ \emptyset \notin X \implies \exists f\ [(f: X\to\bigcup X)\land \forall A\ (A\in X \land ( f(A) \in A ))] \right].$”

Now I give a second more abstract example:

says “$\forall b\ [P(b)\implies \exists c\ (Q(c)\land (S(a)=d)\land T(b,c,d))]$, where $a$ is any set and $d$ is any set for which $R(d)$.”

We usually want to use this notation to define sets. Since I first provide input for the defintion and also state the name of the thing I define, I switch between blue and green two times:

says “Let $B$ be any except for $\emptyset$. Then $Z_B=\{f(x)|\forall a\ (P(a)\implies \exists b\ (b\in B\land R(a,x,b)))\}$.” We might also extend the defintion section by introducing common alternative ways of writing mathematics.

===== Entry title

e.g. Group

==== Main Sections

e.g. Discussion

=== SubSections

• Cohenrence - explanation why the formula makes sense
• Terminology - comment on the name
• Notation - alternative notations in use
• Theorems - theorems which don't deserve their own entry
• Predicates - …
• Alternative definitions - …
• Ad hoc introduction - motivation of how this entry can be understood as “axiom of choice”
• Derivation - explanation of the derivation from the entries in the context section

todo: notation rules, and maybe links to the Glossary

note: seperate the axioms part from the set definitions part. the biggest set is Set which can be viewed as the class of sets for some axiomatic framework. Functions (the sets), defined in Function are the internal homs of Set - and/but they are generally defined not via $\equiv$ but via $\:=$, which implies that these sets know their corresponding arrow in Set and hence their dom and codom can be obtained from those $f$ via $\mathrm{dom}(f)$ resp. $\mathrm{codom}(f)$.

== Headlines

e.g. names of formulas

remark: it there is reason to put an external link into the main body, it must also be in the References.

no requirement links to Meta entries (otherwise stuff like the unordered pair gets connected to set theory, which makes the grath - at least in the graphviz mode - not nice to look at.)

Elaboration explaining the definition Motivation motivation for the Idea associated key insight

About