nLab
reflexive symmetric relation
Context
Relations
Constructivism, Realizability, Computability
Equality and Equivalence
equivalence

equality (definitional , propositional , computational , judgemental , extensional , intensional , decidable )

identity type , equivalence of types , definitional isomorphism

isomorphism , weak equivalence , homotopy equivalence , weak homotopy equivalence , equivalence in an (∞,1)-category

natural equivalence , natural isomorphism

gauge equivalence

Examples.

principle of equivalence

equation

fiber product , pullback

homotopy pullback

Examples.

linear equation , differential equation , ordinary differential equation , critical locus

Euler-Lagrange equation , Einstein equation , wave equation

Schrödinger equation , Knizhnik-Zamolodchikov equation , Maurer-Cartan equation , quantum master equation , Euler-Arnold equation , Fuchsian equation , Fokker-Planck equation , Lax equation

Foundations
foundations

The basis of it all
mathematical logic

deduction system , natural deduction , sequent calculus , lambda-calculus , judgment

type theory , simple type theory , dependent type theory

collection , object , type , term , set , element

equality , judgmental equality , typal equality

universe , size issues

higher-order logic

Set theory
Foundational axioms
Removing axioms
Contents
Definition
An reflexive symmetric relation is a binary relation that is reflexive and symmetric .

Examples
In constructive mathematics
In constructive mathematics, the double negation of equality cannot in general be proven to be an equivalence relation , because the denial inequality cannot be proved to be an apartness relation . Instead, the double negation of equality is only a stable reflexive symmetric relation. Indeed, since excluded middle cannot be proven, we could distinguish between the following reflexive symmetric relations in constructive mathematics:

equality

equivalence relations , a transitive reflexive symmetric relation

double negation of equality

stable reflexive symmetric relation, a reflexive symmetric relation $\approx$ which additionally satisfies $\neg \neg (a \approx b)$ implies $a \approx b$

decidable reflexive symmetric relation, an reflexive symmetric relation $\approx$ which additionally satisfies $(a \approx b)$ or $\neg (a \approx b)$

See also
Created on December 8, 2022 at 20:33:44.
See the history of this page for a list of all contributions to it.