Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up) - MathOverflow

Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-12T23:19:49Z

In http://mathoverflow.net/questions/90820/set-theories-without-junk-theorems/90882#90882 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?

Answer by Hurkyl for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T00:13:56Z

Does Skolem's paradox fit the kind of thing you were thinking? Of course, this is also a type error; it's just a lot easier to miss.

Answer by Tom Leinster for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T01:52:14Z

I'm not sure I understand the intent behind this question, but here goes: the statement "$\mathbb{N} \not\subseteq \mathbb{Z}$" is true in ZFC (in the sense below) but false in the usual way of understanding things.

When I say "true in ZFC" I'm mirroring Steven's usage of "ZFC", but that's a bit careless. ZFC itself is just an axiom system. It says nothing about how, for instance, you encode natural numbers as sets. But presumably Steven is referring to the standard encoding to be found in traditional set theory books. There (if I remember correctly) you encode an integer as an equivalence class of pairs of natural numbers, and a pair as... etc. etc. To be honest, I haven't checked that $\mathbb{N}$ fails to be a subset of $\mathbb{Z}$ with this encoding, and I'm afraid I can't bring myself to...

But even the best friends of traditional set theory would tell you that the encoding of "everything" as sets is arbitrary. So isn't it simply inevitable (and not at all meaningful) that the answer to the question in the title is "yes"?

