Some Consequences of Cryptographical Conjectures forS12and EF

We show that there is a pair of disjoint NP-sets, whose disjointness is provable inS12and which cannot be separated by a set in P/poly, if the cryptosystem RSA is secure. Further we show that factoring and the discrete logarithm are implicitly definable in any extension ofS12admitting an NP-definition of primes about which it can prove that no number satisfying the definition is composite. As a corollary we obtain that the Extended Frege (EF) proof system does not admit a feasible interpolation theorem unless the RSA cryptosystem is not secure and that an extension of EF by tautologiesτp(pprimes), formalizing thatpis not composite, as additional axioms do not admit a feasible interpolation theorem unless factoring and the discrete logarithm are in P/poly.