Searcharxiv⌕ Search

arXiv subjects

Merlin Carl

Publications and source records attributed to Merlin Carl.

At least 37 records · Page 2Linked to original sources
arXiv2020

The Lost Melody Theorem for Infinite Time Blum-Shub-Smale Machines

We consider recognizability for Infinite Time Blum-Shub-Smale machines, a model of infinitary computability introduced in Koepke and Seyfferth [KS]. In particular, we show that the lost melody theorem (originally proved for ITTMs in Hamkins and Lewis [HL]), i.e. the existence of non-computable, but recognizable real numbers, holds for ITBMs, that ITBM-recognizable real numbers are hyperarithmetic and that both ITBM-recognizable and ITBM-unrecognizable real numbers appear at every level of the constructible hierarchy below $L_{ω_{1}^{\text{CK}}}$ at which new real numbers appear at all.

math.LO↗
arXiv2020

Space-Bounded OTMs and REG$^{\infty}$

An important theorem in classical complexity theory is that LOGLOGSPACE=REG, i.e. that languages decidable with double-logarithmic space bound are regular. We consider a transfinite analogue of this theorem. To this end, we introduce deterministic ordinal automata (DOAs), show that they satisfy many of the basic statements of the theory of deterministic finite automata and regular languages. We then consider languages decidable by an ordinal Turing machine (OTM), introduced by P. Koepke in 2005 and show that if the working space of an OTM is of strictly smaller cardinality than the input length for all sufficiently long inputs, the language so decided is also decidable by a DOA.

math.LO↗
arXiv2020

Automatized Evaluation of Formalization Exercises in Mathematics

We describe two systems for supporting beginner students in acquiring basic skills in expressing statements in the formalism of first-order predicate logic; the first, called "math dictations", presents users with the task of formalizing a given natural-language sentence, while the second, called "Game of Def", challenges users to give a formal description of a set of a geometric pattern displayed to them. In both cases, an automatic checking takes place.

math.LO↗
arXiv2020

Taming Koepke's Zoo II: Register Machines

We study the computational strength of resetting $α$-register machines, a model of transfinite computability introduced by P. Koepke in \cite{K1}. Specifically, we prove the following strengthening of a result from \cite{C}: For an exponentially closed ordinal $α$, we have $L_α\models$ZF$^{-}$ if and only if COMP$^{\text{ITRM}}_α=L_{α+1}\cap\mathfrak{P}(α)$, i.e. if and only if the set of $α$-ITRM-computable subsets of $α$ coincides with the set of subsets of $α$ in $L_{α+1}$. Moreover, we show that, if $α$ is exponentially closed and $L_α\not\models$ZF$^{-}$, then COMP$^{\text{ITRM}}_α=L_{β(α)}\cap\mathfrak{P}(α)$, where $β(α)$ is the supremum of the $α$-ITRM-clockable ordinals, which coincides with the supremum of the $α$-ITRM-computable ordinals. We also determine the set of subsets of $α$ computable by an $α$-ITRM with time bounded below $δ$ when $δ>α$ is an exponentially closed ordinal smaller than the supremum of the $α$-ITRM-clockable ordinals. Moreover, we obtain some sufficient and necessary conditions on ordinals $α$ for which the $α$-wITRM-clockable ordinals are bounded by $α$.

math.LO↗
arXiv2020

Reachability for infinite time Turing machines with long tapes

Infinite time Turing machine models with tape length $α$, denoted $T_α$, strengthen the machines of Hamkins and Kidder [HL00] with tape length $ω$. A new phenomenon is that for some countable ordinals $α$, some cells cannot be halting positions of $T_α$ given trivial input. The main open question in [Rin14] asks about the size of the least such ordinal $δ$. We answer this by providing various characterizations. For instance, $δ$ is the least ordinal with any of the following properties: (a) For some $ξ<α$, there is a $T_ξ$-writable but not $T_α$-writable subset of $ω$. (b) There is a gap in the $T_α$-writable ordinals. (c) $α$ is uncountable in $L_{λ_α}$. Here $λ_α$ denotes the supremum of $T_α$-writable ordinals, i.e. those with a $T_α$-writable code of length $α$. We further use the above characterizations, and an analogue to Welch's submodel characterization of the ordinals $λ$, $ζ$ and $Σ$, to show that $δ$ is large in the sense that it is a closure point of the function $α\mapsto Σ_α$, where $Σ_α$ denotes the supremum of the $T_α$-accidentally writable ordinals.

math.LO↗
arXiv2020

Resetting Infinite Time Blum-Shub-Smale-Machines

