Effective choice operations on constructive and positive models (Q1317639): Difference between revisions

The author considers some computable enumeration of all possible r.e. subdiagrams in a finite language. This enumeration generates some natural enumeration of constructivizations and positive enumerations of modeles. The author poses questions like this: When, given a number of a positive enumeration of a fixed model \(M\), can one uniformly find an algorithm to enumerate a relation \(R\) with respect to this enumeration? More precisely, he gives a definition of (weakly) effective choice operation, which is some version of an effective extensional recursive operator on r.e. sets, and shows the above property to be equivalent to definability of \(R\) by \(\Sigma^ r_ 1\)-formulas: Theorem. For a relation \(R\) on \(M\) with a positive enumeration, there is a (weakly) effective choice operation of an r.e. set if and only if \(R\) is positively \(\Sigma^ r_ 1\)-definable on \(M\) (with a finite sequence of parameters). A similar result is proved for constructivizable models and the choice operation of a characteristic function for recursive relations. The author also proves these results are not valid without requirement of extensionality for operators.