/sci/ - Science & Math

I'm trying to phrase the uncountability of PN in second order arithmetic - can you verify my thinking...

Naturally, I phrase it as non-existence of a bijection between N and (N->{0,1}), which we can uncurry to (N x N) -> {0,1}.
We can speak about those as functions by applying a pairing n->(k,m) twice (those functions are encoded as subsets of N and thus we're still second order).
Now I just need to express the bijection property.

A bijectionN N->{0,1}) as encoded by ((N x N) x {0,1}) means

for all m,n, if
??? profit ???
then m=n
I still need to figure out the ??? part in terms of triples

[I couldn't find anything on Cantor diagonalization without set theory]