In this paper, we study strengthenings of Infinite Times Blum-Shub-Smale-Machines (ITBMs) that were proposed by Seyfferth in [14] and Welch in [15] obtained by modifying the behaviour of the machines at limit stages. In particular, we study Strong Infinite Times Blum-Shub-Smale-Machines (SITBMs), a variation of ITBMs where lim is substituted by lim inf in computing the content of registers at limit steps. We will provide lower bounds to the computational strength of such machines. Then, we will study the computational strength of restrictions of SITBMs whose computations have low complexity. We will provide an upper bound to the computational strength of these machines, in doing so we will strenghten a result in [15] and we will give a partial answer to a question posed by Welch in [15].

math.LO↗
arXiv2020

Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics

The Diproche system, an automated proof checker for natural language proofs specifically adapted to the context of exercises for beginner's students similar to the Naproche system by Koepke, Schröder, Cramer and others, uses a modification of an automated theorem prover which uses common formal fallacies intead of sound deduction rules for mistake diagnosis. We briefly describe the concept of such an `Anti-ATP' and explain the basic techniques used in its implementation.

cs.AI↗
arXiv2019

Space and Time Complexity for Infinite Time Turing Machines

We consider notions of space complexity for Infinite Time Turing Machines (ITTMs) that were introduced by B. Löwe and studied further by J. Winter. We answer several open questions about these notions, among them whether low space complexity implies low time complexity (it does not) and whether one of the equalities P=PSPACE, P$_{+}=$PSPACE$_{+}$ and P$_{++}=$PSPACE$_{++}$ holds for ITTMs (all three are false). We also show various separation results between space complexity classes for ITTMs. This considerably expands our earlier observations on the topic in section 7.2.2 of \cite{Ca2}, which appear here as Lemma $6$ up to Corollary $9$.

math.LO↗
arXiv2019

A Note on Clockability for Ordinal Turing Machines

We study clockability for Ordinal Turing Machines (OTMs). In particular, we show that, in contrast to the situation for ITTMs, admissible ordinals can be OTM-clockable, that $Σ_{2}$-admissible ordinals are never OTM-clockable and that gaps in the OTM-clockable ordinals are always started by admissible limits of admissible ordinals.

math.LO↗
arXiv2019

A transfer principle for second-order arithmetic, and applications

