The function [math] f: \{ 0,1,2,3 \} \to \{6,7\} [/math] defined by [math] f(0):=6 [/math] [math] f(1):=6 [/math] [math] f(2):=7 [/math] [math] f(3):=6 [/math] is surjective: Its range (the set of values, 6 and 7) indeed equals its codomain ([math] \{6,7\} [/math]).
The function has a right inverse [math] r: \{6,7\} \to \{ 0,1,2,3 \} [/math] For example, [math] r(6):=3 [/math] [math] r(7):=2 [/math] makes it so that [math]f \circ r[/math] is the identity function on [math] \{6,7\} [/math]: [math]f(r(6))=f(3)=6[/math] [math]f(r(7))=f(2)=7[/math] It's easy to write down some right inverse if the sets involved are finite.
But does every surjective function have a right inverse?
That proof uses the axiom of choice. So I take it you say the axiom of choice is true?
Gavin Evans
You shouldn't need AC if you're not working with infinite functions, no?
Owen Robinson
Consider suicide
Easton Barnes
Wow, you bothered to write all of that down before you bothered to think? Try better next time.
Jace Martin
is this bait how does it have an inverse if r(6)=3 and r(7)=2 what about [eqn]f^{-1}(0)[/eqn]
John Sanders
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.
Cameron Martin
I read Camus.
Think to reach which conclusion?
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.
Nathan Johnson
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.
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.
Robert Price
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.
Matthew Thompson
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?)
Brayden Brooks
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.
Kevin Lewis
The berger says there are not an infinite number of functions.
Jaxson Williams
>finitism
Gabriel Powell
>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"
Jaxson Anderson
>>strong intuitionistic reading of existential quantifer yields a right inverse from the statement of surjectivity Could you elaborate?
Cameron Robinson
So are you on the side of "choose the framework you feel like" or do you have constructionist convictions (in the intuistionstic logic sense)?
Isaiah Walker
Why does the cat look so sad?
Hunter White
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.
Ethan Gomez
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
Angel Perez
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)
"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.
Nolan Stewart
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.
Zachary Williams
the non-constructive aspects of the logical formalization of math were criticized right away. The whol shebang is no 150 years old.
