nLab structural ZFC

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Contents

Idea

In this article we introduce a structural set theory consisting of four basic primitives, sets, elements, functions, and relations, as well as function evaluation, and relation holding, and structural versions of 9 of the 10 axioms of ZFC presented in the nLab article of ZFC, making the set theory equivalent in strength to ZFC. We propose that structural ZFC is a suitable theory for practical foundations, as the primitives and axioms are in alignment with the usage of such objects in mathematical practice, rather than coming with its own additional baggage.

 Presentation

We work in a first-order logic with equality. In structural ZFC, there are four basic primitives:

  • sets AA

  • for every set AA, elements aAa \in A (the membership \in here is a typing judgment, rather than a relation)

  • for every set AA and BB, functions f:ABf:A \to B with domain AA and codomain BB (the function notation f:ABf:A \to B here is a judgment, rather than a relation)

  • for every set AA and BB, relations φ:AB\varphi:A \looparrowright B with domain AA and codomain BB (the relation notation φ:AB\varphi:A \looparrowright B here is a judgment, rather than a relation)

In addition,

  • for every function f:ABf:A \to B and element aAa \in A, one could form the element f(a)Bf(a) \in B; this operation is called function evaluation,
  • for every relation φ:AB\varphi:A \looparrowright B and element aAa \in A and bBb \in B, one could form that φ(a,b)\varphi(a, b) holds of aa and bb.

The axioms of structural ZFC are as follows:

Axiom 0A (Axiom of equality preservation): For all sets AA and BB, functions f:ABf:A \to B, and elements aAa \in A and bAb \in A, if a=ba = b, then f(a)=f(b)f(a) = f(b).

Axiom 0B (Axiom of unique choice): For all functions f:ABf:A \to B, there is a unique relation φ:AB\varphi:A \looparrowright B such that for all aAa \in A, φ(a,f(a))\varphi(a, f(a)) holds of aa and f(a)f(a), and for all relations φ:AB\varphi:A \looparrowright B such that for all aAa \in A, there is a unique bBb \in B such that φ(a,b)\varphi(a, b) holds of aa and bb, there is a function f:ABf:A \to B such that f(a)=bf(a) = b.

A function f:ABf:A \to B is an injection if for all elements aAa \in A and bAb \in A, a=ba = b if and only if f(a)=f(b)f(a) = f(b). Injections are written as f:ABf:A \hookrightarrow B.

Axiom 1 (Axiom of strong extensionality): Given sets AA and BB and an injection i:ABi:A \hookrightarrow B, the following statements are logically equivalent to each other:

  • there exists a function i 1:BAi^{-1}:B \to A such that for all elements aAa \in A and bBb \in B, i 1(i(a))=ai^{-1}(i(a)) = a and i(i 1(b))=bi(i^{-1}(b)) = b
  • for every element xBx \in B there exists an element yAy \in A such that i(y)=xi(y) = x

One uses the axiom of strong extensionality as the definition of a bijection between sets.

Axiom 2 (Axiom of empty set): There exists a set \emptyset such that for every other set AA, there is a unique relation u A :Au_A^\emptyset:\emptyset \looparrowright A.

Axiom 3 (Axiom of Cartesian products): For every set AA and BB, there exists a set A×BA \times B with a function π A:A×BA\pi_A:A \times B \to A and a function π B:A×BB\pi_B:A \times B \to B such that for every element aAa \in A and bBb \in B there is a unique element (a,b)A×B(a, b) \in A \times B, such that π A((a,b))=a\pi_A((a, b)) = a and π B((a,b))=b\pi_B((a, b)) = b.

Given a set II, an II-indexed family of subsets is a relation M:IAM:I \looparrowright A to a set AA called the union of MM.

Axiom 4 (Axiom of indexed subsets): For every set II and II-indexed family of subsets M:IAM:I \looparrowright A with union AA, and for every element iIi \in I, there exists a set M iM_i and an injection m:M iAm:M_i \hookrightarrow A, such that for every element aM ia \in M_i, M(i,m(a))M(i, m(a)) holds for ii and m(a)m(a), and for every other set BB with injection f:BAf:B \hookrightarrow A such that for every element bBb \in B, M(i,f(b))M(i, f(b)) holds for ii and f(b)f(b), there is a unique function u B M i:BM iu_B^{M_i}:B \to M_i such that for every element bBb \in B, f(b)=m(u B M i(b))f(b) = m(u_B^{M_i}(b)).

Axiom 5 (Axiom schema of separation): For any set BB and any formula ϕ(x)\phi(x) with free variable xBx \in B, there exists a set {B|ϕ}\{B \vert \phi\} with an injection m:{B|ϕ}Bm:\{B \vert \phi\} \hookrightarrow B such that for every element xBx \in B, ϕ(x)\phi(x) holds if and only if there exists an element y{B|ϕ}y \in \{B \vert \phi\} such that m(y)=xm(y) = x.

Axiom 6 (Axiom schema of collection): For any set AA and formula ϕ(x,X)\phi(x, X) with free variables xAx \in A and XX, there exists a set BB, function p:BAp:B \to A, and a BB-indexed family of sets M:BCM:B \looparrowright C with union CC, such that for every bBb \in B, ϕ(p(b),M b)\phi(p(b), M_b), and for every aAa \in A, if there exists a set XX with ϕ(a,X)\phi(a, X), then aim(p)a \in \mathrm{im}(p).

