I first want to issue my own interpretation of the proof that $\sqrt{2}$ is irrational.
First, for the sake of contradiction, let's assume it is in fact rational. This means we can write $\sqrt{2} = \frac{a}{b}$ where $\gcd(a,b)=1$ for integers $a,b$ with $b \neq 0$. Then $2b^2 = a^2$ which means $a^2$ is even, which also implies $a$ itself is even. So let $a=2k$ for some integer $k$. Then $2b^2 = (2k)^2 = 4k^2$, or $b^2 = 2k^2$. This means $b^2$ is even, and that $b$ is even too. But if $a$ anad $b$ are both even, then $\gcd(a,b) \neq 1$, a contradiction. Therefore $\sqrt{2}$ is irrational.
Now, I am curious logically where all of these statements fall and what proves what, what contradicts what and implies what, what the premises are, etc. Because I almost feel like there are multiple premises here:
Now technically I don't think the gcd condition is "necessary" for the number to be rational but I don't see where else to put it unless we treat it as another assumption or premise. Or maybe it's a compound premise?
Are we taking two premises:
$p_1 = (\sqrt{2}$ is a rational $\frac{a}{b}$ for integers $a,b$ where $b \neq 0)$
$p_2 = (\gcd(a,b) = 1)$
Then our "main premise" we care to prove:
$p = p_1 \land p_2$
And then from $p$ we use valid operations on $\sqrt{2} = \frac{a}{b}$ and ultimately arrive at a conclusion $q = (\gcd(a,b) \neq 1) = \lnot p_2$.
Since we are saying it is true that $p_2$ and $\lnot p_2$ are true at the same time this already implies a contradiction but I can't help but feel like I've structured this incorrectly.
What exactly are the premises? What are the implications? What are the conclusions? Where is the contradiction and where does it prove that the claim "$\sqrt{2}$ is rational" must be a false premise?
The assumption is merely $p1$: $\sqrt{2}$ is rational, i.e. $\sqrt{2}=\frac{a}{b}$ for some whole numbers $a$ and $b$.
However, we can then point out that if we can write $\sqrt{2}$ as a ratio in some way, then by dividing out the common factors between $a$ and $b$, it follows that we can write it as a ratio where the numerator and denominator have no common factors, i.e. where they are relative prime.
In other words, if $\sqrt{2}=\frac{a}{b}$ for some whole numbers $a$ and $b$, then $\sqrt{2}=\frac{a}{b}$ for some whole numbers $a$ and $b$ where $gcd(a,b) = 1$
You might think that this latter claim is $p1 \land p2$, but that is not correct, since in the expression $p1 \land p2$ the $a$ and $b$ in $p1$ need not be the same $a$ and $b$ in $p2$ ... in fact, in $p1$ the $a$ and $b$ are existentially quantified, whereas in $p2$ they are free variables: So, $p2$ isn't even a 'stand-alone' claim; it only makes sense within the context of $p1$.
In logic: we go from:
$$\exists a,b \in \mathbb{Z} (\sqrt{2} = \frac{a}{b})$$
to:
$$\exists a,b \in \mathbb{Z} (\sqrt{2} = \frac{a}{b} \land gcd(a,b)=1)$$
which is not the same as
$$\exists a,b \in \mathbb{Z} (\sqrt{2} = \frac{a}{b}) \land gcd(a,b)=1$$
This is a crucial thing to note, since the $a$ and $b$ in the claim
$$\sqrt{2}=\frac{a}{b} \text{ for some whole numbers } a \text{ and }b$$
need not be the same $a$ and $b$ in the claim:
$$\sqrt{2}=\frac{a}{b} \text{ for some whole numbers } a \text{ and }b \text{ where } gcd(a,b)=1$$
which is again why you can;t treat $p2$ as a 'stand-alone' claim: are you referring to $a$ and $b$ as stated to exist in the context of the former claim, or in the context of the latter claim? This is not clear, and so you should not treat $p2$ as a claim in and of itself.
As such, you should also not say: "Well, the proof shows that $p1 \land p2$ leads to a contradiction ... but it seems that the only contradiction we reach is that we get $\neg p2$ .. so why should we reject $p1$? Again, there is no such thing as $p1 \land p2$ ... there is $p1$, i.e.:
$$\exists a,b \in \mathbb{Z} (\sqrt{2} = \frac{a}{b})$$
and then there is the claim that follows from $p1$, which is:
$$\exists a,b \in \mathbb{Z} (\sqrt{2} = \frac{a}{b} \land gcd(a,b)=1)$$
and this latter claim is not $p1 \land p2$, but rather the 'integration' of $p1$ and '$p2$', as '$p2$' ends up within the scope of the existential of $p1$. So, we could write this as '$p1 \land p2$', but maybe it's best to just write it as claim $p1'$.
So, we have:
$$p1 \rightarrow \ p1'$$
And then of course we show:
$$p1' \rightarrow \bot$$
And thus:
$$p1 \rightarrow \bot$$
And therefore:
$$\neg p1$$