Talk:Axiom of choice.html

Mathematics portal

This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.

Mathematics rating:

B Class

Top Priority

Field: Foundations, logic, and set theory

Please update this rating as the article progresses, or if the rating is inaccurate. Click to show/hide comments.
Please add to or update the comments to suggest improvements to the article.
For comment, see below. CMummert 20:08, 6 October 2006 (UTC)

Archives
Aug 2004 – Sep 2004 Sep 2004 – June 2006 Ben's archive July 2006 — April 2007

1 GCH implies AC??
- 1.1 Another try
2 What is (G)CH really?
3 Implicit usage before 1900
4 What is the problem?
5 For those of us that are advanced at english, and still don't understand...
6 Minor change which reverses current sense
7 On New Theorems
- 7.1 Speed up of proofs using AxCh?
8 Logical independence
9 4th Paragraph of Usage
10 2nd paragraph of Usage: it's not induction, is it?
11 Nonconstructive aspects

GCH implies AC??

I never quite understood this claim. As I understand it, subtly implied in the usual statement of GCH is that every cardinal is one of the Alephs, hence AC, but couldn't one rephrase it to capture the intended meaning without this unintended consequence? It would seem preferable if it were indeed possible. Leberquesgue 19:02, 15 May 2007 (UTC)

The statement is that if for no infinite cardinal $κ$ does a cardinal $κ < λ < 2 κ$ exist, then the axiom of choice holds. The proof is not very simple. The result was proved by A. Lindenbaum and A. Tarski in 1926, but their proof was lost. Sierpinski found a new proof in 1943, and published it in 1947. Kope 06:25, 16 May 2007 (UTC)

Consider $\kappa = \aleph_\alpha$ . Ordered pairs of ordinals less than kappa can be encoded as ordinals less than kappa. So well-orderings of kappa can be encoded as subsets of kappa. The set of all such subsets of kappa (which can be given an ordering of order type $\aleph_{\alpha+1}$ ) is a subset of the powerset of kappa. Thus $\kappa < \aleph_{\alpha+1} \leq 2^\kappa$ . If GCH holds, then it cannot be strictly between them, so we get that $\aleph_{\alpha+1} = 2^\kappa$ . Using transfinite induction, we can show that every infinite cardinal is an aleph. Thus every set can be well-ordered. Thus the axiom of choice holds. JRSpriggs 07:06, 16 May 2007 (UTC) I forgot the equivalence classes of well-orderings. This shows why these things are not so easy without reviewers. JRSpriggs 07:13, 16 May 2007 (UTC)

I would like to add that in Kope's formulation, κ is not necessarily well-orderable, hence not necessarily an aleph. In other words, "cardinal" is meant as "cardinality" (equivalence class of equipotent sets) and not "initial ordinal". --Aleph4 08:47, 16 May 2007 (UTC)

Yes, but in the inductive proof one could assume that all cardinals up to kappa had been shown to be well-orderable. The problem then being to show that its powerset (and thus any subset thereof) is also well-orderable. JRSpriggs 10:43, 16 May 2007 (UTC)

This may be obsolete, due to the line-outs, but that the cardinals are partially-well-ordered by < also requires a form of the axiom of choice, which seems to be the complete transfinite induction you're attempting. (As has been noted, the cardinally being linearly ordered is a form of choice.) — Arthur Rubin | (talk) 15:50, 16 May 2007 (UTC)

I think you mean "well-founded partial order". ZF certainly does not imply that the cardinalities (I prefer this name to "cardinals" in the absence of choice) are well-founded. Indeed, it is consistent with ZF that there is a strictly decreasing ω-sequence of cardinalities. (Start with the cardinality of any infinite Dedekind-finite set.) --Aleph4 17:01, 16 May 2007 (UTC)

PWO is sometimes used for that concept I believe, but you're correct, that's what I meant. Sorry about not checking for the proper notation. — Arthur Rubin | (talk) 18:34, 16 May 2007 (UTC)

