By definition:
A polynomial-time computable function $f:$ $\{$0,1$\}$$^*$→ $\{$0,1$\}$$^*$ is a one-way function if for every probabilistic polynomial time Turing Machine $PTM$ there is a neglegibible function $E$ $:$$\mathbb{N} → \mathbb{N} $ $ \ s.t. \ $ $Pr$ $x$ $∈$ $\{$0,1$\}$$^n$ $[PTM \ \ inverts \ \ f(x)] ≤ E(n)$.
Now, reading the definition above, the existence of one-way functions seems like an easy bet, however it is considered a stronger assumption than $P \neq NP$. Apparently proving the existence of these functions would be more difficult than proving $P = NP ?$ And I'd like to know the technical reasons for this, does it have something to do with the "for every" in the definition?
What steps would a mathematician or computer scientist take to prove that one-way functions exist? I believe that since proving its existence would also prove $P \neq NP$, this means that we cannot use the techniques that we know for sure does not work: Relativization, diagonalization, Natural Proof.
So, what form could such a proof take? Maybe something in second(+)-order logic?