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 and
illustrates its use with some simple examples.