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. Therefore, I use it as the language with respect to which, in doubt, the syntactic expression in this wiki should be understood. In any case, I also use it to speak about how the default theories such as ZFC together with their sometimes cumbersome definitions.

The definition of Chiron starts out a little like the specification of a programming language and in fact, the syntax of expressions is inspired by lisp.

Reasoning with Chiron starts out with the specification of atomic expression:

1. A countably infinite collection of symbols, including certain default key words.
2. A countable collection of operator names, including certain default build-in operator names, which must be assigned certain sequences of the key words “type”, “term” and “formula”.

They are summarized in Key words and build-in operator names. Examples of the key words are “type”, “term”, “formula”, “fun-app” and “if”. 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 a tree, which eventually stores atomic expressions.

Chiron comes with 25 formation rules. They let you construct proper expressions, which are of the form

“$\text{(keyword, foo sequence)}$”

where the “$\text{foo sequence}$” is specified to fulfill certain conditions. That's essentially a recursive checking of assignments. One should maybe not say “type checking” at this level, because “type” is just one of the many keywords above. The assignment can be a more general expression.

The following link contains a list of some basic notions and gives an rough idea: Chiron Notation.

• If it's established that $\alpha$ is an operator name with assignment “type” and $a$ is a symbol, then $(\operatorname{var},a,\alpha)$ is assigned “term”, and in particular it also says that it's a term of type $\alpha$. I.e. 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.
• 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)$. That could be written $\lambda (x:\alpha).b$, a function of the dependent product type.
• Operators are expressions with first entry “$\operatorname{op}$” and are essentially the functions on the most rudimentary level. They don't have a function type, which the type system of the lambda terms is actually more elaborate than usual.

denote?

The proper expressions denote values. There are also improper non-denoting expressions.

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