(Unless, of course, ZFC is inconsistent, in which case it can't be consistent :-))

Answer by Steven Gubkin for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T02:27:44Z

Here is a very contrived example which almost answers my question:

Say I want to know whether 3 is a root of $x^2-8$. Let $S$ be the set of all roots of $x^2-8$, together with all functions from finite sets to finite sets. I think to myself - if I search through this set and find the number 3, then 3 has to be a root of $x^2-8$, because the only numbers in the set are roots - all the other members of the set are functions. I make a list of all the sets in $S$ written as part of the cumulative hierarchy starting with the empty set, and I find that 3 is an element of this set. So 3 must be a root right?

Now this example was very contrived. In particular I force a type mismatch into the question. I am curious if, given current encoding conventions, situations like this could occur in natural mathematical problems. No one ever actually runs up against these types of problems because no one goes back to raw ZFC, but would we run into these kinds of problems if we did?

Answer by Henry Cohn for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T04:04:15Z

Here's an argument for why the answer is no:

First, let's formulate the question as follows. Is there a meaningful mathematical statement that can be disproved in ordinary mathematical practice but that's a theorem of ZFC under the standard definitions? We need to rule out type mismatches (is $2 \in \pi$?) and abuse of notation (whether $\mathbb{N}$ is actually a subset of $\mathbb{Z}$ or merely canonically isomorphic to a subset of $\mathbb{Z}$), but then there won't be any such statements, of course assuming ZFC is consistent.

The reason is that the ordinary mathematical arguments will have to be based on certain axioms, and the set-theoretic constructions have been designed to satisfy those axioms. For example, you want $\mathbb{N}$ to satisfy the Peano axioms, and indeed ZFC proves that it does. Assuming ZFC is consistent, you therefore can't use the Peano axioms to disprove anything ZFC proves about $\mathbb{N}$.

Similarly, when you construct $\mathbb{R}$ you prove that it's a complete ordered field (i.e., every nonempty subset that is bounded above has a least upper bound). This is enough to do elementary analysis, so our theory isn't going to contradict calculus unless ZFC is inconsistent.

In practice, when people build up mathematics within set theory, there are only two gaps in what they care about. First, there's the behavior of $\in$: ZFC assumes everything is a set, so you always have the potential for unexpected things to be elements of each other, but this is the type mismatch issue and is easily ignored. (You might worry that what if, for example, these sentences have consequences that conflict with the Peano axioms? Then ZFC would be inconsistent, since it can prove the Peano axioms.) Second, there's the abuse of notation. The von Neumann definition of $\mathbb{N}$ is beautiful and pleasant to use, but it's not literally going to be a subset of most other constructions. If you want to be super careful, you should either harmonize all your constructions or explicitly write out inclusion maps, but a little sloppiness does no harm.

The argument I've just outlined really isn't a mathematical theorem, because we haven't defined ordinary mathematical reasoning (ZFC is the closest thing we have to a definition, but that would make this whole argument vacuous). However, it's still true in a philosophical sense.

What it comes down to is that the $\mathbb{N}$ vs. $\mathbb{Z}$ abuse of notation is harmless, and that incorrectly typed statements are never used in ordinary mathematics. (If people proved everyday theorems using $2 \not\in \pi$ as an axiom, then we would have to worry about whether that axiom was compatible with our set-theoretic constructions. However, as long as ZFC is consistent, including incorrectly typed statements together with the usual axioms cannot cause problems.)

Answer by Andrej Bauer for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T05:57:02Z

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.

Answer by abo for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T06:54:29Z

The phenomenon of junk theorems - and the example you cite - are present in a small fragment of ZFC (without the Axiom of Infinity, replacement, choice, ...) which can be modeled by PA, which I presume you accept is consistent. This does not, of course, imply that adding in these deleted axioms might not then cause an inconsistency, just that I don't think you could say it's because of the junk theorems.

Answer by Victor Dods for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T07:21:08Z

I'd like to back Andrej's answer, and add an analogy which will hopefully be useful.

Generating theorems from the ZF(C) axioms using formal logic is analogous to programming a computer in machine code or assembler -- you're just shoveling integers around inside the CPU, which doesn't care how you interpret them. Doing raw set theory has no bearing on the higher level interpretation of the sets (as numbers, functions, etc.).

One of the functions of a high[er]-level computer programming language is to account for how you interpret the data being processed. Types are introduced so that only operations that are intrinsically meaningful will be allowed. For example, multiplying a fraction by a string of ASCII characters is meaningless and prohibited until it is explicitly defined. Under the hood, the fraction and the string are both just integers, which the CPU can operate on. The result depends on the representation and therefore is not intrinsically meaningful.

The expression $2 \in \pi$ is well-defined within raw set theory, but its truth value depends on the representations of the sets $2$ and $\pi$, and is therefore not intrinsically meaningful.

The type theory mentioned by Andrej is the analog to the computer language compiler, and provides the setting for determining if expressions are meaningful.

So my answer to the question would be "yes, we can trust automatic theorem provers", so long as we recognize that they are proving low-level statements about raw sets.

Answer by none for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-13T21:12:51Z

It's conceivable that ZFC is consistent but plain wrong (i.e. arithmetically unsound, even $\Sigma_1$-unsound). I think Nik Weaver believes this to be a real possibility.[1] E.g. we could have the following situation:

ZFC is consistent
ZFC proves the negation of Goldbach's conjecture, i.e. it proves "there exists an even n that is not the sum of two primes".
There is actually no such n.

If Goldbach's conjecture is independent of Peano arithmetic, then all three of the numbered statements above could hold simultaneously, without PA being unsound.

[1] http://www.math.wustl.edu/~nweaver/indisp.pdf

Answer by none for Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)

2012-03-14T18:36:25Z

To Michael Blackmon (in comment on http://mathoverflow.net/questions/91034/can-zfc-prove-false-theorems-and-still-be-consistent-was-junk-theorems-fol/91120#91120 , sorry I don't have the cookie to add a new comment to that post, maybe someone with enough points can transfer this):

Yes, the idea is that if there are two models of PA (one that affirms Goldbach's conjecture and one that refutes it), it's conceivable that ZFC disproves Goldbach's conjecture even though the conjecture is true in the standard integers. That just means that the $\omega$ in every model of ZFC turns out to be nonstandard, i.e. ZFC itself is unsound (though still consistent) and proves theorems that are false for the standard integers. This seems like an unlikely situation, but I don't see how it's nonsensical. Am I missing something?