JR's induction is almost right, but instead of doing the induction on κ you need to do it on ranks. Suppose that V_α can be wellordered; call its cardinality κ. Then if 2^κ is an aleph, it follows that V_α+1 can be wellordered. I don't see any obvious way of making it work at limit steps (you can't pick a wellordering of V_α for each α<λ) but this would at least get you that every set of rank less than ω×2 can be wellordered. --Trovatore 19:11, 16 May 2007 (UTC)

Trovatore is quite right.

Clearly, I was mistaken in thinking that I could come up with a proof off of the top of my head. JRSpriggs 03:58, 17 May 2007 (UTC)

My mother's book Set Theory for the Mathematician has Sierpinski's proof. Basically, without the axiom of choice, it can be shown that (the symbols m will denote cardinals ≥ ℵ₀, and p will denote arbitrary cardinals, and often confusing sets with their cardinalities), that

(Property P) 2^m-m = 2^m.

(that is, if m + p = 2^m, then p = 2^m, and that, writing ℵ(m) as the least aleph not less than or equal to m, that

$\alefsym(\mathbf m) \leq 2^{2^{2^{\mathbf m}}}$

Then, looking at where $2^{2^{\mathbf m}} + \alefsym(\mathbf m)$ , $2^{\mathbf m} + \alefsym(\mathbf m)$ , and $\mathbf m + \alefsym(\mathbf m)$ may fall, we end up with $\alefsym(\mathbf m)$ being a repeated powerset of m, so that m is clearly an aleph, or the contradiction that $\alefsym(\mathbf m)\leq \mathbf m$ .

— Arthur Rubin | (talk) 15:13, 17 May 2007 (UTC)

Two small correction's:

Trovatore's proof sketch will not show that GCH implies AC: Rather, it is the beginning of the proof of "If the power set of every well-ordered set (or ordinal) can be well-ordered, then AC holds". (I think this is an exercise in Kunen's book, and may well be due to Sierpinski.) At limit steps, a fixed well-ordering of the power set of "everything so far" has to be used.

Arthur Rubin probably means "infinite cardinals" rather than "cardinals ≥ ℵ₀". These two are not equivalent in ZF.

--Aleph4 14:33, 18 May 2007 (UTC)

Actually, I'm afraid I did mean "cardinals ≥ ℵ₀". Property P may fail if m is Dedekind finite, and certainly if 2^m is (Dedekind finite). On the other hand, the form of GCH as specified in the reference also assumed m ≥ ℵ₀, so that may be the reason. What's needed is the following statement:

GCH implies (p < 2^q implies p ≤ q),

where q is an arbitrary infinite cardinal. On the other hand, the "standard" version of GCH implies there are no infinite Dedekind finite cardinals, as p < p + 1 < 2^p, so the proof can continue normally. Sorry about that. I'm afraid the confusion is due to my mother's choice of notation and definition of GCH. — Arthur Rubin | (talk) 14:49, 18 May 2007 (UTC)

Responding to Aleph4: That of course depends on what you mean by GCH in a non-AC context. Since the weakest version you can come up with actually implies full AC, it's kind of moot, but ignoring that, a reasonable interpretation would be 2^κ=κ⁺ for every wellordered cardinal κ. (I absolutely do take the position that, in the absence of AC, the natural thing to call the continuum hypothesis is $2^{\aleph_0}=\aleph_1$ -- the weaker claim that there's no intermediate cardinality between $\aleph_0$ and $2^{\aleph_0}$ should have another name, perhaps "weak CH").

There is an issue I'm not sure how to resolve here. If the powerset of any ordinal can be wellordered, does AC in fact follow (say, in ZF alone)? I don't see how to do the limit case, in the simple induction I proposed. --Trovatore 19:57, 18 May 2007 (UTC)

Yes. I don't have access to my parents' books Equivalents of the Axiom of Choice or my mother's Consequences of the Axiom of Choice at the moment, but Set Theory for the Mathemtician has a proof in NBG that if the power set of any (initial) ordinal can be wellordered, then AC.

The trick is two-fold. (See von Neumann universe for notation.) Fix a V_α which you wish to find a well-ordering of. Fix $\lambda = \{\gamma | \gamma \preccurlyeq V_\alpha\}$ , and find a well-ordering of $\mathbf P(\lambda)$ . Then, prove by transfinite recursion, that there is a function F such that, for each β ≤ α, F(β) well-orders V_β.

