Once the type's constructors are specified, the eliminator functions and computation is determined by structural recursion. There are similar, more powerful ways to create types. These include induction-recursion and induction-induction. There is also a way to create similar types using only lambda terms, called Scott encoding. (NOTE: Type theories do not usually include coinductive types. They represent an infinite data type and most type theories limit themselves to functions that can be proven to halt.) Differences from set theory The traditional foundation for mathematics has been set theory paired with a logic. The most common one cited is Zermelo–Fraenkel set theory, known as "ZF" or, with the Axiom of choice, "ZFC". Type theories differ from this foundation in a number of ways. Set theory has both rules and axioms, while type theories only have rules. Set theories are built on top of logic. Thus, ZFC is defined by both the rules of first-order logic and its own axioms. (An axiom is a logical statement accepted as true without a logical derivation.) Type theories, in general, do not have axioms and are defined by their rules of inference. Set theory and logic have the law of excluded middle. That is, every theorem is true or false. When a type theory defines the concepts of "and" and "or" as types, it leads to intuitionistic logic, which does not have the law of excluded middle. However, the law can be proven for some types. In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a predicate function or use a dependently-typed product type, where each element is paired with a proof that the subset's property holds for . Where a union would be used, type theory uses the sum type, which contains new canonical terms. Type theory has a built-in notion of computation. Thus, "1+1" and "2" are different terms in type theory, but they compute to the same value. Moreover, functions are defined computationally as lambda terms. In set theory, "1+1=2" means that "1+1" is just another way to refer the value "2". Type theory's computation does require a complicated concept of equality. Set theory usually encodes numbers as sets. (0 is the empty set, 1 is a set containing