Searcharxiv⌕ Search

arXiv subjects

Merlin Carl

Publications and source records attributed to Merlin Carl.

At least 19 recordsLinked to original sources
arXiv2025

Reduction Complexities in Set Theory

In \cite{Ca2016} and \cite{Ca2018}, we introduced a notion of effective reducibility between set-theoretical $\Pi_{2}$-statements; in \cite{Ca2025}, this was extended to statements of arbitrary (potentially even infinite) quantifier complexity. We also considered a corresponding notion of Weihrauch reducibility, which allows only one call to the effectivizer of $\psi$ in a reduction of $\phi$ to $\psi$. In Stammes \cite{StammesMaster}, a considerably refined analysis through interpolating between these two notions was proposed, where one asks how many calls to an effectivizer for $\psi$ are required for effectivizing $\phi$. This allows us to make formally precise questions such as ``how many ordinals does one need to check for being cardinals in order to compute the cardinality of a given ordinal?'' and (partially) answer many of them. Many of these anwers turn out to be independent of ZFC.

math.LO↗
arXiv2024

A Note on Power-OTMs

We consider the computational strength of Power-OTMs, i.e., ordinal Turing machines equipped with a power set operator, and study a notion of realizability based on these machines. When parameters are allowed, these machines are, modulo access to a global well-ordering, equivalent to the Set Register Machines defined by Robert Passmann in \cite{Passmann}, and while most of the results on the realizability of Power-OTMs are analogous to results obtained by Passmann, the settings lead to different results concerning the axiom of choice. As we will see, the computational strength of power-OTMs can, depending on the set-theoretical background, also differ from that of Set Register Machines.

math.LO↗
arXiv2024

Effective Reducibility for Statements of Arbitrary Quantifier Complexity with Ordinal Turing Machines

This paper is an extended version of our work in \cite{Ca2025}. We extend the concept of effective reducibility between statements of set theory with ordinal Turing machines (OTMs) explored in \cite{Ca2018} for $\Pi_{2}$-statements to statements of arbitrary quantifier complexity in prenex normal form and use this to compare various fundamental set-theoretical principles, including the power set axiom, the separation scheme, the collection scheme and the replacement scheme and various principles related to the notion of cardinality, with respect to effective reducibility. This notion of reducibility is both different from (i.e., strictly weaker than) classical truth and from the OTM-realizability of the corresponding implications. Along the way, we obtain a computational characterization of HOD as the class of sets that are OTM-computable relative to every effectivizer of $\Sigma_{2}$-separation. We also consider an associated variant or Weihrauch reducibility.

math.LO↗
arXiv2024

Recognizable Realizability

We introduce a notion of realizability with ordinal Turing machines based on recognizability rather than computability, i.e., the ability to uniquely identify an object. We show that the arising concept of $r$-realizabilty has the property that all axioms of Kripke-Platek set theory are $r$-realizable and that the set of $r$-realizable statements is closed under intuitionistic provability.

math.LO↗
arXiv2024

Almost sure OTM-realizability

Combining the approaches made in works with Galeotti and Passmann, we define and study a notion of "almost sure" realizability with parameter-free ordinal Turing machines (OTMs). In particular, we show that, in contrast to the classical case, almost sure realizability differs from plain realizability, while closure under intuitionistic predicate logic and realizability of Kripke-Platek set theory continue to hold.

math.LO↗
arXiv2023

Improving the Diproche CNL through Autoformalization via Large Language Models

The Diproche system is an automated proof checker for texts written in a controlled fragment of German, designed for didactical applications in classes introducing students to proofs for the first time. The first version of the system used a controlled natural language for which a Prolog formalization routine was written. In this paper, we explore the possibility of prompting large language models for autoformalization in the context of Diproche, with encouraging first results.

cs.CL↗
arXiv2022

Countable ranks at the first and second projective levels

A rank is a notion in descriptive set theory that describes ranks such as the Cantor-Bendixson rank on the set of closed subsets of a Polish space, differentiability ranks on the set of differentiable functions in $C[0,1]$ such as the Kechris-Woodin rank and many other ranks in descriptive set theory and real analysis. The complexity of many natural ranks is $\Pi^1_1$ or $\Sigma^1_2$. We propose to understand the least length of ranks on a set as a measure of its complexity. Therefore, the aim is to understand which lengths such ranks may have. The main result determines the suprema of lengths of countable ranks at the first and second projective levels. Furthermore, we characterise the existence of countable ranks on specific classes of $\Sigma^1_2$ sets. The connections arising between $\Sigma^1_2$ sets with countable ranks on the one hand and $\Sigma^1_2$ Borel sets on the other lead to a conjecture that unifies several results in descriptive set theory such as the Mansfield-Solovay theorem and a recent result of Kanovei and Lyubetsky.

math.LO↗
arXiv2022

The strange world of transfinite Melodies -- Recognizability for weak and strong infinite time $\alpha$-register machines

