mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...

, a setoid (''X'', ~) is a

set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...

(or type) ''X'' equipped with an

equivalence relation In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation. Each equivalence relatio ...

~. A setoid may also be called E-set,

Bishop A bishop is an ordained clergy member who is entrusted with a position of authority and oversight in a religious institution. In Christianity, bishops are normally responsible for the governance of dioceses. The role or office of bishop is ...

set, or extensional set. Setoids are studied especially in

proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding part ...

and in type-theoretic

foundations of mathematics Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathe ...

. Often in mathematics, when one defines an equivalence relation on a set, one immediately forms the

quotient set In mathematics, when the elements of some set S have a notion of equivalence (formalized as an equivalence relation), then one may naturally split the set S into equivalence classes. These equivalence classes are constructed so that elements a ...

(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 In any of several fields of study that treat the use of signs — for example, in linguistics, logic, mathematics, semantics, semiotics, and philosophy of language — an intension is any property or quality connoted by a word, phrase, or ano ...

al equality (the equality on the original set) and extensional equality (the equivalence relation, or the equality on the quotient set).

Proof theory

In proof theory, particularly the proof theory of constructive mathematics based on the

Curry–Howard correspondence In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct rela ...

, one often identifies a mathematical

proposition In logic and linguistics, a proposition is the meaning of a declarative sentence. In philosophy, " meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same meaning. Equivalently, a proposition is the no ...

with its set of

proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a c ...

s (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 In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...

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.

Type theory

In type-theoretic foundations of mathematics, setoids may be used in a type theory that lacks

quotient type In type theory, a kind of foundation of mathematics, a quotient type is an algebraic data type that represents a type whose equality relation has been redefined by a given equivalence relation such that the elements of the type are partitioned ...

s to model general mathematical sets. For example, in Per Martin-Löf's

intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...

, there is no type of

real number In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...

s, only a type of regular Cauchy sequences of

rational number In mathematics, a rational number is a number that can be expressed as the quotient or fraction of two integers, a numerator and a non-zero denominator . For example, is a rational number, as is every integer (e.g. ). The set of all ra ...

s. To do

real analysis In mathematics, the branch of real analysis studies the behavior of real numbers, sequences and series of real numbers, and real functions. Some particular properties of real-valued sequences and functions that real analysis studies include conv ...

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 In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...

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".

Constructive mathematics

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 In mathematics, a partial equivalence relation (often abbreviated as PER, in older literature also called restricted equivalence relation) is a homogeneous binary relation that is symmetric and transitive. If the relation is also reflexive, the ...

or partial apartness. (see e.g. Barthe ''et al.'', section 1)

Notes

References

*. *.

External links