$ \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 with Lang, Serge. "Basic Mathematics" (p.40, exercise 10). I will prove one of the lemmas present in the exercise using Fitch-style natural deduction system.
Lemma 1: Every positive integer can be written in one of the forms $3k$, $3k+1$, $3k+2$ for some integer $k$.
Proof of Lemma 1:
$ \fitch{1.\, \forall x \forall y((x \in \mathbb{Z} \land y \in \mathbb{Z} \land x > 0 \land y > 0) \to \exists! q \exists! r(x = qy+r \land 0 \leq r < y)) \\ 2.\,(3 \in \mathbb{Z} \land 3 > 0)}{ \fitch{3.\, a \in \mathbb{Z} \land a > 0}{ 4.\,\forall y((a \in \mathbb{Z} \land y \in \mathbb{Z} \land a > 0 \land y > 0) \to \exists! q \exists! r(a = qy+r \land 0 \leq r < y)) \Ae{1} 5.\, (a \in \mathbb{Z} \land 3 \in \mathbb{Z} \land a > 0 \land 3 > 0) \to \exists! q \exists! r(a = 3q+r \land 0 \leq r < 3) \Ae{4} 6.\,a \in \mathbb{Z} \land a > 0 \land 3 \in \mathbb{Z} \land 3 > 0 \ci{3,2} 7.\,\exists! q \exists! r(a = 3q+r \land 0 \leq r < 3) \ie{5,6} 8.\,\exists q(\exists! r(a = 3q+r \land 0 \leq r < 3) \land \forall q'(\exists! r(a = 3q'+r \land 0 \leq r < 3) \to q=q')) \qquad \text{Abbreviation}\\ \fitch{9.\, \exists! r(a = 3k+r \land 0 \leq r < 3) \land \forall q'(\exists! r(a = 3q'+r \land 0 \leq r < 3) \to k=q')}{ 10.\,\exists r((a = 3k+r \land 0 \leq r < 3) \land \forall r'((a=3k+r' \land 0 \leq r' < 3) \to r=r') \land \forall q'(\exists! r(a = 3q'+r \land 0 \leq r < 3) \to k=q') \qquad \text{Abbreviation}\\ \fitch{11.\, (a = 3k+s \land 0 \leq s < 3) \land \forall r'((a=3k+r' \land 0 \leq r' < 3) \to s=r') \land \forall q'(\exists! r(a = 3q'+r \land 0 \leq r < 3) \to k=q')}{ 12.\,a=3k+s \land 0\leq s<3 \ce{11} 13.\,0\leq s<3 \ce{12} 14.\,s=0 \lor (s=1 \lor s=2) \qquad \text{Abbreviation}\\ 15.\,a=3k+s \ce{12} \fitch{16.\, s=0}{ 17.\,a=3k \qe{16,15} 18.\,a=3k \lor (a=3k+1 \lor a=3k+2) \oi{17} }\\ \fitch{19.\, s=1 \lor s=2}{ \fitch{20.\, s=1}{ 21.\,a=3k+1 \qe{19,15} 22.\,a=3k \lor (a=3k+1 \lor a=3k+2) \oi{21} }\\ \fitch{23.\, s=2}{ 24.\,a=3k+2 \qe{23,15} 25.\,a=3k \lor (a=3k+1 \lor a=3k+2) \oi{24} }\\ 26.\,a=3k \lor (a=3k+1 \lor a=3k+2) \oe{19,20-22,23-25} }\\ 27.\,a=3k \lor (a=3k+1 \lor a=3k+2) \oe{14,16-18,19-26} }\\ 28.\,a=3k \lor (a=3k+1 \lor a=3k+2) \Ee{10,11-27} 29.\,\exists y(a=3y \lor (a=3y+1 \lor a=3y+2)) \Ei{28} }\\ 30.\,\exists y(a=3y \lor (a=3y+1 \lor a=3y+2)) \Ee{9,10-29} }\\ 31.\,(a \in \mathbb{Z} \land a > 0) \to \exists y(a=3y \lor (a=3y+1 \lor a=3y+2)) \ii{3-30} 32.\,\forall x((x \in \mathbb{Z} \land x > 0) \to \exists y(x=3y \lor (x=3y+1 \lor x=3y+2))) \Ai{31} } $
Does it correctly show this proposition holds ?
Is the conclusion a disjunction of three statements ? Is my usage of Existential Introduction appropriate in order to accomplish the end goal ?