In the theory of conditional sets, many classical theorems from areas such as functional analysis, probability theory or measure theory are lifted to a conditional framework, often to be applied in areas such as mathematical economics or optimization. The frequent experience that such theorems can be proved by `conditionalizations' of the classical proofs suggests that a general transfer principle is in the background, and that formulating and proving such a transfer principle would yield a wealth of useful further conditional versions of classical results, in addition to providing a uniform approach to the results already known. In this paper, we formulate and prove such a transfer principle based on second-order arithmetic, which, by the results of reverse mathematics, suffices for the bulk of classical mathematics, including real analysis, measure theory and countable algebra, and excluding only more remote realms like category theory, set-theoretical topology or uncountable set theory, see e.g. the introduction of \cite{simpson2009subsystems}.This transfer principle is then employed to give short and easy proofs of conditional versions of central results in various areas of mathematics, including theorems which have not been proven by hand previously such as Peano existence theorem, Urysohn's lemma and the Markov-Kakutani fixed point theorem. Moreover, we compare the interpretation of certain structures in a conditional model with their meaning in a standard model.

math.LO↗
arXiv2018

Effectivity and Reducibility with Ordinal Turing Machines

This article expands our work in [Ca16]. By its reliance on Turing computability, the classical theory of effectivity, along with effective reducibility and Weihrauch reducibility, is only applicable to objects that are either countable or can be encoded by countable objects. We propose a notion of effectivity based on Koepke's Ordinal Turing Machines (OTMs) that applies to arbitrary set-theoretical $Π_{2}$-statements, along with according variants of effective reducibility and Weihrauch reducibility. As a sample application, we compare various choice principles with respect to effectivity. We also propose a generalization to set-theoretical formulas of arbitrary quantifier complexity.

math.LO↗
arXiv2018

Some Observations on Infinitary Complexity

Continuing the study of complexity theory of Koepke's Ordinal Turing Machines (OTMs) that was started by Rin, Löwe and the author, we prove the following results: (1) An analogue of Ladner's theorem for OTMs holds: That is, there are languages $\mathcal{L}$ which are NP$^{\infty}$, but neither P$^{\infty}$ nor NP$^{\infty}$-complete. This answers an open question of \cite{CLR}. (2) The speedup theorem for Turing machines, which allows us to bring down the computation time and space usage of a Turing machine program down by an aribtrary positive factor under relatively mild side conditions by expanding the working alphabet does not hold for OTMs. (3) We show that, for $α<β$ such that $α$ is the halting time of some OTM-program, there are decision problems that are OTM-decidable in time bounded by $|w|^β\cdotγ$ for some $γ\in\text{On}$, but not in time bounded by $|w|^α\cdotγ$ for any $γ\in\text{On}$.

math.LO↗
arXiv2017

Infinite Time Recognizability from Random Oracles and the Recognizable Jump Operator

By a theorem of Sacks, if a real $x$ is recursive relative to all elements of a set of positive Lebesgue measure, $x$ is recursive. This statement, and the analogous statement for non-meagerness instead of positive Lebesgue measure, have been shown to carry over to many models of transfinite computations. Here, we start exploring another analogue concerning recognizability rather than computability. We introduce a notion of relativized recognizability and show that, for Infinite Time Turing Machines (ITTMs), if a real $x$ is recognizable relative to all elements of a non-meager Borel set $Y$, then $x$ is recognizable. We also show that a relativized version of this statement holds for Infinite Time Register Machines (ITRMs). This extends our earlier work where we obtained the (unrelativized) result for ITRMs. We then introduce a jump operator for recognizability, examine its set-theoretical content and show that the recognizable jumps for ITRMs and ITTMs are primitive-recursively equivalent, even though these two models are otherwise of vastly different strength. Finally, we introduce degrees of recognizability by considering the transitive closure of relativized recognizability and connect it with the recognizable jump operator to obtain a solution to Post's problem for degrees of recognizability.

math.LO↗
arXiv2016

Randomness via infinite computation and effective descriptive set theory

We study randomness beyond $Π^1_1$-randomness and its Martin-Löf type variant, introduced in \cite{MR2340241} and further studied in \cite{Continuous-higher-randomness}. The class given by the infinite time Turing machines (\ITTM s), introduced by Hamkins and Kidder, is strictly between $Π^1_1$ and $Σ^1_2$. We prove that the natural randomness notions associated to this class have several desirable properties resembling those of the classical random notions such as Martin-Löf randomness, and randomness notions defined via effective descriptive set theory such as $Π^1_1$-randomness. For instance, mutual randoms do not share information and can be characterized as in van Lambalgen's theorem. We also obtain some differences to the hyperarithmetic setting. Already at the level of $Σ^1_2$, some properties of randomness notions are independent \cite{Infinite-computations}. Towards the results about randomness, we prove the following analogue to a theorem of Sacks. If a real is infinite time Turing computable relative to all reals in some given set of reals with positive Lebesgue measure, then it is already infinite time Turing computable. As a technical tool, we prove facts of independent interest about random forcing over admissible sets and increasing unions of admissible sets. These results are also useful for more efficient proofs of some classical results about hyperarithmetic sets.

math.LO↗
arXiv2016

On the Value Group of a Model of Peano Arithmetic

We investigate $IPA$ - real closed fields, that is, real closed fields which admit an integer part whose non-negative cone is a model of Peano Arithmetic. We show that the value group of an $IPA$ - real closed field is an exponential group in the residue field, and that the converse fails in general. As an application, we classify (up to isomorphism) value groups of countable recursively saturated exponential real closed fields. We exploit this characterization to construct countable exponential real closed fields which are not $IPA$ - real closed fields.

math.LO↗
arXiv2016

Structures Associated with Real Closed Fields and the Axiom of Choice

An integer part I of a real closed field K is a discretely ordered subring with minimal element 1 such that, for every x in K, I contains some i such that x is between i and i+1 in the ordering of K. Mourgues and Ressayre showed that every real closed field has an integer part. Their construction implicitely uses the axiom of choice. We show that the axiom of choice is actually necessary to obtain the result by constructing a transitive model of ZF (i.e. set theory without the axiom of choice) which contains a real closed field without an integer part. Then we analyze some cases where the axiom of choice is not necessary for obtaining an integer part. An integer part I of a real closed field K is a discretely ordered subring of K with minimal positive element 1 such that, for every x in K, I contains some i such that x is between i and i+1 in the ordering of K. Mourgues and Ressayre showed that every real closed field has an integer part. Their construction implicitly uses the axiom of choice. We show that the axiom of choice is actually necessary to obtain the result by constructing a transitive model of ZF (i.e. set theory without the axiom of choice) which contains a real closed field without an integer part. Then we analyze some cases where the axiom of choice is not necessary for obtaining an integer part. On the way, we demonstrate that a class of questions containing the question whether the axiom of choice is necessary for the proof of a certain ZFC-theorem is algorithmically undecidable. We further apply the methods to show that it is independent of ZF whether every real closed field has a value group section and a residue field section. This also sheds some light on the possibility to effectivize constructions of integer parts.

math.LO↗
arXiv2016

Generalized Effective Reducibility

We introduce two notions of effective reducibility for set-theoretical statements, based on computability with Ordinal Turing Machines (OTMs), one of which resembles Turing reducibility while the other is modelled after Weihrauch reducibility. We give sample applications by showing that certain (algebraic) constructions are not effective in the OTM-sense and considerung the effective equivalence of various versions of the axiom of choice.

math.LO↗