predicate logic encoding of Post's Correspondence Problem

Hello,

I've been reading about Post's Correspondence Problem and I'd like to
find encodings of it in predicate logic. Thus far the closest I've
found to this was Ralf Treinen's paper "A New Method for Undecidability
Proofs of First Order Theories" -- but I'd like to see an encoding that
does not use functions (Treinen uses functions for encoding strings.)
Does anyone know of any relevant papers?

Thanks a lot!
--Yarden

.