Search arXivSearch

arXiv · 2507.03827

Abstract computation over first-order structures. Part IIb: Moschovakis' operator and other non-determinisms

Abstract

BSS RAMs were introduced to provide a mathematical framework for characterizing algorithms over first-order structures. Non-deterministic BSS RAMs help to model different non-deterministic approaches. Here, we deal with different types of binary non-determinisms and study the consequences of the decidability of the identity relation and the decidability of finite sets consisting of one or two constants. We compare the binary non-determinism resulting from a non-deterministic branching process, the digital non-determinism resulting from the restriction of guesses to two constants, and some other non-determinisms resulting from the use of Moschovakis' operator applied to oracle sets restricted to tuples of constants. Moreover, we show that the performance capability and the efficiency of individual machines are influenced by the following properties. 1. The identity relation belongs to the underlying structure. 2. The identity is semi-decidable over the underlying structure. 3. Two single-element sets of constants are semi-decidable. 4. A set of two constants is semi-decidable. The order of these properties corresponds to the strength of their influence. In all cases mentioned, the semi-decidability of the sets implies their decidability.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Christine Gaßner. 2025-10-29. Abstract computation over first-order structures. Part IIb: Moschovakis' operator and other non-determinisms. https://arxiv.org/abs/2507.03827

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Bluebirds and mockingbirds cannot produce a fixed-point combinator

Let $B$ be the bluebird combinator with reduction rule $Bxyz \to_{w} x\left(yz\right)$, let $M$ be the mockingbird combinator with reduction rule $Mx \to_{w} xx$, and let $I$ be the identity bird combinator with reduction rule $Ix \to_{w} x$. A fixed-point combinator, called a sage bird by Smullyan, is a closed term $Y$ such that, for a fresh variable $x$, $Yx$ is equivalent to $x\left(Yx\right)$ under these reduction rules. For a fixed variable $x$, we construct an invariant $\mathrm{Tr}_{x}\left(u\right)$ of a $BMI$-term $u$ with respect to $\to_{w}$. This invariant traces the occurrences of $x$ in the leftmost-innermost reduction sequence of $u$. We then prove that $\mathrm{Tr}_{x}\left(Yx\right) \neq \mathrm{Tr}_{x}\left(x^{r}\left( Yx \right)\right)$ for every $x$-free $BMI$-term $Y$ and every $r\geq 1$. Consequently, there exists no fixed-point combinator in $BMI$-combinatory logic. This provides a negative answer to the problem posed by Smullyan in 1985.

math.LO

Pointwise provable equality and the failure of composition

Montagna (1989) and Di Paola--Montagna (1991) claim that the algebraic systems $S'$ and $S'_T$, respectively, are categories. We show that the proposed composition is not independent of the choice of representatives. For every consistent recursively enumerable extension $T$ of Peano arithmetic ($\mathrm{PA}$), we exhibit two program indices that are pointwise provably equal in $T$ but yield inequivalent composites when each is run after the same program. Montagna's $S'$ is the case $T=\mathrm{PA}$. The failure already occurs for partial maps from $ω$ to itself. Weak totality and the proposed range assignment also depend on the choice of representatives. More generally, for consistent $T\supseteq\mathrm{PA}$, pointwise provable equality is a composition congruence exactly when $T$ proves every true $Π^0_1$ sentence, in which case it is extensional equality. This completeness condition fails for every consistent recursively enumerable $T\supseteq\mathrm{PA}$ by Gödel's second incompleteness theorem. For every extension $T\supseteq\mathrm{PA}$, the least composition congruence containing pointwise provable equality is extensional equality if $T$ is $Σ^0_1$-sound and the universal relation otherwise.

math.LO

Compactness via Consistency Properties

We will use consistency properties to characterize strongly compact cardinals, first showing an adequate Model Existence Theorem for larger fragments.

math.LO