1
$\begingroup$

$ \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.

$\endgroup$
4
  • $\begingroup$ 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 $\endgroup$ Jun 11, 2020 at 23:24
  • $\begingroup$ You're right. I am going to edit it. $\endgroup$
    – F. Zer
    Jun 11, 2020 at 23:27
  • $\begingroup$ @Graham Kemp, I set $3a=4-c$ in order to avoid division. What do you think ? $\endgroup$
    – F. Zer
    Jun 11, 2020 at 23:56
  • $\begingroup$ As you said, there was no guarantee that $(4-c)/3 \in \mathbb{Z}$. $\endgroup$
    – F. Zer
    Jun 11, 2020 at 23:56

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you so much, @Graham Kemp ! I really appreciate your precise explanation. I edited the proof. Do you think it is good, now ? Would you change anything ? $\endgroup$
    – F. Zer
    Jun 11, 2020 at 23:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .