Well formed formulas and functions in set theory

Question

In set theory, a function $f:A \to B$ is defined as a subset $f \subseteq A \times B$ such that $$\forall x \in A(\exists!y \in B((x,y)\in f)).$$ Consider the example $f:\mathbf{R} \to \mathbf{R}, x \mapsto 2x^2+3$ which is just an arbitrarily chosen example. To show that this is a function, one has to show that $f$ defines a set that satisfies the property above. As far as I know, sets in set theory are always of the form $$\{a \ | \ \text{some property of a}\}.$$ Hence I think one can write $f$ as $$\{z \ | \ \exists x(\exists y(x \in \mathbf{R} \wedge y \in \mathbf{R} \wedge y=2x^2+3 \wedge z=(x,y)))\}$$ is this correct? Could one also express this as $$\{z \ | \ \exists x(x \in \mathbf{R}) \wedge \exists y(y \in \mathbf{R} \wedge y=2x^2+3) \wedge z=(x,y)\}?$$ If this is the case, I should not be able to write it as a set by "commuting" the introduction of $x$ and $y$, since $y$ depends on $x$, right? What I mean by that can be seen here: $$\{z \ | \ \exists y(y \in \mathbf{R} \wedge y=2x^2+3) \wedge \exists x(x \in \mathbf{R}) \wedge z=(x,y)\}?$$ Since $y$ depends on $x$ it seems weird to me if this would be possible.

Since I try to formalize things in my spare time (I am just starting) I wondered how the statement $$\forall x \in X \forall y \in Y \forall z \in Y(((x,y) \in R \wedge (x,z) \in R) \implies y=z)$$ can be formalized, where $X,Y$ denote some sets and $R \subseteq X \times Y$ denotes a relation. I know that well formed formulas allow for the part "$\forall x \in X \forall y \in Y \forall z \in Y$" followed by a formula. However, I am not sure how to express an according formula. This statement can be found in https://en.wikipedia.org/wiki/Function_(mathematics).

Answer 1

Not a complete answer.

Firstly, it is not generally true that $\{ a \mid \text{some property of } a \}$ is a set: what if the property is $a \not\in a$? If then $b = \{ a \mid a \not\in a \}$ then is $b \in b$ true? This is called Russell’s paradox. What is true (in some axiomatisations of set theory, for instance ZF) is that if $c$ is a set then $\{ a \in c \mid \text{some property of } a \}$ is a set (this is called the axiom of separation, or comprehension).

Your first formalisation of the set describing the function $f \colon x \mapsto 2x^2 + 3$ is correct; the second one is not. The quantifier $\exists x$ only binds instances of $x$ in the next “rank” of the formula: $\exists x (\varphi(x))$ is fine, but $\exists x(\varphi(x)) \land \psi(x)$ is not; the instance of $x$ in $\psi(x)$ is free, i.e. not bound. In fact, since variables can be relabelled, the formulas $$\exists x(\varphi(x)) \land \psi(x)$$ and $$\exists x(\varphi(x)) \land \psi(t)$$ are logically equivalent.

I am not certain what you mean by “formalising” that last statement; it is, after all, already expressed in the formal language. I’ll update this once OP clarifies.

Answer 2

A long comment:

In set theory, a function $f:A \to B$ is defined as a subset $f\subseteq A \times B$ such that $\forall x \in A(\exists!y \in B((x,y)\in f))$

Another commonly used definition of a function in mathematics:

Suppose $A$, $B$ and $G$ are sets such that

1. $G\subset A\times B $
2. $\forall x\in A: \exists!y\in B: (x,y)\in G$

Then we can define a function $f$ such that

$\forall x,y: [x\in A \land y\in B \implies [y=f(x) \iff (x,y)\in G]] $

Here, $G$ is called the graph of $f$.

This form of the definition has the advantage that it cannot be applied for elements outside the domain $(A)$ of the function $f$ here. For those elements, we say that $f$ is undefined.

Why is this important? Consider the reciprocal function on the real numbers. We need to distinguish between, for example, $1/2=3$ being false and the truth value of $1/ 0 =3$ being undefined on the real numbers. The definition of the reciprocal function on the reals simply cannot be used to determine its truth value of $1/0=3$ since $0$ is not in its domain.