Proposition. If two computability models are equivalent, then decidable equality exists for one iff another has one [math-0L0G]

2024-07-22 · Lîm Tsú-thuàn

若 AA 跟 BB model 等價 A≃BA \simeq B，則 AA 有 decidable equality 若且唯若 BB 也有 decidable equality。

Proof [local-0]

先假設 AA 中有一 decidable equality =A=_A，這表示

=A⋅a1⋅a2={trueAa1=a2falseAotherwise=_A \cdot a_1 \cdot a_2 = \begin{cases} \text{true}_A \quad a_1 = a_2 \\ \text{false}_A \quad \text{otherwise} \end{cases}

對所有 a1,a2∈Aa_1, a_2 \in A 成立。由於 A≃BA \simeq B，所以對每個元素 a∈Aa \in A 必有一個 b∈Bb \in B 追蹤 aa，所以我們用 =B,b1,b2,trueB,falseB=_B, b_1, b_2, \text{true}_B, \text{false}_B 對應地表示這個關係。那麼我們有

=B⋅b1⋅b2={trueBb1=b2falseBotherwise=_B \cdot b_1 \cdot b_2 = \begin{cases} \text{true}_B \quad b_1 = b_2 \\ \text{false}_B \quad \text{otherwise} \end{cases}

顯然 BB 也有一個 decidable equality =B=_B。由於論證對 A,BA,B 沒有特別要求，這個證明是對稱的，因此兩個方向都證明完畢。