Chiron: A Set Theory with Types, Undefinedness, Quotation, and Evaluation


William M. Farmer

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.