Axiom 7 (Axiom of power sets): For any set AA, there exists a set 𝒫(A)\mathcal{P}(A) and a relation () A():A𝒫(A)(-)\in_A(-):A\looparrowright \mathcal{P}(A) such that for any set BB with injection i:BAi:B \hookrightarrow A, there exists a unique b𝒫(A)b \in \mathcal{P}(A) such that for any xAx \in A, x Abx \in_A b holds of xx and bb if and only if there exists an element yBy \in B such that i(y)=xi(y) = x.

Axiom 8 (Axiom of natural numbers): There exists a set \mathbb{N} with an element 00 \in \mathbb{N} and a function s:s:\mathbb{N} \to \mathbb{N}, such that for all sets AA with an element 0 A:A0_A:A and function s A:AAs_A:A \to A, there is a unique function u A :Au_A^\mathbb{N}:\mathbb{N} \to A such that u A (0)=0 Au_A^\mathbb{N}(0) = 0_A and for all elements nn \in \mathbb{N}, u A (s(n))=s A(u A (n))u_A^\mathbb{N}(s(n)) = s_A(u_A^\mathbb{N}(n)).

Axiom 9 (Axiom of choice): If f:ABf:A \to B is a function such that for every element xBx \in B there exists an element yAy \in A such that f(y)=xf(y) = x, then there is a function g:BAg:B \to A such that for all elements xBx \in B, f(g(x))=xf(g(x)) = x.

The structural version of the axiom of foundation, the axiom of well-founded materialization, states that every set can be embedded in some well-founded extensional graph. This axiom follows from the axiom of choice, and well-founded extensional graphs are not a fundamental concept in structural set theory, so it is not listed here as a separate axiom.

Making alternate primitive choices

One could choose to make either the relations or the functions a derived object of the other, leading to categorical ZFC and allegorical ZFC respectively.

Dependently-sorted categorical ZFC

Categorical ZFC follows ETCS with elements in taking functions to be fundamental and relations as defined.

We work in a first-order logic with equality. In structural ZFC, there are three basic primitives:

  • sets AA

  • for every set AA, elements aAa \in A (the membership \in here is a typing judgment, rather than a relation)

  • for every set AA and BB, functions f:ABf:A \to B with domain AA and codomain BB (the function notation f:ABf:A \to B here is a judgment, rather than a relation)

In addition, for every function f:ABf:A \to B and element aAa \in A, one could form the element f(a)Bf(a) \in B; this operation is called function evaluation. A relation between sets AA and BB is a set RR with an injection (s,t):RA×B(s, t):R \hookrightarrow A \times B.

 Three-sorted categorical ZFC

An alternate formulation of categorical ZFC three sorts, one for sets, elements, and functions, making structural ZFC into a three-sorted set theory. The membership aAa \in A becomes a relation between the sort of elements and the sort of sets, while the functional domain and codomain notation f:ABf:A \to B also becomes a ternary relation between the sort of functions, and two copies of the sort of sets. There is a quinary relation eval(A,B,f,a,b)\mathrm{eval}(A, B, f, a, b) between all three sorts, which says that given sets AA and BB, the function ff can be evaluated at element aa and the result of the evaluation is the element bb, in the context of φ:AB\varphi:A \looparrowright B, aAa \in A, and bBb \in B.

Dependently sorted allegorical ZFC

Allegorical ZFC follows SEAR in taking relations to be fundamental and functions as defined.

We work in a first-order logic with equality. In structural ZFC, there are three basic primitives:

  • sets AA

  • for every set AA, elements aAa \in A (the membership \in here is a typing judgment, rather than a relation)

  • for every set AA and BB, relations φ:AB\varphi:A \looparrowright B with domain AA and codomain BB (the relation notation φ:AB\varphi:A \looparrowright B here is a judgment, rather than a relation)

In addition, for every relation φ:AB\varphi:A \looparrowright B and element aAa \in A, one could form the judgment that φ(a,b)\varphi(a, b) holds. A function is a relation φ:AB\varphi:A \looparrowright B such that for all aAa \in A, there is a unique element bBb \in B such that φ(a,b)\varphi(a, b) holds, and bb is said to be the evaluation of aa at φ\varphi.

Three-sorted allegorical ZFC

An alternate formulation of allegorical ZFC uses three sorts, one for sets, elements, and relations, making SEAR into a three-sorted set theory. The membership aAa \in A becomes a relation between the sort of elements and the sort of sets, while the relational domain and codomain notation φ:AB\varphi:A \looparrowright B also becomes a ternary relation between the sort of relations, and two copies of the sort of sets. There is a quinary relation holds(A,B,φ,a,b)\mathrm{holds}(A, B, \varphi, a, b) between all three sorts, which says that given sets AA and BB, the relation φ\varphi holds for element aa and bb in the context of φ:AB\varphi:A \looparrowright B, aAa \in A, and bBb \in B.

 See also

 References

The axiom of well-founded materialization, the structural axiom of extensionality (the strong terminal generator condition of well-pointedness), and the structural axiom schemata of separation and collection could be found in:

The rest of the axioms are standard axioms from categorical set theory (or the type theoretic equivalent).

Last revised on November 20, 2022 at 02:06:54. See the history of this page for a list of all contributions to it.