- #1

- 2,111

- 18

- Thread starter jostpuur
- Start date

- #1

- 2,111

- 18

- #2

- 1,838

- 7

Well, everything we can observe is formally describable, at least we don't have any evidence to the contrary. So, although we can talk about the set of real numbers being a continuum (most of which are not formally describable as Turing showed) and then needing to postulate the Axiom of Choice to "legalize" the act of choosing an element from such a set, even though there is no formal describable way to do that, this doesn not prove that we really need this.

This is similar to postulating a God and then finding out that it is a hypothesis we don't really need, although it can be useful in practice (e.g. to get elected as President).

In first order logic, you only need countable sets, http://www.earlham.edu/~peters/courses/logsys/low-skol.htm" [Broken]. This means that any model which is uncountable can be reinterpreted as a countable model.

LST has bite because we believe that there are uncountably many real numbers (more than [tex]\aleph_0[/tex]). Indeed, let's insist that we know it; Cantor proved it in 1873, and we don't want to open the question again. What is remarkable about LST is the assertion that even if the intended interpretation of S is a system of arithmetic about the real numbers, and even if the system is consistent and has a model that makes its theorems true, its theorems (under a different interpretation) will be true for a domain too small to contain all the real numbers. Systems about uncountable infinities can be given a model whose domain is only countable. Systems about the reals can be interpreted as if they were about some set of objects no more numerous than the natural numbers. It is as if a syntactical version of "One-Thousand and One Arabian Nights" could be interpreted as "One Night in Centerville".

Last edited by a moderator:

- #3

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

Algebraic closed fields are important for algebraic geometry and algebraic number theory; I've once heard something to the effect that most of modern algebraic number theory is concerned with the study of the Galois group [itex]\mathrm{Gal}(\bar{\mathbb{Q}} / \mathbb{Q})[/itex].

While I suspect you

Maybe the theorems you want can be proven without algebraically closed fields -- but they'll be much more difficult to show. Maybe the calculations you want to do can be done without algebraically closed fields -- but the theorems that say how to go about doing it might still rely on them.

As for PDE's, Hilbert spaces, and so forth -- I wouldn't dare make any claims as to what would even still work in those theories if you cast out the AoC! I would be too afraid of missing an assumption that depends on some vector space having a basis, or some functional existing, or some set being closed, or such and such that simply isn't true without the AoC.

- #4

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

I suspect you've fallen into a trap -- confusing the internal theory with the external theory. (e.g. see Skolem's paradox) Within your (externally) countable model of first-order set theory, you still have (internally) uncountable sets -- e.g. you still have the theorem that [itex]|\mathbb{N}| < |\mathbb{R}|[/itex]. There simply does not exist an internal bijection of the (internal) setsIn first order logic, you only need countable sets, http://www.earlham.edu/~peters/courses/logsys/low-skol.htm" [Broken]. This means that any model which is uncountable can be reinterpreted as a countable model.

Last edited by a moderator:

- #5

HallsofIvy

Science Advisor

Homework Helper

- 41,833

- 956

- #6

- 2,111

- 18

About PDEs and Hilbert spaces... for example the Fourier modes in [itex]L^2([0,2\pi],\mathbb{C})[/itex] exist fine without AOC. I see that the study of PDEs naturally leads to the study of infinite dimensional vector spaces, and on the other hand the study of infinite dimensional vector spaces naturally leads to the AOC. So one might think that PDEs naturally lead to AOC, but I disagree on this. If you actually fix some concrete vector space, the useful basis usually exist without AOC. I bet you cannot point out an example of a PDE, whose solution's existence depends on AOC.

- #7

- 655

- 3

If this is true, you could look for examples of Sobolev spaces that require Zorn's lemma for a basis, and then invent a PDE using that space.

- #8

- 533

- 5

I don't think you need the axiom of choice for anything, except to make things easier. Trying to do a lot of maths without at least dependent choice (which is a countable version of AOC) would be very tedious.

