Given a set of pairs of words $P = \{(\alpha_1, \beta_1), \dots, (\alpha_n, \beta_n)\} \subseteq \Sigma^*\times\Sigma^*$, the Post Correspondence Problem (PCP) is to decide wether or not there are indices $i_1, \dots, i_k \in \{1\dots n\}$ such that $\alpha_{i_1}\cdot \dots \cdot \alpha_{i_k} = \beta_{i_1}\cdot \dots \cdot \beta_{i_k}$.
It is well known that PCP is not computable in any Turing-equivalent machine model. Usually, this fact is proven by reducing the Halting Problem (HP) to PCP, i.e. describing how to create a PCP instance $\Pi$ for an arbitrary Turing machine $M$ and an input $x$ such that $\Pi$ has a solution if and only if $M$ terminates on $x$.
Arguably, undecidability of PCP is more useful than of HP because it is removed from the notion of computation itself and therefore might be understood without having to read up on Turing machines (or equivalent models) first. Also, it is a more natural choice for many reduction proofs for not computation-related problems, e.g. in formal language theory.
It seems only fair to ask:
Is there a proof for undecidability of PCP that does not employ reduction to HP (or similar problems)?
Note that I want to exclude chains of reductions that end up at HP in the end. Having such an independent proof might open up new ways for students and laymen to understand the underlying issues. Failing that, are there reasons for that lack? Do we need the kind of self-applicability we employ when proving HP not to be computable?
PS: I was unsure wether or not this question should go here or rather onto math.SE. As the proper place might depend on the level of answers, I went with the specialist community.