(The construction used in that book is $V_\alpha := \mathbf P \left (\bigcup_{\beta< \alpha} V_\alpha \right )$ , rather than the one from von Neumann universe, but it's close enough.)

Another try

With the benefit of Arthur Rubin's outline of Sierpinski's proof, I would like to try again. Let S be any set which we want to show is well-orderable. Let $T = \mathcal{P}(\mathcal{P}(S \cup \omega))$ , then S can be injected into T by the singleton of the singleton of an element of S. Notice that $\| S \cup \omega \| = \| S \cup \omega \| + 1$ and thus $\| \mathcal{P}(S \cup \omega ) \| = \| \mathcal{P}(S \cup \omega ) \| \cdot 2$ and thus $\| T \| = \| T \| \cdot \| T \|$ . Any powerset of a set with these three properties will also possess them. Let α be the smallest ordinal which cannot be injected into T. Ordered pairs of elements of T can be encoded as elements of T using $\| T \| = \| T \| \cdot \| T \|$ . Well orderings of T may be encoded as elements of $\mathcal{P}(T)$ . Equivalence classes (wrt order isomorphism) of such well orderings can be encoded as elements of $\mathcal{P}(\mathcal{P}(T))$ . The elements of α can be mapped injectively to the equivalence classes, so α is injected into $\mathcal{P}(\mathcal{P}(T)).$ $\mathcal{P}(T)$ is also injected into $\mathcal{P}(\mathcal{P}(T))$ . So using $\| \mathcal{P}(\mathcal{P}(T)) \| = \| \mathcal{P}(\mathcal{P}(T)) \| + \| \mathcal{P}(\mathcal{P}(T)) \|$ , we get the disjoint union (sum) of them injected into it. Since this disjoint union is larger or equal to the infinite set $\mathcal{P}(T)$ and smaller than or equal to its powerset, we get that it must equal one or the other of them by GCH.

If it equals $\mathcal{P}(\mathcal{P}(T))$ , then consider an injective function from $\mathcal{P}(\mathcal{P}(T)) \times \mathcal{P}(\mathcal{P}(T))$ through $\mathcal{P}(\mathcal{P}(T))$ to the disjoint union. Using a variation of Cantor's diagonal argument, we can show that there must be a subset of $\mathcal{P}(T)$ such that no elements in the column corresponding to it are mapped into $\mathcal{P}(T)$ itself. Thus they must all be mapped injectively into the image of α. Thus that column (a copy of $\mathcal{P}(\mathcal{P}(T))$ ) is equipollent to α. Thus S is injected into a set equivalent to an ordinal and is thus well-orderable.

If it equals $\mathcal{P}(T)$ instead, then we combine α with T. Using the fact that α cannot be injected into T and a similar argument to that in the previous paragraph, we get that $\mathcal{P}(T)$ can be mapped injectively into α and thus again S is well-orderable. JRSpriggs 05:34, 19 May 2007 (UTC)

Simpler than the proof in my mother's book, at least considering it from "first principles". — Arthur Rubin | (talk) 16:49, 19 May 2007 (UTC)

Thank you for your kind words, Arthur. If anyone has any questions about or criticisms of my proof or would like some part of it expanded in more detail, please speak up. It appears to me now that I did not have to make the image of α and the image of $\mathcal{P}(T)$ disjoint, a simple union would have been sufficient. I was thinking of the outline which calls for a sum, but neither GCH nor the variation of Cantor's diagonal argument need that. JRSpriggs 08:16, 21 May 2007 (UTC)

What is (G)CH really?

Perhaps this should really be moved to the CH discussion page?

Responding to Trovatore (above), who says that CH (in the absence of AC) should be $2^{\aleph_0}=\aleph_1$ :

In my opinion, the "natural" definition of CH (over ZF) should be the statement that there is no set of intermediate cardinality between N and R. I can claim that Georg Cantor agrees with me (although I think it was not he who came up with the name "continuum hypothesis"). In his 1878 paper he asks

in how many classes can the linear manifolds [he means: infinite subset of the real line] be divided, if manifolds of the same cardinality are put into the same class...

and later he claims that some kind of induction suggests that there are exactly two such classes. This is exactly the continuum hypothesis. At that time it was still unclear if the real line can be well-ordered, but I think that aleph1 might have been known already.

Aleph4 14:12, 21 May 2007 (UTC)

Probably should be moved to the CH discussion page, and although I've done some work in the field, I'm not really sure whether CH should be

$2^{\aleph_0}=\aleph_1$

$(\not \exists \mathrm m) \aleph_0 < \mathrm m < 2^{\aleph_0}$

They're not the necessarily the same, in the absence of choice. — Arthur Rubin | (talk) 21:38, 21 May 2007 (UTC)

~~Under ZF~~

~~$(\lnot\exists\;\mathrm m) \aleph_0 < \mathrm m < \aleph_1 \le 2^{\aleph_0}$~~

~~so certainly the former implies the latter.~~

CRGreathouse (t | c) 13:51, 23 May 2007 (UTC)

I'm afraid ZF does not imply $\aleph_1 \le 2^{\aleph_0}$ It implies there is a map from $\mathcal P (\omega \times \omega)$ onto

ω 1

(namely, taking any well-ordering to its order type), but chosing representatives requies some form of choice. — Arthur Rubin | (talk) 14:00, 23 May 2007 (UTC)

So what do I have wrong under ZF?

1. Definition of aleph numbers (successor): $(\lnot\exists\;\mathrm m) \aleph_0 < \mathrm m < \aleph_1$

2. Definition of aleph numbers (order): $\aleph_0 < \aleph_1$

3. Cantor's theorem: $\aleph_0 < 2^{\aleph_0}$

Are you saying $\aleph_1 > 2^{\aleph_0}$ is consistent under ZF, or just that $\aleph_1 \not< 2^{\aleph_0} \wedge \aleph_1 \ne 2^{\aleph_0} \wedge \aleph_1 \not< 2^{\aleph_0}$ is?

CRGreathouse (t | c) 14:35, 23 May 2007 (UTC)

The latter. Remember that trichotomy (of < on cardinal numbers) is equivalent to the axiom of choice, as noted back in the article. — Arthur Rubin | (talk) 14:41, 23 May 2007 (UTC)

I do recall that. Does that mean I can say $(\lnot\exists\;\mathrm m) \aleph_0 < \mathrm m < \aleph_1 \not> 2^{\aleph_0}$ under ZF?

CRGreathouse (t | c) 21:11, 23 May 2007 (UTC)

Yes, ZF implies your statement. But $\not>$ is not a very useful notion.

Comment to Arthur Rubin: In your statement about trichotomy I would suggest the name "cardinal" or even better "cardinality" instead of "cardinal number", because "cardinal number" suggests (to me) an ordinal. --Aleph4 09:20, 24 May 2007 (UTC)

You can say that $\aleph_1 \le 2^{2^{\aleph_0}}$ even without AC (as in my proof above) by mapping each countable ordinal to the equivalence class of well-orderings of ω which have its order type. Where ordered pairs of natural numbers are encoded as natural numbers in some standard way. JRSpriggs 07:18, 24 May 2007 (UTC)

In a remarkable theorem Shelah proved that if $\aleph_1\leq 2^{\aleph_0}$ then there is a non-measurable (under the Lebesgue measure) set of reals. So, in every model where all sets are measurable (as Solovay's) $\aleph_1\not\leq 2^{\aleph_0}$ surely holds. Kope 09:51, 14 June 2007 (UTC)

Implicit usage before 1900

I agree with the motive behind Carl's reversion, but the wording is problematic. Before Zermelo, there was no axiomatic system available to "notice" that it didn't prove certain things if you didn't assume AC. (Well, there was Frege's, but it was wrong, and anyway it was after 1900.) So there are two problems, first, what does the claim even mean? and second, why single out AC, as opposed to, say, replacement or powerset? --Trovatore 07:13, 24 June 2007 (UTC)

I think that one reason to single out AC was that the others were recognized as necessary when the 'complete' axiomatic frameworks were written, but many mathematicians thought they didn't need to assume AC (when in fact they did). CRGreathouse (t | c) 18:40, 24 June 2007 (UTC)

Well, that's a historical point from a period later than the one in question, so I don't see how it's relevant. And it still doesn't address the question of what the claim means. --Trovatore 20:15, 24 June 2007 (UTC)

Perhaps the point which needs to be made is that people are often less conscious of using the axiom of choice than they are of using the other axioms. Even people who overtly deny it often make inferences which cannot be validly formalized with invoking the axiom of choice. JRSpriggs 07:28, 25 June 2007 (UTC)

Ya think? Less conscious than they are of using replacement? No, seriously, I think the existing wording is a problem. That's why I didn't restore it when the anon took it out, even though his edit summary looked like nonsense. --Trovatore 09:36, 25 June 2007 (UTC)

Yes, I think so. In my case I was aware of an axiomatic framework and most of the axioms I was using, but would still use the AoC without realizing that I was. But that's beside the point. I'm really a WP:0RR editor, so I'll leave the article as-is.

CRGreathouse (t | c) 12:56, 26 June 2007 (UTC)

I reverted mainly because the claim is very commonly made and because the edit summary was confusing. One fix would be to give an explicit reference for the claim. I'm away from home for a while, though. — Carl (CBM · talk) 14:15, 26 June 2007 (UTC)

What is the problem?

“

First we might try to proceed as if X were finite. If we try to choose an element from each set, then, because X is infinite, our choice procedure will never come to an end, and consequently, we will never be able to produce a choice function for all of X.

”

The statement claims that human brain can alway choose an element from any given set. It is real function of choice. --Javalenok 18:27, 18 July 2007 (UTC)

“

Next we might try the trick of specifying the least element from each set. But some subsets of the real numbers don't have least elements. For example, the open interval (0,1) does not have a least element.

”

Any non-empty interval (a, b) has a middle element (a+b)/2. The infinite interval (a, +inf) has an (a+1) element. --Javalenok 18:27, 18 July 2007 (UTC)

Yes, we don't need the axiom of choice to pick an element from an open interval of R, we can just use the midpoint. But some sets don't include their midpoints -- or don't even have a well-defined notion of 'midpoint'. That's when we need the axiom of choice.

CRGreathouse (t | c) 19:46, 18 July 2007 (UTC)

For those of us that are advanced at english, and still don't understand...

"exactly one object from each bin can be picked and gathered in another bin".
This seems very poorly worded. What on earth is it talking about.
Imagine a collection/set of bins, each containing at least one object. The theorem states that "...exactly one object, from each bin, can be picked" - what do you mean "picked"? As in "Picked up?" Or as in "Selected?"
So let's assume it means selected.

"...and gathered" - what do you mean "gathered?" Do you mean that ALL of these objects that have been picked are gathered somewhere, like in one big pile or something? Or are we only talking about gathering 1 object, in one place, which is hardly gathering at all. "...in another bin" - do you mean one ultimate bin, where everything has been gathered? Or is it like swapping a bit, where an object is picked, and put into some other random bin, and then another object is picked elsewhere, and put into another completely different bin?

I really wish you could elaborate a bit more. This axiom makes no sense.

Rfwoolf 20:53, 19 August 2007 (UTC)

I suggest changing

"be picked and gathered in another bin"

"be selected from and placed into one collecting bin"

--Michael C. Price ^talk 22:14, 19 August 2007 (UTC)

I've never been a fan of physical analogies for AC. It's easy to pick balls out of bins - just reach in and grab one from each bin. AC is about functions that simultaneously select a member from each of a collection of nonempty sets. I can't reach my hand into a set. — Carl (CBM · talk) 22:41, 19 August 2007 (UTC)

simultaneously select? There's nothing in the intuitive description that contradicts this. --Michael C. Price ^talk 23:09, 19 August 2007 (UTC)

Agreed, but I'm not convinced the analogy with bins conveys any useful intuition either. — Carl (CBM · talk) 01:28, 20 August 2007 (UTC)

Hmm, well, it does to me. I'd go so far as to say it makes it clear why AC is true. --Trovatore 03:29, 20 August 2007 (UTC)

What about the specific wording I've suggested? Rfwoolf, does it help? --Michael C. Price ^talk 06:57, 20 August 2007 (UTC)

One other point about thw wording: perhaps we should change

"given a collection "

"given any collection "

--Michael C. Price ^talk 07:18, 21 August 2007 (UTC)

Minor change which reverses current sense

I have deleted the word "not" from the April fool's quote about the axiom of choice. Yes, it reverses the sense, but also makes sense out of non-sense. If anyone feels I am out of order, please revert. Kiwi137 (talk) —Preceding comment was added at 14:13, 21 November 2007 (UTC)

I've reverted your edit. It's a direct quote, and should be word-for-word identical with the original: editing direct quotes, even if it improves on their meaning, renders them invalid. -- The Anome (talk) 14:17, 21 November 2007 (UTC)

On New Theorems

The reason people accept some new axioms, like inaccessible cardinals, is that there are new theorems you can prove with inaccessibles that you can't prove without them. The theorems I am talking about are not abstract existence theorems that talk about enormous sets, although some of the theorems you prove with inaccessible cardinals are certainly of this sort. The theorems I am talking about are statements that can be stated in a verifiable way--- they assert that certain computations do not halt. In logic, they are sometimes called "Real Theorems"(standard terminology), to distiguish them from "Fake theorems"(nonstandard terminology), which are abstract assertions that can't be checked by computing anything.

Using inaccessible cardinals, there are computer programs that can be shown not to halt, which cannot be shown not to halt without inaccessibles. The classic example is the program that deduces all consequences of ZFC, looking for a contradiction. This program does not halt if ZFC is consistent, and the weakest inaccessible cardinal axioms prove that ZFC is consistent, and not much else.

The point of strong axioms is that they prove new real theorems, new theorems about computer programs, so generally when people say axiom system A is stronger than axiom system B, or axiom system A proves more theorems than B, they mean this--- there is a program X that B proves not to halt, which A does not.

The question then arises: is the axiom of choice such an axiom? Does it let you prove new theorems about computations, or is it just an assertion about the abstract existence of certain infinite sets? The proof of equiconsistency shows that AC is of the latter type.

If you prove program X does not halt in ZFC and if the program halts, ZFC is inconsistent. But equiconsistency implies then that ZF is inconsistent, which means that there is a proof in ZF that X does not halt.

Equiconsistency is proven in ZF (you can do it in PA), so ZF actually proves the theorem ZFC proves X does not halt implies ZF proves X does not halt. Godel's proof allows this statement to be made into an algorithm--- given a proof that X does not halt in ZFC, there is a textual manipulation of this proof into a proof that X does not halt in ZF. This is proven in Cohen's "Set Theory and the Continuum Hypothesis", for one. It is neither deep nor controversial.

So to say that the axiom of choice proves new theorems, without also saying that it does not prove any new real theorems, is to my mind a gross mischaracterization. It leaves people with the feeling that there are theorems about the outcome of actual computations whose proof is made possible by the axiom of choice, which is just not true. This is why I inserted a balanced discussion contrasting the elegence of the theorems proved with choice, against their essentially unverifiable content.Likebox (talk) 19:43, 15 January 2008 (UTC)

To say that a theorem which doesn't describe computations is "unreal" is — well, I can't think of an appropriate term. If you want to say something about this, in general, under, say equiconsistency, go right ahead. I probably won't even notice. Perhaps it might have one claus, here, but it clearly doesn't deserve a full sentence. As for the rest of your additions, they refer to the opinions of living mathematicians, so require a source. —Preceding unsigned comment added by Arthur Rubin (talk • contribs) 19:52, 15 January 2008 (UTC)

I don't see how the reference to computer programs is particularly relevant to an article about the axiom of choice. There's no good reason I can see for this article to discuss them, since they are not at all an object of study in elementary set theory such as Levy covers in his book Basic Set Theory.

The independence proof is due to Fraenkel (for ZF with urelements) or Cohen (for ZF). Goedel showed that AC is consistent with ZF, but not that it is independent of ZF (and Cohen beat him to that proof). — Carl (CBM · talk) 19:57, 15 January 2008 (UTC)

The point is that it is standard terminology in logic to call theorems "unreal" when they do not assert the halting of computer programs. The reason you mention computer programs is because you want to take into consideration the considerable number of people for whom the computer is the foundational object in mathematics. I did not use controvertial terminology in the edits.Likebox (talk) 20:03, 15 January 2008 (UTC)

For the purposes of proving that "ZFC-> X doesn't halt" implies "ZF-> X doesn't halt", only Godel's proof is enough. Fraenkel's proof doesn't cut it, and Cohen's is not necessary.Likebox (talk) 20:03, 15 January 2008 (UTC)

I have managed to get a PhD in logic without knowing about the standard terminology "unreal theorem". This may indeed be used by some authors (almost every conceivable terminology is used by someone); could you let me know where to look it up? As for independence, I don't think that the point about arithmetical statements is really important enough to emphasize in an introductory article. It is covered (albeit more abstractly) in absoluteness (mathematical logic). — Carl (CBM · talk) 20:07, 15 January 2008 (UTC)

Me too. --Hans Adler (talk) 20:21, 15 January 2008 (UTC)

Actually, my Ph.D. was in universal algebra and generalized recursion theory, both of which are normally considered to be within logic. I'd never heard of it, either. Perhaps he's a constructivist. — Arthur Rubin | (talk) 20:30, 15 January 2008 (UTC)

Ok, maybe I'm wrong about it being standard. I didn't use this terminology in the article, only in the talk page. I heard it from one or two logic professors who casually said "This system proves more real theorems than that system", when they meant more arithmetic theorems. The reason I think it is important to say this in an introductory article is because of my personal experience. The axiom of choice made me stop studying abstract mathematics as an undergraduate, because I felt it was proving lies, and I couldn't keep track of which theorems used it and which ones didn't. I don't want someone else to be driven away from math. If students understand that its a convenience, not a necessity, maybe that will assuage them. Yes, I do have a constructivist bent, so what. So do a lot of other people. The article as written is not biased toward one philosophy or another, in my opinion, since it only states things that everyone pretty much agrees with.Likebox (talk) 20:36, 15 January 2008 (UTC)

I think this point illustrates one of the sources for our communication problems, perhaps even the main one. You are not distinguishing between different modes of speech in mathematics. What you describe is "blackboard language", informal and unprecise language used by mathematicians to convey their ideas. It is only acceptable if it is (ongoing research or) based on much more precise statements. Except in the occasional descriptive paragraph it is not acceptable in normal publications or Wikipedia articles. Mathematics could also work without this restriction, but then it would be much easier to make mistakes. As it is, such definitions are always ad hoc and cannot be carried over from one context to another. You just can't use them undefined and expect others to understand what you mean. --Hans Adler (talk) 22:46, 15 January 2008 (UTC)

I am sorry for any communication gaffes--- I am trying my best to be clear. Perhaps I am not using the best language, but I am saying something precise. The theorem is that (ZFC->X halts) imlies (ZF->X halts).

This can be proved by a textual transformation. If you are given a proof of a theorem (forall integers n F^n(M) doesn't halt) in ZFC, where F is a function that takes a computer one processor step forward in time, and M is an integer that contains the computer's memory, you can translate the theorem to ZF. Replace every set S that occurs in every stage of the theorem with S_L, which just means the same S restricted to the Godel constructible universe. Then for every set which you used a choice function for, the L version has a choice function in ZF, so the proof goes through in L. Once the proof is finished, you end up with the theorem (forall L-integers n (F_L)^(n_L)(M_L) doesn't halt). But the L integers and the L-functions on the integers are the same as the ZF or ZFC integers, and so you've proved the same theorem. That's the translation. It works for any theorem about any absolute notions like integers and ordinals.Likebox (talk) 23:40, 15 January 2008 (UTC)

You are right in principle, but it is very hard to express this idea unambiguously. For example, how about theorems about the number which is 1 if there is a set that cannot be well-ordered, and 0 otherwise? That's not what you had in mind, but mind-reading should not be required to follow a mathematical argument. (Blackboard mathematics excepted, as above. In that case you can ask when you don't understand something.) --Hans Adler (talk) 00:02, 16 January 2008 (UTC)

Yes, I agree, this is a problem. But if the article becomes overly pedantic about points like this then it might become very technical, and too hard for the non-specialists. I am trying to express the precise statement as colloquially as possible, given the constraints of not saying something wrong. This is why I tried "Any statement about the halting or non-halting of a computer program", which I don't think can be misinterpreted. Maybe there's a way to misinterpret that too though.Likebox (talk) 00:17, 16 January 2008 (UTC)

I've deleted your second instance of computation arguments, and placed an {{importance-section}} tag (as we don't have an {{importance-inline}} tag) on the section. I think it's now clear what you're saying (thanks), but the importance is not clear. — Arthur Rubin | (talk) 00:40, 16 January 2008 (UTC)

I think it is important to note that the axiom is not one of those that proves new theorems about the integers--- that's really important. So that the people that cannot accept Banach-Tarski will be able to take it with a grain of salt.Likebox (talk) 00:46, 16 January 2008 (UTC)

I can't restore the tag, because of 3RR. But, if we were to count partial reverts, I would be at 4 and you at 5 already. So, could you please restore the tag while discussion is proceeding. — Arthur Rubin | (talk) 00:49, 16 January 2008 (UTC)

I'm certainly not going to call you on 3RR. Common sense tells me that at no point has this discussion devolved into anything resembling an edit war. I think it has been a reasonable attempt to come to a compromise. But I think that your tag is a little ridiculous--- why not mention that arithmetic theorems can be dechoiced? It will clarify the role of the axiom for constructively minded people.Likebox (talk) 00:59, 16 January 2008 (UTC)

Maybe your objection is to the use of computer programs as the absolute notion. If so, why not just rephrase it so that it says theorems about arithmetic?Likebox (talk) 01:01, 16 January 2008 (UTC)

(←) I tried to implement that suggestion. I used P = NP and the Riemann hypothesis, two famous unsolved problems, to illustrate that there are important problems for which choice is not a real improvement over ZF. — Carl (CBM · talk) 02:02, 16 January 2008 (UTC)

Looks good to me. As a (former, I suppose) professional logician, I sometimes find it difficult to understand the layman's point of view. I apologize to Likebox for that (as he doesn't want me to write to his talk page). — Arthur Rubin | (talk) 02:03, 16 January 2008 (UTC)

