16
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • $\begingroup$ I am a little bit embarrassed to ask such a question - I would think something so fundamental must be obvious. Somehow, thinking about it I am not so sure. $\endgroup$
    – Steven Gubkin
    Commented Mar 12, 2012 at 23:20
  • 5
    $\begingroup$ Philosophers of mathematics take note: The existence of this question is an important point! (Unless you deem this question nonsensical.) $\endgroup$
    – Alexander Woo
    Commented Mar 12, 2012 at 23:33
  • 2
    $\begingroup$ I don't think you last sentence "should we trust automated theorem provers" is necessarily relevant. They work in their own logic, with their own foundations -- which may or may not be interpretable in ZF(C). I think you trust automated theorem provers, however interpreting what their results means is a lot trickier than it seems. $\endgroup$
    – Jacques Carette
    Commented Mar 12, 2012 at 23:37
  • 2
    $\begingroup$ The only way this could happen, is if the unpacking is not an interpretation. Since interpretations must respect the language they are defined over. $\endgroup$
    – Not Mike
    Commented Mar 12, 2012 at 23:51
  • 1
    $\begingroup$ If you haven't seen it already, here's an example of such a 'junk' statement: us.metamath.org/mpeuni/avril1.html $\endgroup$
    – Charles
    Commented Mar 14, 2012 at 13:18

9 Answers 9

Reset to default
13
$\begingroup$

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.

Improve this answer
$\endgroup$
10
  • $\begingroup$ Great! So these kinds of type differences will never butt head with each other so much that you end up producing false theorems. $\endgroup$
    – Steven Gubkin
    Commented Mar 13, 2012 at 14:23
  • $\begingroup$ Is it still possible that our means of encoding the natural numbers into ZFC allows proofs of some false theorems? I mean say goldbach conjecture turns out to be unprovable in ZFC. Then GC is true, and ZFC + (~GC) is consistent. So ZFC + (~GC) proves a false theorem about the natural numbers. Is it possible that there are some false theorems lurking in ZFC alone, even given its consistency? $\endgroup$
    – Steven Gubkin
    Commented Mar 13, 2012 at 14:27
  • 2
    $\begingroup$ If GC is independent of ZFC then there is no finite counterexample to ZFC (if you can produce a counterexample, that counterexample can be checked in ZFC). If there is no finite counterexample, GC is true. $\endgroup$
    – Steven Gubkin
    Commented Mar 14, 2012 at 4:05
  • 1
    $\begingroup$ I think the comment stream to the answer below is relevant to this discussion: mathoverflow.net/questions/28806/… especially the final comments by Joel David Hamkins and Carl Mummert $\endgroup$
    – Yaakov Baruch
    Commented Mar 14, 2012 at 18:53
  • 1
    $\begingroup$ A better example than Goldbach is Twin Primes. There could be finitely many twin primes and a proof that there are infinitely many without contradiction, or infinitely many twin primes and a proof that there are finitely many without contradiction. Of course, the proofs couldn't be constructive, but a non-constructive proof is entirely possible. $\endgroup$
    – Will Sawin
    Commented Mar 14, 2012 at 19:07
11
$\begingroup$

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.)

Improve this answer
$\endgroup$
10
$\begingroup$

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 :-))

