論理におけるデータ抽象

論理学系（基礎論系？）の方が見てくださっている（かもしれない）うちにお尋ねしようと思ったのですが、論理において「データ抽象」みたいなものはあるんでしょうか。たとえば抽象型のあるプログラミング言語というか、多相λ計算の一種などでは

デカルト座標による複素数の実現M1と、極座標による複素数の実現M2が、適切な抽象型τにおいて文脈等価になる（τからboolへの任意の文脈Cにおいて、C[M1] →* true ⇔ C[M2] →* trueとなる）

などの結果が証明できるわけですが、（プログラミング言語ではなくて）論理でも同様の結果はあるのでしょうか？　もしあるとしたら、どういう手法で証明されているのでしょう。（プログラミング言語ではlogical relationやらbisimulationやら証明技法があって、僕のD論のテーマになったりしたのですが）