It looks good to me too.Likebox (talk) 05:53, 16 January 2008 (UTC)

Brilliant solution. After all this friction the article has definitely been improved. --Hans Adler (talk) 09:31, 16 January 2008 (UTC)

Great work, I'm glad for the friction -- and the good faith on all sides. The article is better now. Would it be too much to ask for a reference, though? CRGreathouse (t | c) 00:30, 17 January 2008 (UTC)

The way I make up my mind whether something is OR or not is by asking myself "Would I be embarassed by triviality to write a paper declaring this result?" In this case, given Godel's construction of L, which is presented in his 194-something monograph, the observation that AC is unnecessary for arithmetic proofs is sort of trivial. But I don't know the literature well enough to know where someone makes this observation explicitly.Likebox (talk) 02:16, 17 January 2008 (UTC)

No, that's not a good test. "Original research" is kind of a WP term of art; it doesn't really mean that it's necessarily particularly original, in the good sense of the word. Certainly something can easily be far too original to be added to WP without attributing it to someone, but not remotely original enough to be published in a research journal. --Trovatore (talk) 02:23, 17 January 2008 (UTC)

(edit conflict) I just vaguely remembered the phrase in Cohen's Set theory and the Continuum Hypothesis: "Godel's proof shows that any proof of a contradiction from ZFC can be textually manipulated into a proof of a contradiction from ZF. Likewise the proof that not-choice is consistent shows that any contradiction from ZF+notC can be textually manipulated into a proof of a contradiction from ZF." or something like that. I think that might be the best reference. Maybe not.Likebox (talk) 02:28, 17 January 2008 (UTC)

