Aksjomatyczna teoria mnogości jest oparta o rachunek predykatów posługujący się jedynym symbolem predykatowym. Symbol ten jest dwuargumentowy i oznaczamy go przez
\( \in \)
Predykat ten jest najczęściej interpretowany w modelu jako symbol przynależności do zbioru. Zbiór, który jest wartością zmiennej po lewej stronie symbolu jest elementem zbioru, który jest wartością zmiennej występującej po prawej.
Dla ułatwienia posługiwania się formalizmem związanym z aksjomatyczną teorią mnogości używamy wielu skrótów pozwalających na bardziej zwięzłe zapisywanie formuł. Często używany symbol \( \notin \) jest skrótem mówiącym, że dwa elementy nie są ze sobą w relacji \( \in \), to znaczy
\( x \notin y \stackrel{\textrm{def}}{\equiv} \lnot x\in y. \)
Kolejny skrót oznaczamy przez \( = \) i definiujemy go w następujący sposób,
\( x = y \stackrel{\textrm{def}}{\equiv} \forall z ( z\in x\iff z\in y). \)
Zgodnie z intuicją wyniesioną z naiwnej teorii zbiorów skrót ten definiuje dwa zbiory jako równe, jeśli dla każdego wartościowania zmiennej \( z \) element jest w zbiorze \( x \) wtedy i tylko wtedy, kiedy jest w zbiorze \( y \). Nieformalnie, dwa zbiory są równe jeśli posiadają dokładnie te same elementy. W naszym języku nie mamy możliwości zdefiniowania pojedynczego bytu w modelu, gdyż nie mamy wpływu na to, jak interpretowane są predykaty. Będziemy mówić, że zbiór posiadający daną cechę jest unikalny, jeśli wszystkie zbiory posiadające tą cechę są równe.
Podobnie do równości jesteśmy w stanie zdefiniować zawieranie, czyli inkluzji zbiorów
\( x \subset y \stackrel{\textrm{def}}{\equiv} \forall z ( z\in x \Longrightarrow z\in y). \)
Inkluzja ta spełnia własności, które pochodzą z naiwnej teorii mnogości. Przede wszystkim, dwa zbiory są sobie równe wtedy i tylko wtedy, kiedy jeden jest podzbiorem drugiego, a drugi pierwszego.
Fakt 2.1.
Następująca formuła jest prawdziwa w aksjomatycznej teorii mnogości
\( \forall x \forall y ( x = y \iff x\subset y \land y\subset x). \)
Dowód
Zastępując skróty przez odpowiadające im napisy, otrzymujemy:
\( \forall x \forall y [ \forall z ( z\in x\iff z\in y) \iff \forall z ( z\in x \Longrightarrow z\in y)\land \forall z ( z\in y \Longrightarrow z\in x)]. \)
Używając podstawowych własności rachunku predykatów, otrzymujemy:
\( \forall x \forall y [\forall z ( z\in x\iff z\in y) \iff \forall z ( (z\in x \Longrightarrow z\in y)\land ( z\in y \Longrightarrow z\in x))] \)
i dalej
\( \forall x \forall y [\forall z ( z\in x\iff z\in y) \iff \forall z (z\in x\iff z\in y)], \)
co jest tautologią rachunku predykatów.
W bardzo podobny sposób możemy pokazać, że
\( \forall x \forall y \forall z (x\subset y \land y\subset z ) \Longrightarrow x\subset z. \)
Czyli, że zawieranie zbiorów zdefiniowane w rachunku predykatów jest przechodnie.