Decidability of Scott's model as an ordered ℚ-vectorspace
Miklós Erdélyi‐Szabó · Journal of Symbolic Logic · 1997
Abstract Let L = 〈<, +, hq, 1〉q∈ℚ where ℚ is the set of rational numbers and hq is a one-place function symbol corresponding to multiplication by q. Then the L-theory of Scott's model for intuitionistic analysis is decidable.