A remark on pseudo proof systems and hard instances of the satisfiability problem

We link two concepts from the literature, namely hard sequences for the satisfiability problem sat and so‐called pseudo proof systems proposed for study by Krajíček. Pseudo proof systems are elements of a particular nonstandard model constructed by forcing with random variables. We show that the existence of mad pseudo proof systems is equivalent to the existence of a randomized polynomial time procedure with a highly restrictive use of randomness which produces satisfiable formulas whose satisfying assignments are probably hard to find.