The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms.
Lets consider the simple case where the terms
N are free variables,
M = x and
N = y. Choosing the program context
C[-] = (λxy.[-]) v w we have,
C[M] = (λxy.x) v w →* v
C[N] = (λxy.y) v w →* w
So by definition
N wouldn't be observationally equivalent.
However, consider any adequate denotational semantics of PCF. Then by definition of adequacy,
⟦M⟧ = ⟦N⟧ implies
N observationally equivalent. The denotations of both (open) terms are,
⟦M⟧ = ⟦x ⊢ x⟧ = id
⟦N⟧ = ⟦y ⊢ y⟧ = id
From what we conclude
N to be observationally equivalent.
So, surely I must be going wrong somewhere, and I suspect it to be some trivial mistake. But where?