Chiron: A Set Theory with Types, Undefinedness, Quotation, and
Evaluation
William M. Farmer
2012
Abstract
Chiron is a derivative of von-Neumann-Bernays-G\"odel (NBG) set theory
that is intended to be a practical, general-purpose logic for
mechanizing mathematics. Unlike traditional set theories such as
Zermelo-Fraenkel (ZF) and NBG, Chiron is equipped with a type system,
lambda notation, and definite and indefinite description. The type
system includes a universal type, dependent types, dependent function
types, subtypes, and possibly empty types. Unlike traditional logics
such as first-order logic and simple type theory, Chiron admits
undefined terms that result, for example, from a function applied to
an argument outside its domain or from an improper definite or
indefinite description. The most noteworthy part of Chiron is its
facility for reasoning about the syntax of expressions. Quotation is
used to refer to a set called a construction that represents the
syntactic structure of an expression, and evaluation is used to refer
to the value of the expression that a construction represents. Using
quotation and evaluation, syntactic side conditions, schemas,
syntactic transformations used in deduction and computation rules, and
other such things can be directly expressed in Chiron. This paper
presents the syntax and semantics of Chiron, some definitions and
simple examples illustrating its use, a proof system for Chiron, and a
notion of an interpretation of one theory of Chiron in another.