How could anyone accept anything as non-obvious as the axiom of choice as a fucking axiom?

>shittiest grammar you can possibly imagine.
so this is... the true autism...

>Everything that can be proven with the AC can be proven, although longer, with other axioms.

This is demonstrably false because there are important theorems that have been proven to not only be implied by AC, but that also imply AC if they are assumed as the axiom.

For example. The statement:
>Given any two sets, they either have the same cardinality or one has a smaller cardinality than the other

is equivalent to the axiom of choice. So if you assume this as an axiom (and lets be real, this theorem should be axiom as it is more obvious) then you could prove "the theorem of choice".

AC being the axiom is just a historical quirk. God was writing his set theory to give it to us humans when he found that the original axioms were not enough to prove the well ordering theorem, and then formulated the axiom of choice in such a way to complete his proof immediately.

So blame God.

Yeah, fuck off. If you haven't seen anything that needs AC then you haven't even finished your undergrad. Applications of Zorn's Lemma are fucking everywhere.

- Every vector space has a basis
- Alexander's subbase theorem (and the following Tychonoff product theorem)
- Every ideal is in a maximal ideal (+ a shitload of results in commutative algebra)
- Every product of nonempty sets has an element
- Every set can be well-ordered

>non-obvious
go back to MIT nigger

>assuming structure and not just proving that that structure exists

non-constructivists make me want to throw up

Not understanding first order logic.

Go back to engineering where you belong.

What, pray tell, don't I understand about FOL?

Proof by contradiction, i.e. that if we prove a contradiction upon assuming an object does not exist then the object must exist.

Constructivists believe that despite the object being unable to not exist, it doesn't necessarily exist. Pure genius.

>the object
what object?

1. It's necessary
2. See 1

Axioms aren't supposed to be self-evident rules, they're the smallest package of rules that work to get the results we know we should get and can't be demonstrated from previous rules.

Publish that argument in a national journal.

>Constructivists believe that despite the object being unable to not exist, it doesn't necessarily exist. Pure genius.

same to you friendo

"Something can exist and not exist at the same time".

You haven't shown that something exists, you've just shown that it isn't the case that something doesn't exist

If it isn't the case that something doesn't exist, what other cases are there other than the case that something does exist?

the whole point of constructive mathematics is a more stringent standard for proof. It is not enough to know that something must be out there, you have to actually exhibit or construct the object

I know what constructive mathematics is, but that doesn't answer my question.

Since some proofs require only the existence of something, but other proofs require an explicit construction of this thing we already have a distinction between the amount we can conclude from showing the existence of something compared to actually constructing something. What does deciding that the existence of an object (but not construction) is meaningless do to improve the rigour of mathematics?

>Since some proofs require only the existence of something, but other proofs require an explicit construction of this thing we already have a distinction between the amount we can conclude from showing the existence of something compared to actually constructing something

I'm not sure what you're talking about. In fact, the distinction between constructive existence and classical existence disappears with classical logic

Some proofs only require knowing something exists with a certain property, others require you to know a specific thing with this property.

>Some proofs only require knowing something exists with a certain property

If your proof actually doesn't require a specific object, a constructivist would say you're being more "honest" by using ¬∀¬ instead of ∃ in the statement of whatever you're proving. In this manner, all classical results can be interpreted naturally within intuitionistic logic, while the reverse cannot be said

e.g. Cantor–Schröder–Bernstein tells us that if we have injections from A to B and from B to A, there exists a bijection from A to B.

So if we needed to prove something that relied on A being the same size as B, just the existence of the bijection is enough.

Whereas if we needed to give a specific bijection from A to B, then C-S-B would not be enough (assuming A and B infinite, in the finite case we know the injection from A to B so this must also be a bijection).

Honestly I just disagree that you can refute the law of excluded middle, it doesn't make sense to me to decide "not false =/= true".