===== Chiron =====
==== Framework ====
>todo: Make a syntax entry for formal language, and join it with Chiron, Haskell, as well as logical theories.

{{ chiron-moreau.jpg?X300}}

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. So for exmaple, there is a way to express "f(x)", a function applied to an argument. In conventional set theories, this is only a notation defined in the meta theory. 

[[http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory|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 (we don't repeat any set theory axioms in this entry), the latter is self-standing in the way of a type theory. This entry gives a sketch of [[http://imps.mcmaster.ca/doc/chiron-tr.pdf|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.

=== Expressions ===
== Atomic expressions ==
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//:
  - A countably infinite collection of //symbols//, denoted by $\mathcal S$, which includes certain default //key words//. (The key words are listed in the last section of this entry. Examples are 'type', 'term', 'formula', 'if', 'op', 'op-app' and 'fun-app'.)
  - 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]]. 

== Compound expressions ==
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. 

== Proper and improper 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'}}$

== Example of a proper expression ==
  * **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)$

=== Semantics ===
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 operator name, define the associated operator and formulate axioms about it as expressions. 

A long discussion of the semantics is given in the link in the intro. Roughly speaking, the expressions **operators**, **types**, **terms** and **formulas** make up the "set theory objects" of Chiron. Terms denote classes (including sets), types denote superclasses (collections of classes), formulas denote truth values and operators denote operations, which construct more expressions. Other expressions are "non-denoting". However, there is a lisp-like $\operatorname{quote}$-$\operatorname{eval}$ mechanism to map any expression to a "set-level object". Without going into detail, one must make such an assignment to elements of $\mathcal{S}\cup\mathcal{O}$ and then recursively extend it to trees via ordered pairs.

== More examples of expressions ==
  * **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}$. Remember that, e.g. in NBG-set theory, a class is a set if it's the member of another class.
  * **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)$.
  * **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. The point of variables is to be bound.  
  * **existential quantification**: $(\operatorname{exists},(\operatorname{var},a,\alpha),B)$ or $\exists(x:\alpha)\,B$ for short, is an expression!
  * **definite description**: The expression $(\operatorname{def-des},(\operatorname{var},a,\alpha),B)$ denotes the term term which fulfills the formula $B$. We also write this as $\iota(x:\alpha).\,B$. Note that $\operatorname{def-des}$ is a keyword (not an operator name) and so the corresponding expression a priori isn't denoting. So we can describe the term $\lim_{x\to\infty}\sin{(\frac{1}{x})}$, which usually is semantically undefined.
  * **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)$.
  * **equality**: $\operatorname{type-equal}, \operatorname{term-exqual}$ and $\operatorname{formula-equal}$ are operator names too.

The following link contains a list of some basic proper expression: **[[http://imps.mcmaster.ca/doc/chiron-notation.pdf|Chiron Notation]]**. An example for a proper expression which is not built in is the following: 
  * **empty set**: This can be described 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.

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 $\mathrm{T}, \mathrm{F}, \bot$ and list and set constructions. What more do you need? 

Finally, some terminology: 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//. Moreover, 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//.

Lastly, we list the key words and operator names.

=== Key words ===
Main key words:
<code>
op
type
term
formula
op-app
var
type-app
dep-fun-type
fun-app
fun-abs
if
exists
def-des
indef-des
quote
eval
</code>

Extended:
<code>
con
uni-exists
forall
set-cons
list-cons
class-abs
dep-type-prod
left-type
right-type
dep-ord-pair
dep-head
dep-tail
</code>

=== Built-in operator names ===
Names with their signatur assignments: 

<code>
set             type
class           type
op-names        term
lang            type
expr-sym        type
expr-op-name    term, type
expr            term, type
expr-op         term, type
expr-type       term, type
expr-term       term, type
expr-term-type  term, term, type
expr-formula    term, type
in              term, term, formula
type-equal      type, type, formula
term-equal      term, term, type, formula
formula-equal   formula, formula, formula
not             formula, formula
or              formula, formula, formula
</code>

The signature is, roughly, "type of constant" if only one keyword is given, "function type" else. In the operators "$\mathrm{(op,myname,\dots)}$" corresponding to the operatorname $\mathrm{myname}$, the keyword 'term' is replaces by some explicit thing. 

=== Reference ===
[[http://imps.mcmaster.ca/wmfarmer/chiron.html|Publications about Chiron on W. M. Farmers home page]]

Wikipedia: [[http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory|Von Neumann–Bernays–Gödel set theory]]

==== Parents ====
=== Related ===
[[Type theory]], [[Set theory]]