In Set theories without "junk" theorems? Jacques Carette consider's "junk theorems" of ZFC – theorems which are artifacts of our means of encoding standard mathematical objects into set theory, but don't respect types. For instance, given one encoding of the integers, it is a theorem that the only natural numbers which are functions are 0 and 3.
The examples of junk theorems presented so far all immediately strike you as "junk" – basically there is a type error, and you can immediately recognizer that the junk theorem is the result of mixing types in a way you shouldn't. The theorems are junk, not so much because they are wrong, but because they are not meaningful.
Is it possible for some false and meaningful statement in "normal mathematical language" to be a true statement of ZFC when it is unpackaged?
I am imagining some mundane mathematical question, like is the constant function 3 an element of the zero set of some functional F. Unpackaging the set theoretic definitions of all of the terms involved shows that yes, 3 is a member of that set, but in fact F(3) is not zero. Is this possible?
In other words, should we trust automated theorem provers?
Best Answer
With the constraints you have imposed, the answer is negative. In practice, mathematicians write "normal mathematical statements" in a type theory which is then interpreted into ZFC. Because the interpretation is sound (if something is derivable in type theory then its interpretation is derivable in ZFC) we will never see the sort of phenomenon you are looking for.
Of course, to make my answer a bit more water-tight I would have to explain what the supposed type theory is. I am imaginging something like a dependent type system (with a type universe to distinguish sets and classes, inductive and coinductive types, powertypes, full subset types, etc.) with a first-order classical logic. This would cover most of what mathematicians do.