For exponentially closed ordinals $\alpha$, we consider recognizability of constructible subsets of $\alpha$ for $\alpha$-(w)ITRMs and their distribution in the constructible hierarchy. In particular, for $\alpha$-ITRMs, we show that, there are lost melodies that are recognizable without parameters for all $\alpha$, that the iterated recognizability is absolute between $L$ and $V$ for most values of $\alpha$ and generalize "all or nothing"-phenomenon known from ITRMs occurs for a proper class of $\alpha$. For $\alpha$-wITRMs, we offer a complete characterization of those $\alpha$ for which lost melodies exist and that the relation between the sets of computable and recognizable subsets of $\alpha$ varies wildly, depending on $\alpha$: The computable sets may be included among the recognizable sets (which is usually the case in ordinal computability), but there are also class many values of $\alpha$ for which the set of recognizable sets is empty and such for which the set of recognizable sets is non-empty, but disjoint from the set of computable sets. %for class many values of $\alpha$, the sets of $\alpha$-wITRM-computable and $\alpha$-wITRM-recognizable subsets of $\alpha$ are both non-empty, but disjoint, and, also for class many values of $\alpha$, the set of $\alpha$-wITRM-recognizable subsets of $\alpha$ is empty. This paper is an extension of our paper in the CiE 2023 proceedings.

math.LO↗
arXiv2022

Natural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diproche

We present and analyze the employment of the Diproche system, a natural language proof checker, within a one-semester mathematics beginners lecture with 228 participants. The system is used to check the students' solution attempts to proving exercises in Boolean set theory and elementary number theory and to give them immediate feedback. The benefits of the employment of the system are assessed via a questionnaire at the end of the semester and via analyzing the solution attempts of a subgroup of the students. Based on our results we develop approaches for future improvements.

cs.LO↗
arXiv2021

What is worthy of investigation? Philosophical attitudes and their impact on mathematical development by the example of discovering 10-adic numbers

We describe in dialogue form a possible way of discovering and investigating 10-adic numbers starting from the naive question about a `largest natural number'. Among the topics we pursue are possibilities of extensions to transfinite 10-adic numbers, 10-adic representations of rational numbers, zero divisors, square roots and 10-adic roots of higher degree of natural numbers, and applications of 10-adic number representation in computer arithmetic. The participants of the dialogue are idealized embodiments of different philosophical attitudes towards mathematics. The article aims at illustrating how these attitudes interact, in both jarring and stimulating ways, and how they impact mathematical development.

math.NT↗
arXiv2021

Lower bounds on $\beta(\alpha)$ and other properties of $\alpha$-ITRMs

This paper extends our paper \cite{C2} for the conference ``Computability in Europe'' 2022. After Infinite Time Turing Machines (ITTM) were introduced in Hamkins and Lewis \cite{HL}, a number of machine models of computability have been generalized to the transfinite, along with various variants thereof. While for some of these models the computational strength has been successfully determined, there are still several white spots on the map of transfinite computability. In this paper, we contribute to the understanding of the computational strength of transfinite machine models by (i) proving lower bounds on the computational strength of $\alpha$-Infinite Time Register Machines ($\alpha$-ITRMs) for certain values of $\alpha$, refuting a conjecture about their strength made in \cite{alpha itrms}, (ii) showing that the computational strength of cardinal-recognizing ITRMs is equal to that of ITRMs and (iii) showing that non-solvability of the bounded halting problem, existence of a universal machine and an increase of computational power by allowing machines to recognize cardinals are equivalent for $\alpha$-ITRMs for all relevant values of $\alpha$ .

math.LO↗
arXiv2021

Randomising Realisability

We consider a randomised version of Kleene's realisability interpretation of intuitionistic arithmetic in which computability is replaced with randomised computability with positive probability. In particular, we show that (i) the set of randomly realisable statements is closed under intuitionistic first-order logic, but (ii) different from the set of realisable statements, that (iii) "realisability with probability 1" is the same as realisability and (iv) that the axioms of bounded Heyting's arithmetic are randomly realisable, but some instances of the full induction scheme fail to be randomly realisable.

math.LO↗
arXiv2020

Decision times of infinite computations

The decision time of an infinite time algorithm is the supremum of its halting times over all real inputs. The decision time of a set of reals is the least decision time of an algorithm that decides the set; semidecision times of semidecidable sets are defined similary. It is not hard to see that $\omega_1$ is the maximal decision time of sets of reals. Our main results determine the supremum of countable decision times as $\sigma$ and that of countable semidecision times as $\tau$, where $\sigma$ and $\tau$ denote the suprema of $\Sigma_1$- and $\Sigma_2$-definable ordinals, respectively, over $L_{\omega_1}$. We further compute analogous suprema for singletons.

math.LO↗
arXiv2020

Realisability for Infinitary Intuitionistic Set Theory

We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.

math.LO↗
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_{\omega_{1}^{\text{CK}}}$ at which new real numbers appear at all.

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

Number Theory and Axiomatic Geometry in the Diproche System

Diproche ("Didactical Proof Checking") is an automatic system for supporting the acquistion of elementary proving skills in the initial phase of university education in mathematics. A key feature of Diproche - which is designed by the example of the Naproche system developed by M. Cramer and others - is an automated proof checker for proofs written in a controlled fragment of natural language specifically designed to capture the language of beginners' proving exercises in mathematics. Both the accepted language and proof methods depend on the didactical and mathematical context and vary with the level of education and the topic proposed. An overall presentation of the system in general was given in Carl and Krapf 2019. Here, we briefly recall the basic architecture of Diproche and then focus on explaining key features and the working principles of Diproche in the sample topics of elementary number theory and axiomatic geometry.

math.LO↗