Also, you could take any proof using AOC and rewrite it to prove that "if such and such a choice function exists then ...". in any applications you would hopefully be able to find the necessary choice functions and then apply the theorem without AOC. If you can't, then I'm not sure that your theorem is really that helpful (i.e. you've proved something exists but have no way of constructing it).

Maybe HallsofIvy's post illustrates my point.

if a Hilbert space H has a choice function mapping any closed proper subspaces to an element of H not in that subspace, then H has an orthonormal basis.

In fact the choice function picks out a unique such basis. In many cases you can describe such a choice function too.

If you can find a sequence of elements x_1,x_2,x_3,... whose linear span is dense in H then there is a choice function taking a subspace V to the first x_k not in H.

Also, you could take any proof using AOC and rewrite it to prove that "if such and such a choice function exists then ...". in any applications you would hopefully be able to find the necessary choice functions and then apply the theorem without AOC. If you can't, then I'm not sure that your theorem is really that helpful (i.e. you've proved something exists but have no way of constructing it).

Maybe HallsofIvy's post illustrates my point.

without AOC you could say that.

if a Hilbert space H has a choice function mapping any closed proper subspaces to an element of H not in that subspace, then H has an orthonormal basis.

In fact the choice function picks out a unique such basis. In many cases you can describe such a choice function too.

If you can find a sequence of elements x_1,x_2,x_3,... whose linear span is dense in H then there is a choice function taking a subspace V to the first x_k not in H.

Last edited:

- #9

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

- #10

- 533

- 5

well, [itex]\bar{\mathbb{Q}}[/itex] is just the set of algebraic numbers in the complex number field, which constructs it. You don't need AOC for algebraic closures of finite fields either.While I suspect youmightbe able to construct [itex]\bar{\mathbb{Q}}[/itex] without AoC, I wouldn't dare make any predictions about how infinite Galois theory would behave. And even if you can... you still need algebraic closures of finite fields, which you don't get without AoC.

You do need it for the infinite galois group [itex]\operatorname{Gal}(\bar{\mathbb{Q}}/\mathbb{Q})[/itex] though. I think you could still do algebraic number theory without it, but you'd have to replace the elements of the galois group with elements on finite but arbitrarily large extensions of Q. AOC makes life easier but leads to very nonconstructive proofs.

- #11

- 22

- 0

The proof of the independence result also shows that a wide class of mathematical statements, including all statements that can be phrased in the language of Peano arithmetic, are provable in ZF if and only if they are provable in ZFC. Statements in this class include the statement that P = NP, the Riemann hypothesis, and many other unsolved mathematical problems.

- #12

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

Oh bleh, and I just went through all this a couple years ago too. Woe is me and my spotty memory! What about the p-adic fields? I imagine you can do those too, then.well, [itex]\bar{\mathbb{Q}}[/itex] is just the set of algebraic numbers in the complex number field, which constructs it. You don't need AOC for algebraic closures of finite fields either.

- #13

- 22

- 0

Whoa, a theorem intheorem. (at least as I understand things) Of course, you have to be careful about all of the other things that become more complicated....

- #14

- 533

- 5

aah yes. I remember hearing something like that too. I'm a bit vague about it, but I expect that it is a theorem in the "metalanguage", and not inside the logic itself. That is, constructivism restricts what you can construct so much that there's not really any arbitrary choices left to be made.I would like to point out that, oddly enough, if you're really serious about constructivism, then it turns out that the axiom of choice is actually atheorem.

- #15

- 533

- 5

Hmm, not sure, I'd have to think about it...What about the p-adic fields? I imagine you can do those too, then.

...

no, you don't need AOC!

you only need to add roots of integer or rational polynomials, because they're dense, and they can be well ordered - which should avoid AOC.

(that's my first thought. haven't been through the details)

Last edited:

- #16

CRGreathouse

Science Advisor

Homework Helper

- 2,820

- 0

The constructive axiom "V = C" implies AC in ZF.Whoa, a theorem inwhat? Gödel showed it is not a theorem in ZF, and neither is its negation (assuming ZF is consistent, of course.)

- #17

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

I confess that I don't know how constructivist set theory is done from a formal logic viewpoint. But I can state a version of choice for Turing macines; I strongly suspect the analogous theorem for constructivist set theory is similar in spirit (if not actually the same).

**Theorem**: There exists a Turing machine AC that has the following behavior on a string M.

1. If M is a description of a Turing machine T that accepts at least one string, then AC accepts M, and outputs a string AC(M) that is accepted by T

2. If M is a description of a Turing machine T that never accepts anything, then AC doesn't halt

3. If M is not a description of a Turing machine, then AC rejects M.

If we interpret a Turing machine T as being analogous to a set (i.e. [itex]x \in T[/itex] is defined to mean "T accepts x"), then AC computes an explicit choice function on the class of all nonempty sets.

One implementation of AC is as follows:

(where I've assumed we've chosen an enumeration of all strings, and an enumeration of all pairs of natural numbers)

1. If M is a description of a Turing machine T that accepts at least one string, then AC accepts M, and outputs a string AC(M) that is accepted by T

2. If M is a description of a Turing machine T that never accepts anything, then AC doesn't halt

3. If M is not a description of a Turing machine, then AC rejects M.

If we interpret a Turing machine T as being analogous to a set (i.e. [itex]x \in T[/itex] is defined to mean "T accepts x"), then AC computes an explicit choice function on the class of all nonempty sets.

One implementation of AC is as follows:

Code:

```
If M is not a turing machine description, Reject.
For every pair of natural numbers m, n:
Let S be the n-th string
Simulate M for m steps on S
If M has accepted S, then Accept and output S
```

Last edited:

- #18

- 533

- 5

but strings are well ordered, so AOC for subsets of such things is trivial anyway. Is that really enough to imply AOC for constructive logic

(AOC applies to sets of nonempty sets. Maybe any constructive proof that the sets are nonempty can be converted to a choice function. Seems reasonable, but I'm not very familar with constructive logic.)

(AOC applies to sets of nonempty sets. Maybe any constructive proof that the sets are nonempty can be converted to a choice function. Seems reasonable, but I'm not very familar with constructive logic.)

Last edited:

- #19

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

My understanding of constructivist set theory (and related things) is that it's very closely related to computability theory, so I suspect that it is enough.but strings are well ordered, so AOC for subsets of such things is trivial anyway. Is that really enough to imply AOC for constructive logic?

However, my quote that AoC is a theorem is relayed by a friend of mine who studied non-standard analysis (NSA): he loves to tell the story about how he'd explain his discipline to most mathematicians, and they'd view it with suspicion because of the way it uses AoC... so when he was explaining it to a constructivist, he expected to be outright rejected, and was completely taken aback when the constructivist had absolutely no problems with NSA's foundations, because AoC becomes the "theorem of choice".

- #20

- 22

- 0

Ahh, thank you.The constructive axiom "V = C" implies AC in ZF.

- #21

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

- #22

- 533

- 5

Where does that go wrong with constructive logic.

- #23

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

(I'm not having any luck finding a good online source for constructive analysis. Bleh)

- #24

- 533

- 5

So, in constructive logic, the only subsets of the reals are emptyset and R. Is that true?

Seems to follow from what you said, but I don't know what you're allowed to do in CL

- #25

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

- Last Post

- Replies
- 9

- Views
- 4K

- Last Post

- Replies
- 27

- Views
- 5K

- Replies
- 3

- Views
- 2K

- Replies
- 9

- Views
- 3K

- Replies
- 61

- Views
- 9K

- Replies
- 2

- Views
- 563

- Last Post

- Replies
- 5

- Views
- 3K

- Last Post

- Replies
- 2

- Views
- 1K

- Last Post

- Replies
- 3

- Views
- 3K

- Last Post

- Replies
- 1

- Views
- 3K