[suyjuris]

> It is of course possible to construct a problem that will require strictly more steps than the most efficient algorithm for SAT; for example, we could give a language SAT-PRIME = {<φ,n>: φ is satisfiable and n is prime}, which will take longer to decide than SAT.

A minor point, admittedly, but the second part of this statement is not true. Running time is w.r.t. the length of the input, and <φ,n> is longer than just φ. Deciding whether n is prime is easy, so per bit of input the algorithm is faster.

[eynsham]

Oh, you’re right! Well, hm, how about SAT-PRIME' = {φ: φ is satisfiable and its Gödel number (under some scheme) has [some property]}.

[suyjuris]

I would guess that this can work, but it seems impossible to prove. I do not have any good candidates for an NP problem that is provably harder than SAT for a deterministic Turing machine, though I would not be surprised if some tricky diagonalisation argument works.