Chiron is a set theory designed for writing down, reason about and do mathematics. It's self-standing in that it actually comes with it's own logic, which is formally specified. According to its purpose, it has an unusually broad range of basic notions. Notably it contains a rich type system with many standard types and tools to reason about syntactic expression themselves.

I use it because this wiki deals with several theories of foundational character are not necessarily suited to express each other. In any case, due to the fact that more entries are about “everyday mathematics” definition rather than topics close to pure logic, the very foundational axioms will in general not be visible anyway.

Now I provide the basic outline of Chirons workings. The definition starts out a little like the specification of a programming language and in fact, the syntax of expressions is inspired by lisp.

Since we want to work with an unending storage of words, we don't want to specify all of them. So providing the full alphabet is a task to be done on a meta level. Reasoning with Chiron starts out with the specification of atomic expression:

1. A countably infinite collection $\mathcal S$ of symbols, including certain default key words.
2. A countable collection $\mathcal O$ of operator names, including certain default build-in operator names, which must be assigned certain sequences of the key words “type”, “term” and “formula”. The data of this section point is called a language for chiron.

The special words are summarized in Key words and build-in operator names. Examples of the key words are 'type', 'term', 'formula', 'if', 'op', 'op-app' and 'fun-app'. Examples of the build-in operator names are 'set', 'class', 'type-equal' and 'not'. The first two are assigned 'type', the third is assigned 'type, type, formula' and the last one is assigned 'formula, formula'. The operator names are like typed symbols.

A compound expressions is of the form “$(e_1,e_2,\dots,e_n)$” where $n\ge 0$ and the $e_i$ are atomic of compound expressions. So a general expression is an atomic expressions or a tree, which eventually stores atomic expressions.

negation operation: Note that the negation of a logical proposition is again a proposition. Now remember that 'op', 'op-app' and 'formula' are key words in $\mathcal S$ and 'not' is an in-build operator name in $\mathcal O$ which happens to be assigned 'formula, formula'. A particular default expression of Chiron is

$(\operatorname{op}, \operatorname{not}, \operatorname{formula}, \operatorname{formula})$

This is what is called an operator and the point is that it stores some information about the operator name 'not'. The features of that example (key in the first entry, name in the second, etc.) should be reflected upon in the next section.

negation of a formula: Now say $A$ is short for some other expression which is assigned 'formula'. Then its negation is

$(\operatorname{op-app},(\operatorname{op}, \operatorname{not}, \operatorname{formula}, \operatorname{formula}),A)$

Chiron comes with 25 formation rules. They let you construct proper expressions, which are of the form “$(\operatorname{key word}, \operatorname{foo sequence})$”, where the “$\operatorname{foo sequence}$” is specified to fulfill certain conditions. Conversely the formation rules let you check if a given expression is proper. E.g. the not-operation above happens to be a proper one, unsurprisingly. The nice thing is that proper expression can contain improper expressions in their “$\operatorname{foo sequence}$”, and so Chiron can reason about those.

• variables: If it's established that $\alpha$ is in $\mathcal O$ with assignment 'type' and $a$ in $\mathcal S$, then $(\operatorname{var},a,\alpha)$ is an expression assigned 'term'. In particular, this object tells us that it's a term of type $\alpha$. Let me maybe say that again differently: As an object of the theory, $(\operatorname{var},a,\alpha)$ is a 'term' and, as a term in the theory, it is also of a certain type.
• functions: If $\beta$ is a type, $b$ is a term of type $\beta$ and $(\operatorname{var},x,\alpha)$ is a term, then $(\operatorname{fun-abs},(\operatorname{var},x,\alpha),b)$ is a term of type $(\operatorname{dep-fun-type},(\operatorname{var},x,\alpha),\beta)$. If the type of (the term corresponding to the symbol) $x$ is clear, that could less formally be written $\lambda x.b$. I.e. that's a lambda term of a dependent product type.
• operators: Operators are expressions with first entry $op$ and are essentially the functions on the most rudimentary level. An $\operatorname{op-app}$-expression eats an $\operatorname{op}$-expression so that the result has the type of the output. The negation example was already given. Operators themselves don't have a function type, whereas the type system of the lambda terms in the theory is actually more elaborate than some other type theories.
• sets, classes and $\in$: The expression $(\operatorname{op},\operatorname{set},\operatorname{type})$ tells us that $\operatorname{set}$ is he operator name of a constant operator and in turn $\mathrm{V}\equiv(\operatorname{op-app},(\operatorname{op},\operatorname{set},\operatorname{type}))$ represent the sets. The operator name 'class' is treated in the same way and gives us $\mathrm{C}$.
• membership: Note that 'in' is also an operator name and so the string “$a\in b$” is just the expression $(\operatorname{op-app},(\operatorname{op},\operatorname{in},\mathrm{V},\mathrm{C},\operatorname{formula},a,b)$.

The following link contains a list of some basic proper expression: Chiron Notation.

denote?

The proper expressions denote values, while improper expressions are non-denoting.

There is $\mathrm{T}, \mathrm{F}, \bot$ and $D_s$. That's true, false, undefined and the domain of discourse $D_s$.

We distinguish between two subdomains $D_v\subset D_c\subset D_s$.

1. The “meta” domain is the collection of superclasses.
2. A superclasses contains the normal mathematical working universes called classes.
3. If a class is a member of such a universe, it's called a set.

Most math can be done inside the third level, while e.g. categories are often proper classes.

Lastly there are $n$-ary operations mapping to either $D_s$, $D_c\cup\{\bot\}$ or $\{\mathrm{T},\mathrm{F}\}$. Many operations can be represented inside of $D_c$, where they are called partial functions.

$\equiv$?

Publications about Chiron on W. M. Farmers home page

Foundations