# Show the set $\{(x,y) \in \mathbb{Z} \times \mathbb{Z} : 3x+y=4\}$ is a function from $\mathbb{Z}$ to $\mathbb{Z}$.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\}$$

Working on the book: Richard Hammack. "Book of Proof" (p. 239)

Exercise 7. Consider the set $$f = \{(x,y) \in \mathbb{Z} \times \mathbb{Z} : 3x+y=4\}$$. Is this a function from $$\mathbb{Z}$$ to $$\mathbb{Z}$$? Explain.

I define $$f(x)=4-3x$$, and use an abbreviation for the uniqueness quantifier in line 21.

Proof that $$f(x)=4-3x$$ is indeed a function:

$$\fitch{ 1.\,\forall x\forall y((x \in \mathbb{Z} \land y \in \mathbb{Z}) \to x+y \in \mathbb{Z}) \qquad \textit{Addition is closed on \mathbb{Z}}\\ 2.\,\forall x\forall y((x \in \mathbb{Z} \land y \in \mathbb{Z}) \to xy \in \mathbb{Z}) \qquad \textit{Multiplication is closed on \mathbb{Z}}\\ 3.\,(-3) \in \mathbb{Z}\\ 4.\,4 \in \mathbb{Z} }{ \fitch{5.\, a \in \mathbb{Z}}{ 6.\,(-3) \in \mathbb{Z} \land a \in \mathbb{Z} \ci{3,5} 7.\,(-3 \in \mathbb{Z} \land a \in \mathbb{Z}) \to (-3)a \in \mathbb{Z}\Ae{2} 8.\,-3a \in \mathbb{Z} \ie{7,6} 9.\,4 \in \mathbb{Z} \land -3a \in \mathbb{Z} \ci{4,8} 10.\,(4 \in \mathbb{Z} \land (-3a) \in \mathbb{Z}) \to (4-3a) \in \mathbb{Z}\Ae{1} 11.\,4-3a \in \mathbb{Z} \ie{10,9} 12.\,3a+(4-3a)=4 \qi{} \fitch{12.\, c \in \mathbb{Z} \land 3a+c=4}{ 13.\,3a+c=4 \ce{12} 14.\,3a=4-c \qquad \textit{Arithmetic}\\ 15.\,4-3a=4-3a \qi{} 16.\,4-3a=4-(4-c)=c \qe{14,15} 17.\,4-3a=c }\\ 18.\,(c \in \mathbb{Z} \land 3a+c=4) \to 4-3a=c \ii{12-17} 19.\, \forall z(z \in \mathbb{Z} \land 3a+z=4) \to 4-3a=z)\Ai{18} 20.\,4-3a \in \mathbb{Z} \land 3a+(4-3a)=4 \ci{11,12} 21.\,(4-3a \in \mathbb{Z} \land 3a+(4-3a)=4) \land \forall z(z \in \mathbb{Z} \land 3a+z=4) \to 4-3a=z) \ci{20,19} 22.\,\exists y((y \in \mathbb{Z} \land 3a+y=4) \land \forall z(z \in \mathbb{Z} \land 3a+z=4) \to y=z)) \Ei{19} 23.\,\exists! y(y \in \mathbb{Z} \land 3a+y=4)) }\\ 24.\,a \in \mathbb{Z} \to \exists! y(y \in \mathbb{Z} \land y=f(a)) \ii{5-23} 25.\,\forall x(x \in \mathbb{Z} \to \exists! y(y \in \mathbb{Z} \land y=f(x)) \Ai{24} }$$

• Is this a valid proof?
• In particular, do lines 12-15 properly show uniqueness ?

EDIT: I modified the proof to take into account the excellent advise I received. Deleted premise 0 where I assumed $$f$$ was a function.

• Don't use division; $\Bbb Z$ is not closed under division so there is no immediate guarantee that $(4-c)/3$ will be an integer Jun 11, 2020 at 23:24
• You're right. I am going to edit it. Jun 11, 2020 at 23:27
• @Graham Kemp, I set $3a=4-c$ in order to avoid division. What do you think ? Jun 11, 2020 at 23:56
• As you said, there was no guarantee that $(4-c)/3 \in \mathbb{Z}$. Jun 11, 2020 at 23:56

Every inference is valid, however the premise on line 0 basically says "$$f$$ is a function ...", which was to be proven.
You need to derive $$\forall x\,(\exists y\,(3x+y=4\wedge\forall z\,(3x+z=4\to z=y))$$ without relying on such a premise.