I'm not suggesting it's OR, just that a reader might want more details from some mathematical source. The Cohen source sounds good, if it's in there. CRGreathouse (t | c) 13:41, 17 January 2008 (UTC)

Speed up of proofs using AxCh?

The current revision by CBM says "When one attempts to solve problems in this class, it makes no difference whether ZF or ZFC is employed.". Even though one cannot prove more propositions in the language of Peano arithmetic, I think that you can prove some of them more easily (shorter, more direct proofs) if you are allowed to use the axiom of choice. Is this not correct? So this sentence should be changed. JRSpriggs (talk) 01:31, 17 January 2008 (UTC)

Doubtful. I don't have a source, but I don't see it as likely. — Arthur Rubin | (talk) 01:40, 17 January 2008 (UTC)

The essential point is that there is a textual map which takes a proof with AC to a proof without AC of almost exactly the same length. The only thing you need to do is put L subscripts on all the objects you are using and constructing. For example, if at some point you say "Consider the ring of functions on [0,1] under pointwise multiplication with the discrete topology, and the maximal ideal containing Froo and Bat and blah blah blah", you just say "Consider the ring of L-functions on L-R under pointwise multiplication and the L-maximal ideal containing Froo_L and Bat_L and blah blah blah", and then all the choice theorems are true for the L-versions of the objects even in plain ZF, or in ZF + "every subset of R is measurable", or in any other non-choicey extension.

