0
$\begingroup$

Suppose a logical function which takes a set and an element and iteratively tells wether $x$ is inside or not. It is defined as

$$f(S,x)\iff x\in S \bigvee_{A\in S}f(A,x)$$

But how do I define its domain? It is clear what it takes, a set and an element, so it should be something like $f:S'\times X\to \mathbb{B}$ where $S'$ is the set of all sets(?) and $X$ the set of all elements(?). Clearly, these sets does not exist in ZFC, but the function yes, and I really need to define its domain. How can I do it?

I thought about $(S,x)\mapsto b$, but useful info gets hidden, which I dont want.

$\endgroup$
0
$\begingroup$

Rather than "logical functions," it's better to just think of formulas. You have a formula here of two variables. That said, if you really want to think of it as a function, it's a class function like the "function" $x\mapsto \{x\}$, and its domain is a proper class (namely, the whole set-theoretic universe).

As a side note, it's more succinct to say "$f(x, S)\iff x\in tcl(S)$" (where "$tcl$" denotes the transitive closure).

$\endgroup$
0
$\begingroup$

Letting $V$ denote the type of all sets, the domain of $f$ would be the type $V \times V$.

Note in ZFC there is no distinction between "set" and "thing which can be an element".

$\endgroup$
  • $\begingroup$ I would say "class," rather than "type," since the latter isn't used very often in the set theory literature. $\endgroup$ – Noah Schweber Sep 28 '17 at 22:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.