nLab simply sorted set theory

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

 Overview

Simply sorted set theory is a set theory which is a first order theory without dependent sorts; i.e. written in first order logic and whose domains of discourse (called sorts here) do not on other domains of discourse. In addition, membership aAa \in A is a relation, rather than a judgment as in dependently sorted set theory. Simply sorted set theories come in both material set theories and structural set theories.

Simply sorted set theory could be distinguished between how many sorts the theory has; these include

Notions of sets and elements

Definition

A notion of set and element in a simply sorted first-order theory consists of:

  • A sort SS of probable sets. By probable set, we mean that certain terms of SS are to be considered as the sets in the theory.

  • A sort EE of probable elements. By probable element, we mean that certain terms of EE are to be considered as the elements in the theory.

  • A binary predicate in SS, ()= S()(-)=_S(-), called definitional equality of sets

  • A binary predicate in EE, ()= E()(-)=_E(-), called equality of elements

  • A unary predicate in SS, set()\mathrm{set}(-), called being a set

  • A unary predicate in EE, element()\mathrm{element}(-), called being an element

  • A binary predicate in EE on the left and SS on the right, ()()(-)\in(-), called membership

such that

  • ()= E()(-)=_E(-) is an equivalence relation

  • if aba \in b, then aa is an element and bb is a set

a:E.b:S.(ab)element(a)set(b)\forall a:E.\forall b:S.(a \in b) \to \mathrm{element}(a) \wedge \mathrm{set}(b)
  • weak extensionality for sets and elements: for all a:Sa:S and for all b:Sb:S, if a and b are sets, then a= Sba =_S b if and only if, for all c:Ec:E, if cc is an element, then cac \in a if and only if cbc \in b
a:S.b:S.(set(a)set(b))((a= Sb)c:E.(element(c)((ca)(cb))))\forall a:S.\forall b:S.(\mathrm{set}(a) \wedge \mathrm{set}(b)) \implies ((a =_S b) \iff \forall c:E.(\mathrm{element}(c) \implies ((c \in a) \iff (c \in b))))

In one-sorted set theory, the sorts EE and SS are the same sort.

 See also

Last revised on November 19, 2022 at 20:38:17. See the history of this page for a list of all contributions to it.