Even number elements in universum - sentence in second order I would like to write following sentence in second order logic:
universum has even number of elements.
And my atempt is as follows:
$$\psi \wedge \exists_{f()} \forall_x \forall_y x\neq y \wedge f(x) = y \rightarrow f(y) = x $$
$\psi$ states that universum is finite - it is easy to express in second order logic.
Is this correct ?
Edition
Below, @Noah answered and corrected slightly my solution.   However, I would like to try use his hint for alternative solution:
$$\phi_A=\exists_{A_1}\exists_{A_2}\forall_{x\in A}\left[ (x\in A_1\rightarrow x\notin A_2 \wedge x\in A_2\rightarrow x\notin A_1\right) \wedge (\exists_{f:A_1\to A_2} \text{f is injective and surjective}]$$   
$$\phi_A \wedge (\forall_{x\in A}\neg \phi_{A\setminus \{x\}})$$ expresses weakly even - I believe. However, I don't know how to express strong parity. Can you help me ?
 A: This is almost correct. You need, however, to rule out the possibility of $f(x)=x$; e.g. the following would work: $$\psi\wedge\exists F\forall x\forall y[(F(x)=y\implies x\not=y)\wedge(F(x)=y\implies F(y)=x)].$$

Another way to do this, which I think is kind of neat since it avoids invoking $\psi$, is the following. Say a set is weakly even if it is finite and of even size, or is infinite; basically, a set is even if it can be partitioned into pairs. Then a set $X$ is (genuinely) even iff $X$ is weakly even, and there is no element $x\in X$ such that $X\setminus \{x\}$ is also weakly even. But "weakly even" can be described similarly to what we've done above! So this yields an expression of "the universe is (finite and) even" in second-order logic, which doesn't involve $\psi$.
Interestingly, this second approach requires the axiom of choice! It is consistent with ZF (= set theory without choice) that there is an infinite set which can be partitioned into pairs, but which cannot be partitioned into pairs + one leftover element. So this is a sense in which the approach you've taken is better.

EDIT: Your expression does indeed describe weak evenness. And it's easy to tweak it to get strong evenness: just add $\psi$, as before.
