I don't want your opinion, I want just the mathematical truth

>does every surjective function have a right inverse
Yes, this is the definition of surjectivity.

>>8059014

https://proofwiki.org/wiki/Surjection_iff_Right_Inverse

File: Wikipedia.png (27KB, 383x149px) Image search: [Google]

27KB, 383x149px

>>8059022
That proof uses the axiom of choice.
So I take it you say the axiom of choice is true?

>>8059380
You shouldn't need AC if you're not working with infinite functions, no?

>>8059380
Consider suicide

>>8059014
Wow, you bothered to write all of that down before you bothered to think? Try better next time.

is this bait
how does it have an inverse
if r(6)=3 and r(7)=2 what about [eqn]f^{-1}(0)[/eqn]

>>8059405
Infinite functions? The axiom of choice is only needed in this case when it is not clear how to pick an element of the preimages to form the inverse.

>>8059407
I read Camus.

>>8059408
Think to reach which conclusion?

>>8059413
Right inverse:
For the surjection
[math]f: D \to C [/math]
this is a function
[math]r: C \to D [/math]
so that [math]f \circ r[/math] equals the identify on the [math] C [/math].
Here [math] C [/math] may be smaller than [math] D [/math], as in the example.

>>8059425
Nope.

From wikipedia:
>Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin. In many cases such a selection can be made without invoking the axiom of choice; this is in particular the case if the number of bins is finite.


https://en.wikipedia.org/wiki/Axiom_of_choice

>>8059405
you're not working with infinite functions (I assume you mean infinite domain or codomain by this), but to prove things about all functions, as OP is trying to do, you are essentially talking about an infinite number of functions, including ones with domains you can't easily choose elements from to form a right inverse. Thus, you need AC to prove that every surjective function has a right inverse.

>>8059455
By the way, this comes up all the time in category theory when you try to factorize an arrow through an equalizer. In the category of sets, this coincides with OP's statement.

>>8059455
If we axiomize that every surjective function has a right inverse, can we prove the axiom of choice?
(If we axiomize that every surjective function has a right inverse, can we prove Banach Tarski?)

>>8059464
If you take that as an axiom, it is equivalent to AC, as are a lot of statements of this type.
So yeah, you could prove Banach-Tarski.

>>8059455
The berger says there are not an infinite number of functions.

>>8059471
>finitism

File: 1374308882536.png (28KB, 238x231px) Image search: [Google]

28KB, 238x231px

>accept constructivism
>strong intuitionistic reading of existential quantifer yields a right inverse from the statement of surjectivity
why on earth would someone EVER accept classical logic but then reject AC? It's like getting the worst of both worlds, and there's no good philosophical justification
>"b-but I want to be able to construct my mathematical objects...some of the time"

>>8059556
>>strong intuitionistic reading of existential quantifer yields a right inverse from the statement of surjectivity
Could you elaborate?

File: Woof.jpg (2MB, 1698x1131px) Image search: [Google]

2MB, 1698x1131px

>>8059556
So are you on the side of "choose the framework you feel like" or do you have constructionist convictions (in the intuistionstic logic sense)?

>>8059566
Why does the cat look so sad?

>>8059564

According to the BHK interpretation, a proof of

[math]\forall x\in A \varphi(x)[/math]

is a "function" that takes as input an element [math]a \in A[/math]
and outputs a proof of [math]\varphi(a)[/math]; and a proof of

[math]\exists x\in A \varphi(x)[/math]

is a pair consisting of an element [math]a \in A [/math] and a proof of [math]\varphi(a)[/math].

Thus, a proof or statement of [math]\forall y\in B\exists x \in A f(x) = y[/math] is read in this interpretation as a function accepting inputs [math]b \in B[/math] and outputs pairs [math]\langle a,P\rangle[/math] where [math]P[/math] is a proof of [math]f(a)=b[/math].
If we throw out the second component this gives us a function [math]g : B \rightarrow A[/math]. Furthur, we can use those [math]P[/math]'s to prove that [math]g[/math] is a right inverse.

I believe that in this manner, the statement that every surjection has a right inverse is provable in most type theories. Things get a bit hairier in constructive set theories, but I don't know much about that.

>>8059566
Both I guess. I like constructive mathematics because you can immediately see applications to the real world and the ontology is a bit more coherent. However, I think convincing mathematicians to give up classical logic is a bit of a fool's errand. And anyway, most mathematician's proofs end up being constructive anyway, or can be easily modified to yield constructive content

>>8059606
Yeah, I know that 'an' axiom of choice is provable in Per Martin Löf's type theory
(that theories notion of "set" is of course not as permissive as the ones written down in first-order logic)

>>8059611
"easy", depending on how explicit you want it.
I don't know but it might be that the algorithmic part of even new modern proves is not particular special. It often might come down to ideas found to be effective at the right place.

File: 1404674920492.jpg (31KB, 285x281px) Image search: [Google]

31KB, 285x281px

>>8059556
People who cry about AC are retarded psuedophilosophers who aren't bright enough to actually produce something definitive and modern so they have make problems out of previously insignificant things. They then create a proof without AC and expect to receive praise for solving a problem they themselves created and nobody gave a fuck about to begin with.

It's like blowing up a building in the middle of fucking nowhere then rebuilding it again and then expecting to receive an award for beautiful architecture the second time around.

File: DFW_SUFF.png (220KB, 347x440px) Image search: [Google]

220KB, 347x440px

>>8059706
the non-constructive aspects of the logical formalization of math were criticized right away. The whol shebang is no 150 years old.

https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy#Origins_of_disagreement

>>8059380
>If it's in one thing it's also in da other thing

Wow it's fucking nothing. Can we stop trying to reinvent the definition of functions and get on with it?

>>8061221
bump for what, bre?

File: 1438686462258.png (58KB, 991x311px) Image search: [Google]

58KB, 991x311px

>>8061404
In a locally-small category, arrows which are epic are not necessarily a surjection, while monics may not be an injection.

this proves that m is monic, yet not injective.

>>8061411
funfact on the side?

It's not like epics are a very setty notion (they shouldn't be primarily thought of as functions to begin with)