the empty set, etc. See Set-theoretic definition of natural numbers.) Type theory can encode numbers as functions using Church encoding or more naturally as inductive types. The constructors "0" and "S" created by the inductive type closely resemble Peano's axioms. Set theory has set-builder notation. It can create any set that can be defined. This allows it to create Uncountable sets. Type theories are syntactic, which limits them to a countably infinite terms. Additionally, most type theories require computation to always halt and limit themselves to recursively generable terms. As a result, most type theories do not use the Real numbers but the Computable numbers. In set theory, the Axiom of Choice is an axiom and is controversial, particularly when applied to uncountable sets. In type theory, the equivalent statement is a theorem (type) and is provable (inhabited by a term). In type theory, proofs are mathematical objects. The type "x+1 = 1+x" cannot be used unless there is a term of the type. That term represents a proof that "x+1 = 1+x". Thus, type theory opens up proofs to be studied as mathematical objects. Proponents of type theory will also point out its connection to constructive mathematics through the BHK interpretation, its connected to logic by the Curry–Howard isomorphism, and its connections to Category theory. Technical details A type theory is a mathematical logic. It is a collection of rules of inference that result in judgements. Most logics have judgements meaning "The term is true." or "The term is a well-formed formula.". A type theory has additional judgements that define types and relate terms to types. Terms A term in logic is recursively defined as a constant symbol, variable, or a function application, where a term is applied to another term. Some constant symbols will be "0" of the natural numbers, "true" of the Booleans, and functions like "S" and "if". Thus some terms are "0", "(S 0)", "(S (S x))", and "if true 0 (S 0)". Judgements Most type theories have 4 judgements: " is a type." " is a term of type ." "Type is equal to type ." "Terms and are both of type and are equal." The judgements can be made under an assumption. Thus, we might say, "assuming is a term of type 'bool' and is a term of type 'nat' , (if x y y) is a term of type 'nat'". The mathematical