Improve this answer
$\endgroup$
12
  • 1
    $\begingroup$ Your example is an instance of "type mismatch" which I try to disallow in my question. $\endgroup$
    – Steven Gubkin
    Commented Mar 13, 2012 at 2:11
  • 1
    $\begingroup$ OK, but then I don't understand your question. Many mathematicians would understand "$\mathbb{N} \subseteq \mathbb{Z}$" to be a meaningful, well-typed statement. $\endgroup$
    – Tom Leinster
    Commented Mar 13, 2012 at 2:16
  • 3
    $\begingroup$ Many mathematicians would understand it to be meaningful and well-typed (and moreover true), but most (I think) would also be willing to be convinced that it is an abuse of notation (and therefore not well-typed in the strictest sense). Or at least that the $\mathbb{N}$ and $\mathbb{Z}$ that appear in the ZFC theorem $\mathbb{N} \nsubseteq \mathbb{Z}$ are not the same $\mathbb{N}$ and $\mathbb{Z}$ that appear in the true statement $\mathbb{N}$ and $\mathbb{Z}$ (which might be, for example, subsets of $\mathbb{R}$). $\endgroup$
    – Toby Bartels
    Commented Mar 13, 2012 at 6:08
  • 2
    $\begingroup$ I can't edit it now, but two comments ago, the last ‘$\mathbb{N}$ and $\mathbb{Z}$’ should be ‘$\mathbb{N} \subseteq \mathbb{Z}$’. $\endgroup$
    – Toby Bartels
    Commented Mar 13, 2012 at 6:09
  • 2
    $\begingroup$ fedja, I totally agree that many "inclusions" are really embeddings. (I'm a category theorist; I probably tell people this ad nauseam.) The underlying problem here is that what ZFC means by "set" is different from what most mathematicians mean by "set". $\endgroup$
    – Tom Leinster
    Commented Mar 13, 2012 at 13:41
7
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ As someone who meddled in assembler for a few years (including programming, and other related stuff) I can highly relate to that answer! $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 13, 2012 at 8:08
3
$\begingroup$

To Michael Blackmon (in comment on Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up) , 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?

Improve this answer
$\endgroup$
10
  • $\begingroup$ The fact that $\in$ is well-founded. $\endgroup$
    – Not Mike
    Commented Mar 14, 2012 at 22:12
  • $\begingroup$ If ZFC is not $\Sigma_1$-sound then there is no wellfounded model of ZFC. $\endgroup$
    – François G. Dorais
    Commented Mar 15, 2012 at 0:04
  • $\begingroup$ @François, $V_\omega$ is always well-founded. I don't understand $\endgroup$
    – Not Mike
    Commented Mar 15, 2012 at 0:18
  • 1
    $\begingroup$ @Michael: With what model of the natural numbers are you measuring well-foundedness of $V_\omega$ in your model of ZFC? The specific $\omega$ from your model of ZFC, right? $\endgroup$
    – user13113
    Commented Mar 15, 2012 at 0:42
  • $\begingroup$ @Hurkyl, here is my reasoning for why $\omega$ is well-ordered by $\in$ (in what follows I'm going to assume $(\mathbb{N},0,+,\cdot,\le)$ is the standard model of $PA$ produced by Tennenbaums theorem en.wikipedia.org/wiki/Tennenbaum%27s_theorem ): first $\omega \subset V_\omega$, second, the finite levels of $V$, namely $V_{n+1} = \mathcal{P}(V_n)$, with $V_0 = \emptyset$ are finite and hereditarily finite; from theses we can get, for every $\gamma \in \omega$ there is some $n \in \mathbb{N}$ such that $\gamma \in V_n$, which since $V_n$ is hereditarily finite, implies the result. $\endgroup$
    – Not Mike
    Commented Mar 15, 2012 at 1:32
2
$\begingroup$

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.

Improve this answer
$\endgroup$
4
2
$\begingroup$

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?

Improve this answer
$\endgroup$
7
  • $\begingroup$ This is not true under every interpretation, and hence is not a member of the theory. en.wikipedia.org/wiki/… $\endgroup$
    – Not Mike
    Commented Mar 13, 2012 at 2:54
  • 2
    $\begingroup$ Forming the set S is much the same kind of abuse as thinking of N as a subset of Z. You should never form the union of two sets that are not already given as subsets of a fixed ambient set; instead, you should form their disjoint union (which has a couple of common encodings in ZFC). Then of course 3 is not (barring the possibility of mistyped junk) an element of the disjoint union; but when considering whether 3 is a root, you really want to know whether i(3) is an element of the disjoint union (where i and j are the inclusion maps into a disjoint union). And this is true iff 3 is a root. $\endgroup$
    – Toby Bartels
    Commented Mar 13, 2012 at 6:17
  • 4
    $\begingroup$ Compared to the other ingredients of mathematics in practice, I think that disjoint unions get short shrift. People will make complicated circumlocutions like ‘Assume without loss of generality that A and B are disjoint, and consider their union.’ or even ‘Take two disjoint copies of A, and consider their union.’. One would only write this if the term ‘disjoint union’ is not in one's vocabulary. Neither the notation for disjoint union nor the encoding into ZFC are standardised either, further evidence of the concept's obscurity. Yet it is used all over the place. $\endgroup$
    – Toby Bartels
    Commented Mar 13, 2012 at 6:22
  • 1
    $\begingroup$ @Toby: I heartily agree, with one incidental reservation: the fact that the notation for disjoint union isn't standardized isn't evidence for its obscurity, I'd say. There are many important concepts for which notation and terminology aren't standardized. Does $\mathbb{N}$ included $0$? Does a constant function count as "increasing"? Do you write the complement of $B$ in $A$ as $A\setminus B$ or $A - B$? $\endgroup$
    – Tom Leinster
    Commented Mar 13, 2012 at 12:49
  • 2
    $\begingroup$ @Toby I realized that my example was wrong in this way, which is why I said it was "A very contrived example which almost answers my question". Really it was an attempt to try and convey the flavor of an answer. $\endgroup$
    – Steven Gubkin
    Commented Mar 13, 2012 at 14:02
2
$\begingroup$

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:

  1. ZFC is consistent
  2. 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".
  3. 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

Improve this answer
$\endgroup$
12
  • 1
    $\begingroup$ What? This makes no sense. $\endgroup$
    – Not Mike
    Commented Mar 14, 2012 at 12:13
  • 3
    $\begingroup$ Michael Blackmon: Why not? $\endgroup$
    – Steven Landsburg
    Commented Mar 14, 2012 at 15:15
  • $\begingroup$ Ignoring the fact that the conjunction of 1, 2, and 3 can never happen. Goldbach's conjecture is the statement: $\forall n \in \mathbb{N}\ \exists p,q \le n\ ( 2 n = p + q$ and $p,q$ are prime$).$ In order for this statement to be independent of $PA$ (or $ZFC$) you must be able to produce a pair of models of $PA$; one model must affirm Goldbach's conjecture, and the other must refute Goldbach's conjecture. $\endgroup$
    – Not Mike
    Commented Mar 14, 2012 at 16:17
  • 1
    $\begingroup$ The categoricity argument doesn't actually rule out non-standard elements. It's true that ZFC can characterize the natural numbers up to isomorphism: given any model $M$ of ZFC, any two sets in $M$ satisfying second-order PA will have an isomorphism between them in $M$. However, $M$ might not include any set containing just the standard natural numbers. (For example, if $M$ is a model of ZFC plus the negation of Con(ZFC), then $M$ won't contain any standard model of PA.) It's even possible that no model of ZFC contains the standard model of PA, in which case ZFC is $\omega$-inconsistent. $\endgroup$
    – Henry Cohn
    Commented Mar 15, 2012 at 1:09
  • 1
    $\begingroup$ This is related to the overspill lemma in the study of non-standard models of PA. The key is that there's no definition of "standard" in the first-order language of set theory. Looking at a given model of ZFC from the outside, we may be able to tell that its natural numbers include some non-standard numbers. Inside the theory, we can't express this and will never notice it. $\endgroup$
    – Henry Cohn
    Commented Mar 15, 2012 at 1:17
1
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .