Why do people question the Axiom of Choice? Banach-Tarski is nothing compared to what can do wrong without it

But doesn't that require the excluded middle?

Minimalism is a meme, but I understand if you rather want 10 axioms instead of 20.

>Thus, AC deniers believe in nonconstructible sets.
I don't follow you.

If I restrict my universe to an extend that the choice only says something about countable sets, then the axiom (or theorem) of choice is of course nothing to be scared of.
For "choice deniers", the axiom of choice is not bad in itself. It's just that if your theory describes a huge and possibly inaccessible quantity of things, adopting the axiom makes statements about those inaccessible things that have no basis you can grap on.
Indeed, a "set" is something for which the axiom of choice should hold, and even the constructive people will says that. Choice is good. But if you consider ZF with it's infinite chain powersets and more, THEN choice lets you prove claims you have no hold on - except when you wish them true by adopting the non-constructive axiom.

>We should not
nice opinion undergrad, where is your tumblr?

Maybe to state the point more explicitly:
If the axiom of choice becomes a theorem once you require the axiom of constructibility to hold, then this is because adopting the axiom of constructibility forces a lot of set theoretical objects (possibly available in general ZF without any of the extra axioms) to be no-go objects.
Stated again differently: The theory ZF+Constructilbiility is much more conservative than ZF alone, and axiomizes as much more hands on notion of "set". So, then, for those restricted class ob objects, you wouldn't be surprised that choice holds.

It's like when you set up the theory of groups G, there might be a statement S that you can easily prove for all finite groups. And it might turn out to be extremely hard to prove for non-finite groups. And then there are the GS people who work with the theory of groups+S, requiring S to hold for all groups from the get go.

You're the guy who says
>lel, the finite group people are so silly! Don't they know that if you require all groups to be finite, then this implies S!! This means finite group people believe in the truths of GS.
No. S is just true for the finite group. S as a theorem about groups is never problematic, it only becomes problematic when you think of it in context of all groups.

Maybe, but mathematics is by definition a language in which the not true is false and the not false is true. If you do not think this, you are not doing mathematics.

Funny thing is, intuitionists define their logic using binary logic, and just do classical logic over models with truth values in their desired classically-defined Heyting algebra with classical interpretations. Intuitionists are not self-aware.

I do certainly think there are nonconstructible sets. I just find it funny that those who reject AC also think so.

>>Maybe, but mathematics is by definition a language in which the not true is false and the not false is true.
there are no truths in mathematics. There are truth values, which have nothing do to with truths.

Let me add interpretational clarification brackets for you:

>Maybe, but mathematics is by definition a language in which [that which is proved] not true [is proved] false and [that which is proved] not false [is proved] true.

>I do certainly think there are nonconstructible sets. I just find it funny that those who reject AC also think so.
What do you mean by "there are"?

From a nominalist standpoint, obviously everyone agrees that you can write down a theory in the language of logic and try and formalize what constructive means and if there are terms in the domain of discours that are not constructive, then "there are" non-constructive sets in the theory.

And also in type theory, even if the theory is 100% constructive and you may check for 3+5 that it's of type N (the number "3+5" belongs to N), the system might be haunted by Gödelian non-computability and general type checking might be provably impossible and you can't decide everything about your system.

PS, rejecting the axiom of choice doesn't mean you're a constructionist. E.g. there are theories of differential geometry that have a rich notion of infinitesimal neighborhood, and to set up the theory you must reject even the (non-constructive) law of excluded middle because it contradicts other axioms.
But these axioms are also not constructive. So they reject non-constructive axioms in favor of other ones. They drop what they have to in terms of axioms to get back a still consistent framework to do math.

Show me one instance in real mathematics where excluded middle is rejected as a valid means of inference.

Show me this "differential geometry" that rejects excluded middle. It must be something other than nonstandard analysis or synthetic differential geometry because certainly both of those are real mathematics.

mathoverflow.net/questions/8537/synthetic-differential-geometry-and-other-alternative-theories#comment11558_8537

youtube.com/watch?v=zmhd8clDd_Y

I just reject the idea of actual infinity.
Life suddenly becomes simpler, easier and more intuitive.

I was half-wrong; this looks neither like the classical-logic metamathematics of intuitionism nor the quirks of formalism philosophical logicians concoct, but like mathematics.

I still think (correctly) that intuitionist logic is nothing more than classical logic operating over Heyting-algebra valued models, whence mathematics in any form is classical. This is true of smooth infinitesimal analysis as well.

But at least it's actually interesting.

I don't understand why (some!) people aren't accepting the axiome of choice as a something certain.

You could pretty much say "It seems obvious to me that the axiom of choice is a reasonable proposition we could accept as a fact, however, since it cannot provide constructive results, I will chose not to rely on it in my work.", but some are closer to saying "Hurr choice is dumb le boogeyman spooky choice banach tarski.".

>Just another few dozen axioms to add to ZF
More than that, it's not just "a few dozen axioms", it's "a few dozen axioms far less intuitive and which are harder to express but that we will keep so that this one non-intuitive result can not be proven even though it doesn't change much and 'preventing it' would actually just be 'not looking at it'".

Notions like the power set PY of a set Y are characterized by some formula in your logic, say
(S∈PY) ⇔ (∀Z.(Z∈S ⟹ Z∈Y)))

With a finite set, say
y={3,4}
you can run an algorithm constructing the subsets and you'll end up with
{}, {3}, {4}, {3,4}
making
Py = {{}, {3}, {4}, {3,4}}
the power set.
But with uncountable things, what PY means is "wished for", you don't have a list of subsets but just formulas in the logic. It's determined by the axioms.

This statement about the cardinalities of power sets
(|Y| > |X|) => (|PY| > |PX|)
i.e.
>"If a set Y is bigger than another set X, then it also has more subsets"
is also a "certain" "reasonable proposition", but neither the statement nor its negation is provable from ZF or ZF+Choice.

The above statement in fact turns out to imply the independent continuum hypothesis
>∄Y. |ℕ| < |Y| < |R|
(There are models which have such an inbetween set Y, with |PY|=R)

Clearly, the collection of axioms you call ZF or ZFC or any other of the strong ones are expressions of what you like a "set" to be, but what you get out of it will probably be a disappointment. Life is tough, things get hard already once you go from finite to countable, pic related.
I'd agree with you, "it's something certain for sets", but ZF is merely an attempt to define sets mathematically, and arguably not a good one.

People tend to not need it at all. You might need it when you want to prove some results in functional analysis and have your theorem say "for all vector spaces", including extremely opaque ones nobody ever uses. But of course, once you've proven it using choice, you just used a sledge hammer to make it true.

The axioms that are "certainly true" are those that will break any sensible notion of "collection" once you deny one of them, see e.g.
en.wikipedia.org/wiki/Kripke–Platek_set_theory
Beyond that, you generate "sets" that someone will eventually be troubled with.

>R can be a countable union of countable sets.

Wait what? How to achieve this in ZF?

As I've pointed out in , OP didn't list statements provable in ZF.
Otherwise, if they were provable false with in ZF+C and true in just ZF, then ZFC would be an inconsistent theory.

Instead, those are statements that ZF can't judge true or false, and they can be made true by adjoining more axioms to ZF.

For example, if you take ZF and literally add the axiom "R can be a countable union of countable sets", then this statement is trivially true there.
The only question is if this new set theory is inconsistent. If the negation can't be proven without choice, then it's consistent to adopt it.

This just shows that notion like "countable" are relative, if you leave the constructive core.

In other words, it not surprising that it can be made true (wished for). The surprising part about that is that ZF, as theory of sets, is not strong enough to prove it false (leaves it open).

Proofs by contradiction are not constructive.

>We should not want to permit these even as possibilities.
>not knowing about topos theory

>Maybe, but mathematics is by definition a language in which the not true is false and the not false is true.
No, apart from independence (the axiom shizzle), there are computationally undecidable problems.

en.wikipedia.org/wiki/List_of_undecidable_problems

E.g. the moral matrix problem
>The mortal matrix problem: determining, given a finite set of n × n matrices with integer entries, whether they can be multiplied in some order, possibly with repetition, to yield the zero matrix. This is known to be undecidable for a set of six or more 3 × 3 matrices, or a set of two 15 × 15 matrices.

You can't come up with a general algorithm that answers this query, i.e. a computer program that takes two square matrices as input and will return True or False whether this is the case or not.
There will always be a pair of matrices for which the property (of being able to be multiplied to the zero matrix) not true and not false.

>There will always be a pair of matrices for which the property (of being able to be multiplied to the zero matrix) not true and not false.

dafuq? no, just no.

this is ugly

I can understand why most people take AoC. It lets you prove some nice results that we intuitively think of as true yet aren't provable without choice.

But every time I've seen AoC/Zorn's Lemma/etc. invoked in a proof, it always feels like hand-waving.

Why does it have to have 9 variables? Does it not work for anything smaller?

>Julia Robinson and Yuri Matiyasevich showed that every Diophantine set has dimension no greater than 13. Later, Matiyasevich sharpened their methods to show that 9 unknowns suffice. Although it may well be that this result is not the best possible, there has been no further progress.[9] So, in particular, there is no algorithm for testing Diophantine equations with 9 or fewer unknowns for solvability in natural numbers. For the case of rational integer solutions (as Hilbert had originally posed it), the 4 squares trick shows that there is no algorithm for equations with no more than 36 unknowns. But Zhi Wei Sun showed that the problem for integers is unsolvable even for equations with no more than 11 unknowns.

I'm not sure to what extend you know this, but I may also point out that when it comes to classically interpreted propositions, classical propositional logic and intuitionistic propositional logic have the same proof strength (although proving theorems in classical logic might be more straight forward). This is because if the former proves P, then the latter always proves classically equivalent statements such as ¬¬P (and the converse of this is trivial). So to prove any (classically provable) theorem P, you can start out and stick to the intuitionistic framework the whole time, up until the end where, having proven ¬¬P intuitionistically, you apply an non-constructive (purely classical) translation such as ¬¬P→P.
(This can be extended to a theory with existential quantifier. It can also be extended to the universal quantifier, except the translation is more intricate. )

Example, constructive proof of the double negation of the law of excluded middle:

Using the classical equialence

P↔¬¬P

and

¬(P∧Q)↔(¬P∨¬Q),

we get the classical equivalences

(A ∨ ¬A)

↔ (¬¬A ∨ ¬¬¬A)

↔ ¬(¬A ∧ ¬¬A)

↔ ¬¬¬(¬A ∧ ¬¬A)

The last two can be proven constructively!
Take any A, B and observe that

((A→B) ∧ ((A→B)→B))→B

>If it's the case that 'A implies B' and also that 'A implies B' implies B, then B is the case.

In (constructive) type theory, the prove f is the expression
f(p) := eval(π2(p), π1(p))
where p is a pair of functions and π's are the left and right projections so that
π2(pair) : A→B
π1(pair) : (A→B)→B

If we now consider B to be absurdity resp. the empty type ⊥, then we have proof resp. a term of

(A→⊥) ∧ ((A→⊥)→⊥)→⊥

which using

¬X ≡ X→⊥

reads

¬(¬A ∧ ¬¬A)

>If it's the case that 'A leads to an absurdity' and also that 'A leads to an absurdity' leads to an absurdity, then this leads to an absurdity.

...

PS: The downside of not using LEM being your proofs might be long, and the upside being your proofs always have an algorithmic content (LEM just makes some things true by definition)

E.g. having proven
A → ((A → B) → B)
you simultanously construct a function. Here
f(a) := g ↦ g(a)
where g : A → B.

Or
(A ∧ B) → B
is proven by the right projection
π2
or
f(p) := π2(p)

Or
(A ∧ B) → (B ∧ A)
is proven by
f(p) := (π2(p), π1(p))

Or
A → ¬¬A
which is read as
A → ((A→⊥) →⊥)
which is a special case of
A → ((A→B) →B)
above.

And finally,
¬¬A → A
or more generally
((A→B) → B) → A
is something that just has no functional content, because given a function
F: (A→B) → B
where if
g : A→B
then
F(g)
is a term of B ... this F doesn't enable you to construct a term of A in any way, so
((A→B) → B) → A
is not constructively provable.

intuitionists are classical guys thinking they are better than everybody.
the truth is that constructivists are the best

The logic is the same of the last two

what!? proof of 3 and 4? very doubtful

that's not the only downside. many statements in math are equivalent to LEM, I think the intermediate value theorem for exmaple

>equivalent
Maybe be more specific. A theorem in a theory about things that have a topology like the real numbers is not equivalent to a 4 symbol sentence in propositional logic.
To prove the intermediate value theorem, as classically formulated, you need LEM.

But (as I go in at lengths in that post) eve if you drop LEM, you can prove a statement that's classically the same as the intermediate value theorem:
You can't prove the intermediate value theorem in constructive analysis - you can "merely" prove any form of it that you could realize algorithmic ally.
But you can, in a classical logic, prove the intermediate value theorem USING JUST constructive analysis.

>muh axioms
math is the most authoritarian shit I've ever seen

How come? Everybody can choose his own?
It's rather like fashion, choose the clothes that you like.