So for example, if you like to thing of the universe as ZF+ "every subset of the real numbers is measurable", you can state, prove, and use the Banach-Tarski theorem in the following form: The set of L points in the unit ball in R^3 can be partitioned into a finite number of pieces, rotated and rearranged to form the L points in two unit balls in R^3. In this model, you have proven that the L-points are measure zero in the unit ball. If you use L-subscripts conscientiously, you lose no theorems by rejecting choice.

The complete lack of speed up is in stark contrast to the axiom of inaccessible cardinals, or any other large cardinal, which will shorten the proofs of certain theorems by such a large amount, that for a general provable theorem the old proof length will be greater than any computable function of the new proof length. This is a great, in my opinion under recognized, theorem of Godel's.Likebox (talk) 01:51, 17 January 2008 (UTC)

To Likebox: Your argument does not show a "complete lack of speed up". It shows that the speed up is merely linear. However, the proportionality may be very large in the formal language of set theory. JRSpriggs (talk) 02:53, 17 January 2008 (UTC)

You're right, the speed up in a formalization is linear, but that's the same speedup as by switching to a somewhat better formal syntax, which allows shorthand "macro" symbols which can be unpacked into more complex symbols. So the usefulness of AC is that of a macro. This is a stark contrast to the axioms of infinity and powerset, which produce speedups which are greater than any computable function. In informal mathematics, which uses shorthands without reservation, the only speed up comes from omitting "I am working in L" at the beginning of the proof.Likebox (talk) 03:15, 17 January 2008 (UTC)

