Setoid
Encyclopedia
In mathematics
, a setoid (also called an E-set) is a set (or type) equipped with an equivalence relation
.
Setoids are studied especially in proof theory
and in type-theoretic foundations of mathematics
. Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the quotient set (turning equivalence into equality). In contrast, setoids may be used when a difference between identity and equivalence must be maintained, often with an interpretation of intension
al equality (the equality on the original set) and extension
al equality (the equivalence relation, or the equality on the quotient set).
In proof theory, particularly the proof theory of constructive mathematics based on the Curry–Howard correspondence, one often identifies a mathematical proposition with its set of proofs (if any). A given proposition may have many proofs, of course; according to the principle of proof irrelevance, normally only the truth of the proposition matters, not which proof was used. However, the Curry–Howard correspondence can turn proofs into algorithm
s, and differences between algorithms are often important. So proof theorists may prefer to identify a proposition with a setoid of proofs, considering proofs equivalent if they can be converted into one another through beta conversion or the like.
In type-theoretic foundations of mathematics, setoids may be used in a type theory that lacks quotient types to model general mathematical sets. For example, in Per Martin-Löf
's Intuitionistic Type Theory
, there is no type of real number
s, only a type of regular Cauchy sequences of rational number
s. To do real analysis
in Martin-Löf's framework, therefore, one must work with a setoid of real numbers, the type of regular Cauchy sequences equipped with the usual notion of equivalence. Predicates and functions of real numbers need to be defined for regular Cauchy sequences and proven to be compatible with the equivalence relation. Typically (although it depends on the type theory used), the axiom of choice will hold for functions between types (intensional functions), but not for functions between setoids (extensional functions). The term "set" is variously used either as a synonym of "type" or as a synonym of "setoid".
In constructive mathematics, one often takes a setoid with an apartness relation
instead of an equivalence relation, called a constructive setoid. One sometimes also considers a partial setoid using a partial equivalence relation
or partial apartness. (see e.g. Barthe et. al., section 1)
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, a setoid (also called an E-set) is a set (or type) equipped with an equivalence relation
Equivalence relation
In mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
.
Setoids are studied especially in proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
and in type-theoretic foundations of mathematics
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
. Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the quotient set (turning equivalence into equality). In contrast, setoids may be used when a difference between identity and equivalence must be maintained, often with an interpretation of intension
Intension
In linguistics, logic, philosophy, and other fields, an intension is any property or quality connoted by a word, phrase or other symbol. In the case of a word, it is often implied by the word's definition...
al equality (the equality on the original set) and extension
Extension (semantics)
In any of several studies that treat the use of signs - for example, in linguistics, logic, mathematics, semantics, and semiotics - the extension of a concept, idea, or sign consists of the things to which it applies, in contrast with its comprehension or intension, which consists very roughly of...
al equality (the equivalence relation, or the equality on the quotient set).
In proof theory, particularly the proof theory of constructive mathematics based on the Curry–Howard correspondence, one often identifies a mathematical proposition with its set of proofs (if any). A given proposition may have many proofs, of course; according to the principle of proof irrelevance, normally only the truth of the proposition matters, not which proof was used. However, the Curry–Howard correspondence can turn proofs into algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
s, and differences between algorithms are often important. So proof theorists may prefer to identify a proposition with a setoid of proofs, considering proofs equivalent if they can be converted into one another through beta conversion or the like.
In type-theoretic foundations of mathematics, setoids may be used in a type theory that lacks quotient types to model general mathematical sets. For example, in Per Martin-Löf
Per Martin-Löf
Per Erik Rutger Martin-Löf is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in...
's Intuitionistic Type Theory
Intuitionistic type theory
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
, there is no type of real number
Real number
In mathematics, a real number is a value that represents a quantity along a continuum, such as -5 , 4/3 , 8.6 , √2 and π...
s, only a type of regular Cauchy sequences of rational number
Rational number
In mathematics, a rational number is any number that can be expressed as the quotient or fraction a/b of two integers, with the denominator b not equal to zero. Since b may be equal to 1, every integer is a rational number...
s. To do real analysis
Real analysis
Real analysis, is a branch of mathematical analysis dealing with the set of real numbers and functions of a real variable. In particular, it deals with the analytic properties of real functions and sequences, including convergence and limits of sequences of real numbers, the calculus of the real...
in Martin-Löf's framework, therefore, one must work with a setoid of real numbers, the type of regular Cauchy sequences equipped with the usual notion of equivalence. Predicates and functions of real numbers need to be defined for regular Cauchy sequences and proven to be compatible with the equivalence relation. Typically (although it depends on the type theory used), the axiom of choice will hold for functions between types (intensional functions), but not for functions between setoids (extensional functions). The term "set" is variously used either as a synonym of "type" or as a synonym of "setoid".
In constructive mathematics, one often takes a setoid with an apartness relation
Apartness relation
In constructive mathematics, an apartness relation is a constructive form of inequality, and is often taken to be more basic than equality. It is often written as # to distinguish from the negation of equality ≠, which is weaker....
instead of an equivalence relation, called a constructive setoid. One sometimes also considers a partial setoid using a partial equivalence relation
Partial equivalence relation
In mathematics, a partial equivalence relation R on a set X is a relation that is symmetric and transitive...
or partial apartness. (see e.g. Barthe et. al., section 1)
External links
- Implementation of setoids in CoqCoqIn computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...