no not at all
intuitionist think that the powerset axiom [for any set, its power set exists] is fine
constructivist are predicative constructivist

>without AC there are vector spaces without bases

this fact alone is enough to make me want AC

>waaahhhh math without choice is too hard.

kys yourself

It has been rather hot, hasn't it

>Maybe, but mathematics is by definition a language in which the not true is false and the not false is true. If you do not think this, you are not doing mathematics.

>knowing that a type is inhabited is exactly the same as having the value of that type

sure, senpai.

*a value

>>without AC there are vector spaces without bases
>
>this fact alone is enough to make me want AC
brain.let

How many of those can happen under Dependent choice?

NBG > ZF
Prove me wrong.

Sup Wildberger, how is that "Affine Line" treatin ya?

wtf I hate math now

dude just let V = L axiomatically lmao

With [math]0^\sharp[/math], there is an ordinal [math] \alpha [/math] such that [math]L_\alpha[/math] is elementarily equivalent to the entire constructible universe [math] L [/math]. Wouldn't that be nice? Too bad you can't have it with your [math]V=L[/math].

I'm not this guy, and I don't know any cardinal analysis - so can you tell my why that would be nice?

Also, do you know what level of cardinal the smallest non-trivial Grothendieck universe is? It may be the one generated by the naturals, or [math] \omega_0 [/math].
Or why in the world one would go beyond that?

It would be nice because it is pretty.

To be of any use we clearly want a Grothendieck universe in which there is an infinite set, as otherwise we really can't do any mathematics. Your intuition is right that the smallest Grothendieck universe (other than the empty set) is the set of hereditarily finite sets (i.e. sets whose transitive closures under [math]\in[/math] are finite).

But we generally want our Grothedieck universe to contain infinite sets. In this case, a Grothendieck universe is nothing more than [math]V_\kappa[/math] for [math]\kappa[/math] a strongly inaccessible cardinal. Inaccessible cardinals are the weakest large cardinal hypothesis, being equiconsistent with the mere assertion that ZF (or equivalently ZFC) is consistent.

People don't really question AoC anymore. Some prefer to do without it but it's not a topic of debate anymore.

I really dislike ideas of what "proper" axioms are. They're just the rules for the game you're playing, if it creates an interesting game you're fine.

I wish this were the case but it's absolutely not. It's pretty easy to find modern debates over what the proper axiomization of thing X is. "Formalists during the work week, platonists on weekends" and all that.

I can be very good friends with the constructible universe and saying that I adopt it as my setting to do math.

Okay, let's assume we do that.
What do we gain from the axiom L=V?
If I'm "so conservative as to choose L as my universe", why would I (still) care for V?

You seem to like large cardinals, here the question: What's to gain from going beyond the neat model of ZFC that is L?

The Axiom of Determinacy is a large cardinal hypothesis that is not only very large but is incompatible with V=L.

It is a very useful hypothesis in recursion theory, measure theory, descriptive set theory (which has applications outside of logic to ergodic theory) and others, in which it gives many very elegant results. That it gives such elegant results is viewed as evidence of its utility as a large cardinal axiom and why we might wish to work in ZF+AD.

That AD is so utile outside of set theory and outside of even mathematical logic is why mathematicians as a whole might care about it. But other large cardinal properties also have applications to the likes of model theory, such as strongly compact cardinals and their application to model theory over infinitary languages. Model theory finds increasing use in fields such as algebraic geometry, and a model theory of infinitary languages may transitively have applications to it.

Large cardinal axioms can also serve as evidence against things like AC due to their sheer beauty. For instance, a nontrivial elementary embedding of the universe of sets into itself would be beautiful: it implies a sort of "absolute fullness" of the universe of sets above a certain point. The least cardinal moved by such an elementary embedding is called a Reinhardt cardinal. Unfortunately, it is incompatible with AC, but it feels like it should be true. Thus large cardinals can translate to a sort of philosophy of mathematics.

So from concrete applications to fields outside of logic to a mathematical philosophy of mathematics as a whole, there is much to gain from the study of large cardinals.

Do you know anything about how Mochizuki uses set theory?
Looks model theory-like to me.

I do not.

The axioms are interesting when they mean something. But if you know what they mean, you have the added benefit of knowing where to apply them. If you just look at it as a game and work on whatever looks like a cool game, fine whatever, but that kind of math doesn't tend to last or have a meaningful impact on things.

since type theory is prettier than retarded set theory, type theory is evidently useful and can also serve as evidence against things like set theory due to their sheer beauty.