A question about quantifiers

Question

I'm trying to prove this theorem:

Let $F$ and $G$ be functions. Then $F=G$ if and only if $\operatorname{Dom}(F)=\operatorname{Dom}(G)$ and $\forall X (X\in \operatorname{Dom}(F)\rightarrow F(X)=G(X))$.

To prove it I need to justify as much as possible my steps by using rules of logic. So this is what I have for $\Longrightarrow$ (I'm working on the second part but it's pretty much the same). My question is specifically on step number 5. If you have any comment or anything I'll be very grateful:

$1)F=G\Longrightarrow \forall X(X\in F \longleftrightarrow X\in G)$ (Definition of $``="$)

$2)\Longrightarrow \forall X(\exists A \exists B (X=(A,B)\wedge X\in F) \longleftrightarrow X\in G)$ (F is a binary relation)

$3)\Longrightarrow \forall (A,B)(\exists A \exists B ((A,B)\in F \longleftrightarrow (A,B)\in G) $ (Properties of $``="$)

$4)\Longrightarrow \forall (A,B)((A,B)\in F \longleftrightarrow (A,B)\in G)$ (Existential elimination)

$5)\Longrightarrow \forall A\forall B (A\in \operatorname{Dom}(F)\wedge F(A)\in \operatorname{Ran}(F) \longleftrightarrow A\in \operatorname{Dom}(G)\wedge F(A)\in \operatorname{Ran}(G) \wedge F(A)=G(A))$ (???It sounds to me like I can introduce quantifiers but I'm not sure and I don't know how to justify it).

$6)\Longrightarrow \forall A\forall B (A\in \operatorname{Dom}(F)\longleftrightarrow A\in \operatorname{Dom}(G))\wedge \forall A\forall B (A\in \operatorname{Dom}(F) \longrightarrow F(A)=G(A))$

($\wedge$ and $\exists$ property. Also simplification of $\wedge$ and $\longleftrightarrow$ )

