Statement F. $\ a^n+b^n+c^n=d^n$ has no positive integer solutions $a,b,c,d$ for any $n=3,4,5,...$.
(Please don't comment on whether or not Statement F is true!)
$Suppose$ I proved in the Gödel-sense that Statement F is undecidable in ZFC.
a) Is the following theorem TRUE, and is its proof correct? If it is a valid proof, how can I formalize it in some axiom system? We certainly cannot use ZFC, because Statement F is undecidable (unprovable) in ZFC (our assumption).
Theorem. Statement F is true.
Proof. I plug in a=b=c=d=1, and I don't get equality. I plug in a=b=c=1, d=2, and I don't get equality. I keep going by using an enumeration of $\mathbb{N}^4$. But I don't finish the calculations, because I don't have infinity much time. Instead I ask: can I get ever equality (if I kept going forever)? No, because, if, say, $3^5+4^5+8^5=9^5$, then that would be a proof of Statement F $not$ being true in ZFC, a contradiction. So our Theorem must be true!
b) option 2: if we can formalize the above proof in ZFC, then that means we cannot prove that Statement F is undecidable in ZFC. But then, similarly, we cannot prove that any Diophantine equation is undecidable in ZFC. I have not heard of such result! Did you?
Your argument is correct, and there is no difficulty formalizing it in any axiomatic system such as ZFC. In fact, assuming ZFC is consistent, you cannot prove within ZFC that any statement is undecidable in ZFC, or indeed that there is any statement that ZFC cannot prove. If you could prove that, then you could conclude that ZFC is consistent (since if it were inconsistent, it would prove everything, since anything follows from a contradiction!). So you would have a proof that ZFC is consistent, within ZFC. This is impossible (unless ZFC is inconsistent), by Gödel's second incompleteness theorem.
To be clear, this doesn't mean that there are no Diophantine equations (or other statements) which are undecidable in ZFC. It just means that you can't prove such undecidability in ZFC itself (as opposed to some stronger theory such as ZFC+Con(ZFC)).