I was just thinking model theoretically. I added another sentence; feel free to edit that further. — Carl (CBM · talk) 04:15, 17 January 2008 (UTC)

While your at it, you might also mention that adding the axiom of "decimal notation" shortens proofs by a linear factor. It allows 34 to be written as 34 instead of (1+1+1)*(1+1+1+1+1+1+1+1+1+1)+1+1+1+1. The point is nobody actually carries out proofs in a first order language without shorthands. If you add a short way of saying "Relativized to L" to the formal proof language, and you prove V=L is a model of ZFC, the proofs are essentially the same length.Likebox (talk) 05:51, 17 January 2008 (UTC)

I don't think there is need for this sort of detail. JRSpriggs was concerned, I think, about the claim that it makes "no difference", and gave an example of a difference it might make. I added a caveat to the sentence that should resolve that concern. — Carl (CBM · talk) 12:39, 17 January 2008 (UTC)

I was just making a point--- I have no complaints with the article.Likebox (talk) 12:46, 17 January 2008 (UTC)

Logical independence

"For example, the generalized continuum hypothesis (GCH) is not only independent of ZF, but also independent of ZF plus the axiom of choice (ZFC). However, ZF plus GCH implies AC, making GCH a strictly stronger claim than AC, even though they are both independent of ZF."

