Asserting that
∀a∈A ∃b∈B s.t. P(a, b)
implies
∃f : A ⟶ B s.t. ∀a∈A P(a, f(a))
is just the same as asserting the Axiom of Choice.
This Tweet was deleted by the Tweet author. Learn more
Conversation
I feel like they also have different computational content in a constructive setting? Although nothing jumps out at me for a proof
2
3
They mean different things constructively because the Axiom of Choice isn't constructive. Constructively,
∃f : A ⟶ B s.t. ∀a∈A P(a, f(a))
implies
∀a∈A ∃b∈B s.t. P(a, b)
(just take b = f(a)), but not the converse (since you can't pull f out of thin air).
5
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
I don't really understand your first tweet, but your second has made me finally /feel/ the connection to Choice, so thank you.
Also, under what system is your final remark (about P(a, b1) and P(a, b2))?
1
1
This Tweet was deleted by the Tweet author. Learn more
is there a dual notion to "squash" called "smoosh"?
2
This Tweet is from an account that no longer exists. Learn more
sorry this was a really bad drive-by joke and I should be ashamed. but this was a better response than I deserved so thanks I think? (it was interesting! 🤩)