Chiron is a set theory designed for writing down, reason about and do mathematics. According to its purpose, it has an unusually broad range of basic notions. It contains a rich type system and, most notably, a facility to reason about syntactic expression.

Von Neumann–Bernays–Gödel set theory can be faithfully interpreted in Chiron. The former is usually axiomatized as a theory over first-order logic, the latter is self-standing in the way of a type theory. This entry gives a sketch of Chirons formalization. It starts out a little like the specification of a programming language and in fact the syntax of expressions is inspired by lisp. Indeed, Chiron feels a little like a programming language where you already know that things like lists and function are do make sense. Using a theory with a small number of logical notions from which others are defined certainly also has it merits. From the pedagogical standpoint for an introduction to foundations of mathematics itself, it is probably better to start from Logic or Type theory and then pass on to Set theory or Category theory. I'm interested in Chiron because this wiki deals with several different theories which are not necessarily well suited to express each other. In any case, due to the fact that most entries are about “everyday mathematics” rather than topics close to pure logic and the logical basic don't shine though all that much.

At the moment, this is the most formal of all the foundational entries. Note that I sometimes use the sign “$\equiv$” in the meta logic to introduce abbreviations for some mathematical expressions. In these cases, some simple pattern matching is up to the human user.

We want to work with an unending alphabet and providing it is, apart from a finite part, a task of the meta logic. So reasoning with Chiron always starts out with the specification of atomic expressions:

1. A countably infinite collection of symbols, denoted by $\mathcal S$, which includes certain default key words. (Examples of the key words are 'type', 'term', 'formula', 'if', 'op', 'op-app' and 'fun-app'.)
2. A countable collection of operator names, denoted by $\mathcal O$, which includes certain default built-in operator names. The operator names must be assigned a signatur. That's a sequences of the key words 'type', 'term' and 'formula'. (The operator names are similar to names of typed functions, and the corresponding operators are formalized using the symbols. Examples of the built-in operator names are 'in', 'type-equal' and 'not', but also 'set' and 'class'.)

The default expressions are summarized in Key words and built-in operator names.

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

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. Importantly, proper expression can contain improper expressions in their “$\operatorname{foo sequence}$”, and so Chiron can reason about those. An example of a formation rule is

$\large\frac{\text{if } x\text{ is a symbol and } \alpha \text{ is assigned 'type'}}{\text{then } (\operatorname{var},x,\alpha) \text{ is assigned 'term'}}$

• negation operation: Note that the negation of a logical proposition is again a proposition. This interpretation of “$\neg$” is usually part of the meta logic. As stated, 'op', 'op-app' and 'formula' are key words in $\mathcal S$ and 'not' is an in-built 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'. Reflect upon the syntax: key word in the first entry, operator name in the second, etc.

• negation of a formula: Now say $A$ is short for some other expression which is assigned 'formula'. Then its negation “$\neg A$” is the expression

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

In general, the overhead to capture some of the meaning of “$\neg$” inside the theory can seem a little of an overkill. But the point is that it actually makes things easier if we introduce many theories with new names and operations. For example we might specify $\in^{\text{ZFC}}$ to be an operatorname, define the associated operator and formulate axioms about it as expressions. We say that assigning a sequence to operator names provides us with a language $L$ and a language together with a set of axioms $\Gamma$ is a theory in Chiron.

• 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, from thie expression you can actually read of the type $\alpha$. Let me maybe say it 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.
• lambdas: 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)$. This could complactly be written $\lambda (x:\alpha).b$. I.e. this is a lambda term of a dependent product type $\beta(x)$.
• operators: Operators are expressions with first entry $\operatorname{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.
• sets and classes: The expression $(\operatorname{op},\operatorname{set},\operatorname{type})$ tells us that $\operatorname{set}$ is he operator name of a constant operator with image in $\operatorname{type}$. In turn $\mathrm{V}\equiv(\operatorname{op-app},(\operatorname{op},\operatorname{set},\operatorname{type}))$ represent the sets. The operator name $\operatorname{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)$.
• definite description $\operatorname{def-des}$: The expression $\iota(x:\alpha).\,B$ is ment to be the term which fulfills the formula $B$.

The following link contains a list of some basic proper expression: Chiron Notation. An example for a proper expression which is not built in is the following:

• empty set: This can be defined via the definite description $\iota(u:\mathrm{V}).\,\forall (v:\mathrm{V}).\,\neg(v\in u)$.
• matrix types: If we've defined natural numbers $\operatorname{N}$ in some reasonably way, then $O\equiv(\operatorname{op},\operatorname{matrix},\operatorname{N},\operatorname{N},\operatorname{type},\operatorname{type})$ will be part of the theory of matrices. For example, we might take $(\operatorname{op-app},O,3,5,Q)$ to denote the type of $3\times 5$ matrices with rational number entries.

I don't quite understand the semantics yet.

A long discussion of the semantics is given in the link in the intro. Here some crucial notes:

A bijective mapping from $\mathcal S\cup\mathcal O$ into the sets of some set theory with ordered pair induces a representation of expressions of Chiron. The representation of an expression is called construction.

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

Above in the example section, the expressions $\mathrm{V}$ and $\mathrm{C}$ were defined from the built-in operator 'set' and 'class' and the empty set was defined via definite description. We also have list and set constructions, what more do you need? 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.

Publications about Chiron on W. M. Farmers home page

Wikipedia: Von Neumann–Bernays–Gödel set theory

Foundations