$7)\Longrightarrow \operatorname{Dom}(F)=\operatorname{Dom}(G) \wedge\forall A (A\in \operatorname{Dom}(F) \longrightarrow F(A)=G(A))$ ($\forall$ elimination and definition of $``="$).

Answer 1

For completeness' sake, a complete derivation of the theorem in (a form of) natural deduction. We follow the approach set out in this comment.

---

For convenience and explicitness, we introduce a predicate $\mathsf{Func}(F)$, with intended reading "$F$ is a function". That is:

$$\forall F:\mathsf{Func}(F) \leftrightarrow ((\forall X \in F:\exists a,b:X = \langle a,b\rangle )\land (\forall a,b,b': (\langle a,b\rangle \in F\land \langle a,b'\rangle \in F) \to b=b') )$$

We now split out the theorem into two parts, i.e. we prove:

• $\mathsf{Func}(F)\land \mathsf{Func}(G) \to (F = G \leftrightarrow \forall a, b: \langle a,b\rangle \in F \leftrightarrow \langle a,b\rangle \in G)$
• $(\forall a, b: \langle a,b\rangle \in F\leftrightarrow \langle a,b\rangle \in G) \hskip{4em}\leftrightarrow (\mathsf{Dom}(F) = \mathsf{Dom}(G)\land \forall a (a \in \mathsf{Dom}(F) \to F(a) =G(a)))$

---

In the derivations below, the "Pool" indicates the assumptions a certain line depends on.

Part 1: $F = G \to (\forall a, b: \langle a,b\rangle \in F \leftrightarrow \langle a,b\rangle \in G)$

1. $F = G$ (Assumption) (Pool: 1)
2. $\forall X(X \in F \leftrightarrow X \in G)$ (Extensionality) (Pool: 1)
3. $X \in F \leftrightarrow X \in G$ (Universal Instantiation) (Pool: 1)
4. $X = \langle a,b\rangle \to (X \in F \leftrightarrow X \in G)$ (Implication Introduction) (Pool: 1)
5. $\forall a,b: \forall X: X = \langle a,b\rangle \to (X \in F \leftrightarrow X \in G)$ (Universal Generalisation) (Pool: 1)
6. $F = G \to (\forall a, b: \langle a,b\rangle \in F \leftrightarrow \langle a,b\rangle \in G)$ (Implication Introduction)

where in the last derivation, we have used that the formula 5. is the proper form for the consequent.

Part 2: $\mathsf{Func}(F) \to ((\forall a, b: \langle a,b\rangle \in F \to \langle a,b\rangle \in G)\to F \subseteq G)$

1. $Y \in F$ (Assumption) (Pool: 1)
2. $\mathsf{Func}(F)$ (Assumption) (Pool: 2)
3. $\forall X(X \in F \to \exists a,b: X = \langle a,b\rangle)$ (Conjunction Elimination) (Pool: 2)
4. $Y \in F \to \exists a,b: Y = \langle a,b\rangle$ (Universal Instantiation) (Pool: 2)
5. $\exists a,b: Y = \langle a,b\rangle$ (Modus Ponens on 1. and 4.) (Pool: 1,2)
6. $Y = \langle\alpha,\beta\rangle$ (Existential Instantiation) (Pool: 1,2)
7. $\forall a, b: \langle a,b\rangle \in F \to\langle a,b\rangle \in G$ (Assumption) (Pool: 7)
8. $\langle\alpha,\beta\rangle \in F \to \langle\alpha,\beta\rangle \in G$ (Universal Instantiation) (Pool: 7)
9. $Y \in F \to Y \in G$ (Some reasoning in Propositional Calculus) (Pool: 1,2,7)
10. $Y \in G$ (Modus Ponens on 1. and 9.) (Pool: 1,2,7)
11. $Y \in F \to Y \in G$ (Implication Introduction on 1. and 10.) (Pool: 2,7)
12. $F \subseteq G$ (Universal Generalisation, definition of $\subseteq$) (Pool: 2,7)

Two more Universal Generalisations suffice to establish the desired expression; interchanging $F$ and $G$ and combining these with Part 1 yields the first of our bullet points.

Part 3: $(\forall a, b: \langle a,b\rangle \in F\to \langle a,b\rangle \in G)\to (\mathsf{Dom}(F) \subseteq \mathsf{Dom}(G))$

1. $\forall a, b: \langle a,b\rangle \in F\to \langle a,b\rangle \in G$ (Assumption) (Pool: 1)
2. $\exists b: \langle\alpha,b\rangle \in F$ (Assumption) (Pool: 2)
3. $\langle\alpha,\beta\rangle\in F$ (Existential Instantiation) (Pool: 2)
4. $\langle \alpha,\beta\rangle \in F\to \langle \alpha,\beta\rangle \in G$ (Universal Instantiation) (Pool: 1)
5. $\langle \alpha,\beta\rangle \in G$ (Modus Ponens on 3. and 4.) (Pool: 1,2)
6. $\exists b: \langle \alpha,b\rangle \in G$ (Existential Generalisation) (Pool: 1,2)
7. $(\exists b: \langle\alpha,b\rangle \in F) \to (\exists b: \langle\alpha,b\rangle \in G)$ (Implication Introduction) (Pool: 1)
8. $\forall a((\exists b: \langle a,b\rangle \in F) \to (\exists b: \langle a,b\rangle \in G)$ (Universal Generalisation) (Pool: 1)
9. $(\forall a, b: \langle a,b\rangle \in F\to \langle a,b\rangle \in G)\to (\mathsf{Dom}(F) \subseteq \mathsf{Dom}(G))$ (Implication Introduction)

where in the last derivation, we have used that $a \in \mathsf{Dom}(f)$ iff $\exists b: \langle a,b\rangle \in F$; interchanging $F$ and $G$ we establish $(\forall a, b: \langle a,b\rangle \in F\leftrightarrow \langle a,b\rangle \in G)\to (\mathsf{Dom}(F) = \mathsf{Dom}(G))$.

Part 4: $(\forall a, b: \langle a,b\rangle \in F\to \langle a,b\rangle \in G)\to (\forall a: a \in \mathsf{Dom}(F) \to F(a) \subseteq G(a))$

1. $\forall a, b: \langle a,b\rangle \in F\to \langle a,b\rangle \in G$ (Assumption) (Pool: 1)
2. $\forall b: \langle \alpha,b\rangle \in F\to \langle \alpha,b\rangle \in G$ (Universal Instantiation) (Pool: 1)
3. $(\exists b: \langle \alpha,b\rangle \in F) \to (\forall b: \langle \alpha,b\rangle \in F\to \langle \alpha,b\rangle \in G)$ (Implication Introduction) (Pool: 1)
4. $(\forall a, b: \langle a,b\rangle \in F\to \langle a,b\rangle \in G)\to (\forall a: a \in \mathsf{Dom}(F) \to F(a) \subseteq G(a))$ (Implication Introduction)

where we have chosen to interpret $F(a)$ as the set $\{b: \langle a,b\rangle \in F\}$; interchanging $F$ and $G$ and using Part 3, we obtain the desired equality.

---

The above four parts constitute a proof of the two bulleted formulae, which together imply the desired theorem.

The above explicit proof (which still wouldn't be accepted by a formal proof checker) should leave the reader deeply appreciative of proofs written in words, as well as serve as a positive witness to the fact that such proofs can actually be written (because many claim that such is possible, but hardly pursue it to any extent, as it is tedious and -- besides being a good natural deduction proof writing exercise -- not very enlightening).