Here is a how a typical proof might look like in group theory--- Suppose we are given a finite group $G$. Enumerate the elements $g\_1, \dots, g\_n$. Now consider a formula $\phi(g\_1, \dots, g\_n)$ which discusses some property of $G$....


This proof is not rigorous. In any set theory I can think of, a finite set is equinumerous to $\{0, \dots, n}$ where $n$ may be a non-standard integer. So when we are proving things about finite sets, we really should allow the size of the set to be non-standard. But, at least implicitly, any proof assumes that $n$ is a standard integer.


This seems to be different than proofs of arithmetic, in which we can assume that the computations are occurring in the true structure of $\mathbf N$, which contains only standard integers. We may need extra axioms to pin down the behavior of $\mathbf N$, but we ultimately will never need the non-standard integers.


EDIT: I think I have boiled down this issue to the the following example.


We will prove that $CON(ZFC) \vdash (ZFC \vdash CON(ZFC))$, which is obviously false.


Consider the following proof. Suppose CON(ZFC) is true. Given a model $M$ of ZFC and $n$ an integer of $M$. If $n$ is a standard integer, then by assumption $n$ is not a proof of contradiction of ZFC. So we have shown that for all standard integers $n$ and all models $M$ of ZFC, $n \in M$ does not disprove ZFC. Hence, by the transfer principle, ZFC proves that all integers $n$ are not disproofs of ZFC. Hence ZFC proves CON(ZFC).


The key issue is that some formulas *do* behave differently for standard and non-standard formulas. In this case, the formula "$x$ is a disproof of ZFC" is a formula which picks out the non-standard integers.



Why do we ignore non-standard finite sets in ordinary mathematics?
You are right, a lot of published proofs are non-rigorous in something like the sense you describe. See this answer and the comments attached to it:


[Why is it so difficult to write complete (computer verifiable) proofs?](https://mathoverflow.net/questions/24220/why-is-it-so-difficult-to-write-complete-computer-verifiable-proofs/56021#56021)


I remember chasing down some of the references from that post and finding them interesting too.
The Bundy et paper is here: <http://www.jstor.org/pss/30039733> (link courtesy of schropp on reddit).