This seems to me to be the opposite of independence. Not(AC) implies Not(GCH), which is Not(logical independence). I'm changing it. --68.161.161.206 (talk) 12:11, 18 April 2008 (UTC)

Never mind. I should read what I'm talking about first. --68.161.161.206 (talk) 12:14, 18 April 2008 (UTC)

4th Paragraph of Usage

In 4th paragraph of Usage, there occurs this line -- "First we might try to proceed as if X were finite. If we try to choose an element from each set, then, because X is infinite, our choice procedure will.."

In this line "try to proceed as if X were finite." and "then, because X is infinite" are contradictory. —Preceding unsigned comment added by Histre (talk • contribs)

The key words are "as if" and the subjunctive "were". — Carl (CBM · talk) 13:04, 19 April 2008 (UTC)

There are two different cases (one is when X is finite, and the other is when X is infinite). In the first case, there is a method by which we can produce a choice function without appealing to this axiom. Unfortunately, that method does not work in the second case. That is all it is saying. There is no contradiction here. JRSpriggs (talk) 05:58, 20 April 2008 (UTC)

2nd paragraph of Usage: it's not induction, is it?

Quote: "(A formal proof for all finite sets would use the principle of mathematical induction.)" -- well, strictly speaking it's not proof by induction because a proof will not use the inductive step, i.e. the k'th step will not depend on the step(s) before. Isn't that right? A proof may just show it for an arbitrary k within the finite range. Or am I missing a point here? Regards, mikl-dk. —Preceding unsigned comment added by 87.60.229.89 (talk • contribs) 21:31, 14 June 2008

Nonconstructive aspects

From another point of view, mathematical constructivists do accept a version of the axiom of choice: If one assumes that every element of the original set is constructively inhabited (which is a stronger property than non-emptiness in constructive mathematics), then a choice function for the set can be constructively realized, and the axiom is not needed. [1]

It is true that any constructive proof of $\forall x \in a \; \exist y \in b \; R(x,y)$ must contain some way of constructing some element of b related by R to any element of a. But this is set theory, not type theory. Sets are supposed to be extensional. There can be many different ways of describing the same set, and no guarantee that this construction will associate extensionally equal elements of b to extensionally equal elements of a. So there won't always be a choice function.

On the other hand, if elements of a have a normal form, such as if a is the set of natural numbers, then of course one can get around this, so the axiom of countable choice is usually acceptable. A whole article could be written on constructive choice principles. --Unzerlegbarkeit (talk) 15:32, 4 July 2008 (UTC)

Hmm, interesting; I hadn't thought of that point (the one in the first paragraph). However I believe the claim that you removed is in fact accurate for some systems (for example, Intuitionistic Type Theory). It's true that ITT is type theory rather than set theory, but that doesn't mean that the relevant theorem is not reasonably understood as a form of AC.

I think there are also set theoretic theories for which the claim is accurate. Maybe this is a difference between CZF and IZF (I never really got straight what the difference is). --Trovatore (talk) 21:39, 4 July 2008 (UTC)

I don't think there is a "set-theoretic" theory for which that is accurate. Not CZF or IZF, anyway. Yes, we can certainly say something about type theory. In fact, I'd like to. And there was certainly truth underlying what I removed, but I think we'll have to do better than that. --Unzerlegbarkeit (talk) 22:25, 4 July 2008 (UTC)

Finanse • Informacja • Reklama • Pozycjonowanie • Reklama • Optymalizacja • Optymalizacja • Biurka • Meble • Reklama • Pozycjonowanie • Biurka • Kredyt • Pokoje • Rewal All Right Reserved © 2007, Designed by Stylish Blog.