Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A setoid or Bishop set whose quotient set is a field.
“Field setoid” and “Bishop field” are placeholder names for a concept which may or may not have another name in the mathematics literature.
Let $R$ be a commutative ring setoid. An element $a \in R$ is invertible if there exists an element $b \in R$ such that $a \cdot b \sim 1$.
A field setoid or Bishop field is a commutative ring setoid $F$ in which for every element $a \in F$, $a$ is invertible if and only if $a \sim 0$ is false.
Similarly to the case for fields, there are different notions for field setoids in constructive mathematics. These include
discrete field setoids
Heyting field setoids
weak Heyting field setoids
Kock field setoids
A discrete field setoid is a commutative ring setoid $F$ in which for every element $a \in F$, either $a \sim 0$ or $a$ is invertible.
A weak Heyting field setoid is a commutative ring setoid $F$ in which for every element $a \in F$, $a$ is not invertible if and only if $a \sim 0$.
A Heyting field setoid is a weak Heyting field setoid which is also a local ring setoid.
Given any Archimedean ordered field $F$, the set of Cauchy sequences in $F$ is a field setoid. In constructive mathematics, the set of Cauchy sequences in $F$ is only a Heyting field setoid.
Given any Archimedean ordered field $F$, the set of all locators of all elements of $F$ is a field setoid. In constructive mathematics, the set of all locators of all elements of $F$ is only a Heyting field setoid.
Last revised on August 19, 2024 at 14:53:48. See the history of this page for a list of all contributions to it.