How do you prove the finite axiom of choice? The theorem is that given a finite number of non-empty sets, there exists a finite choice function from the collection of those sets to an element from each set.
If you ask a mathematician you might get something like the following “proof”. Let F = {X1, …, Xn}. Each Xi is nonempty so let xi be some element from Xi for each i. Now we can define the required choice function as f = {〈X1, x1〉, …, 〈Xn,xn〉}.
This proof seems fine, and maybe many or most mathematicians would find this proof acceptable; However, it isn’t really correct. The problem is that the above is actually a proof schema and it only establishes the theorem for sets that can be written as term with a finite number of variables as opposed to all sets that are equipollent to some initial segment of ω.
More specifically, the step from F is finite to there exists some X1, …, Xn such that F = {X1, …, Xn} is not a valid logical deduction. There is no formula in first order logic that even lets you state ∃n:ℕ.∃X1.…∃Xn.…. Even if there were such a formula, it wouldn’t be sound deduction. The problem is that there are (and must be) models of set theory where ω contains non-standard natural numbers. The above proof does not establish the theorem for so-called finite sets of non-standard size for models of set theory with non standard natural numbers.
Essentially, the problem comes down to a confusion between theory and meta-theory. The proof above applies induction in the meta-theory and establishes an infinite number of proofs of specific finite versions of the original problem, rather than applying induction from the theory.
Why isn’t this problem recognized in mathematics? There are several reasons for this. Firstly, the error is very subtle. In fact, if you are not a logician, you might not even be convinced by the above there is actually a problem. Secondly, the theorems being claimed in these situations are typically provable. Therefore, even if the proofs given, such as the one above, are wrong, it won’t cause any harm to continue using the theorems. Thirdly, I believe such erroneous proofs establish the theorem for all the standard natural numbers, and since we are usually only interested in what is true for the standard model of natural numbers, in some sense the proof is actually adequate.
Given this third point, is there really a problem when mathematicians do induction in the meta-theory instead of the actual theory? Or is it the logicians problem for not adequately capturing the type of valid reasoning that comes naturally to mathematicians? Or, mostly likely of all, is what is going on here even more subtle than I realize?
This issue came up in response to “Why is it so difficult to write complete (computer verifiable) proofs?”. schropp pointed out this problem makes it difficult to translate paper proofs to (proper) computer verified proofs. Carl Mummert produced the finite axiom of choice example.