Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
On the Wikipedia page for the Axiom of Choice the following statement is given:
$(\forall x^\sigma)(\exists y^\tau)R(x,y)\rightarrow(\exists f^{\sigma \rightarrow \tau})(\forall x^\sigma)R(x, f(x))$
Most of it seems fairly straightforward, except for the meanings of the symbols that look like 180 degree rotated 'E' and 'A'
The symbols are quantifiers. They bind a new variable name to the symbolic logic statements. ∃ reads as there exists. ∀ reads for all so the first part of the statement would be read as:
forall x (of type 𝜎), there exists a y (of type 𝜏) such that ...
$\forall$ reads as "for all", and $\exists$ reads as "there exists". So, in english we have
$$\text{"if }\underbrace{\text{for all $x$}}_{\forall x^\sigma}\text{ }\underbrace{\text{exists a $y$}}_{\exists y^\tau}\text{ with $R(x,y)$, }\underbrace{\text{then}}_\to\text{ }\underbrace{\text{there is a function $f$}}_{\exists f^{\sigma\to\tau}}\text{ so that }\underbrace{\text{for all $x$}}_{\forall x^\sigma}\text{ holds $R(x,f(x))$".}$$
I skipped over the $\sigma$ and $\tau$ superscripts, as they indicate types and are not of primary importance here.
