Expressibility in the elementary theory of recursively enumerable sets with realizability logic (Q1097266)

Let \({\mathcal L}+{\mathcal W}\) denote the first-order language obtained from \({\mathcal L}=<\emptyset,N,\cup,\cap,'>\) by adding the symbols \(w_ 0,w_ 1,..\). as constants. The author defines the relation e r \({\mathfrak A}\) (``the integer e realizes the closed formula \({\mathfrak A}'')\). Let \({\mathcal E}_ r\) be the set of all realizable formulae of \({\mathcal L}\). A predicate \(P(X_ 1,...,X_ n)\) is said to be expressible in \({\mathcal L}\) if there is a formula \({\mathfrak A}(X_ 1,...,X_ n)\) of \({\mathcal L}\) such that \({\mathfrak A}(W_{i_ 1},...,W_{i_ n})\) is realizable if and only if \(P(W_{i_ 1},...,W_{i_ n})=t\). The author proves that the predicates ``X is finite'', ``X and Y are finite and \(| X| <| Y| ''\), \(``| X| +| Y| =| Z| ''\), \(``| X| \cdot | Y| =| Z| ''\), ``X and Y are finite and \(| X| \leq_ 1| Y| ''\) are expressible. This allows him first to embed arithmetic in \({\mathcal E}_ r\) and secondly to obtain a complete characterization of the class of all predicates expressible in \({\mathcal E}_ r\). Namely, a predicate is expressible in \({\mathcal E}_ r\) if and only if it is recursively invariant. The proofs of all these results are simple and elegant. The main regrettable feature of the paper is its completeness. The author has not left any work for other mathematicians.