Combining that with OP article, the obstruction to showing hardness is therefore not technical but foundational- ie. the required axiom lies outside the standard minimal toolkit