arXiv subjects

Franziskus Wiesnet

Publications and source records attributed to Franziskus Wiesnet.

8 recordsLinked to original sources

arXiv2026

On the Limits of Recursive Characterizations in the Refined $A$-Translation

This paper studies the limits of recursive classifications in proof theory and program extraction, using the refined $A$-translation as a central example. The refined $A$-translation, due to Berger, Buchholz, and Schwichtenberg, is based on recursively defined classes of formulas in minimal arithmetic $\mathsf{MA}^ω$, in particular the classes of definite and goal formulas. One of its basic properties is that $D[\bot := F] \to D$ is derivable for every definite formula $D$. Schwichtenberg and Wainer observed that this property also holds for formulas outside the class of definite formulas and asked for a useful characterization of all formulas $D$ for which $D[\bot := F] \to D$ is derivable. In addition to definite formulas, the refined $A$-translation involves three further classes of formulas satisfying related properties. We show that none of these four properties admits a recursive characterization. In addition to this negative result, we extend the framework of refined $A$-translation in two directions. First, we add conjunction $\wedge$ to the language of $\mathsf{MA}^ω$, whose original formulation contains only the logical connectives $\forall$ and $\to$, and adapt the formula classes accordingly. Second, we present the corresponding slightly extended formulation of the refined $A$-translation theorem and discuss possible recursive extensions of these classes. Finally, we discuss a prover written in Rust which implements the theory $\mathsf{MA}^ω$ and the four formula classes. The prover is not used as a formal verification of the results, but serves as a case study for examining Rust as a programming language for proof assistants. We highlight some advantages and drawbacks of Rust in this setting, including its type system, support for partial constructions, ownership and borrowing model, modularity, and testing infrastructure.

math.LO↗

arXiv2026

Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives

This article revisits standard theorems from elementary number theory from a constructive, algorithmic, and proof-theoretic perspective, framed within the theory of computable functionals TCF. Key examples include Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorisation method. All definitions and theorems are fully formalised in the proof assistant Minlog, laying the foundation for a comprehensive formal framework for number theory within Minlog. While formalisation guarantees correctness, the primary emphasis is on the computational content of proofs. Leveraging Minlog's built-in program extraction, we obtain executable terms and export them as Haskell code. The efficiency of the extracted programs plays a central role. We show how performance considerations influence even the original formulation of theorems and proofs. In particular, we compare formalisations based on binary encodings of natural numbers with those using the traditional unary (successor-based) representation. We present several core proofs in detail and reflect on the challenges that arise from formalisation in contrast to informal reasoning. The complete formalisation is available online and linked throughout. Minlog's tactic scripts are designed to follow the structure of natural-language proofs, allowing each derivation step to be traced precisely and thereby bridging the gap between formal and classical mathematical reasoning.

math.LO↗

arXiv2025

Material Interpretation and Constructive Analysis of Maximal Ideals in $\mathbb{Z}[X]$

This article presents the concept of material interpretation as a method to transform classical proofs into constructive ones. Using the case study of maximal ideals in $\mathbb{Z}[X]$, it demonstrates how a classical implication $A \to B$ can be rephrased as a constructive disjunction $\neg A \vee B$, with $\neg A$ representing a strong form of negation. The approach is based on on Gödel's Dialectica interpretation, the strong negation, and potentially Herbrand disjunctions. The classical proof that every maximal ideal in $\mathbb{Z}[X]$ contains a prime number is revisited, highlighting its reliance on non-constructive principles such as the law of excluded middle. A constructive proof is then developed, replacing abstract constructs with explicit case distinctions and direct computations in $\mathbb{Z}[X]$. This proof clarifies the logical structure and reveals computational content. The article discusses broader applications, such as Zariski's Lemma, Hilbert's Nullstellensatz, and the Universal Krull-Lindenbaum Lemma, with an emphasis on practical implementation using tools such as Python and proof assistants. The material interpretation offers a promising framework for bridging classical and constructive mathematics, enabling algorithmic implementations.

math.LO↗

arXiv2025

Limits with Signed Digit Streams

We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. The main objective of this paper is an algorithm which takes a sequence of signed digit representations of reals and returns the signed digit representation of their limit, if the sequence converges. As a first application we use this algorithm together with Heron's method to build up an algorithm which converts the signed digit representation of a non-negative real number into the signed digit representation of its square root. Instead of writing the algorithms first and proving their correctness afterwards, we work the other way round, in the tradition of program extraction from proofs. In fact we first give constructive proofs, and from these proofs we then compute the extracted terms, which is the desired algorithm. The correctness of the extracted term follows directly by the Soundness Theorem of program extraction. In order to get the extracted term from some proofs which are often quite long, we use the proof assistant Minlog. However, to apply the extracted terms, the programming language Haskell is useful. Therefore after each proof we show a notation of the extracted term, which can be easily rewritten as a definition in Haskell.

cs.LO↗

arXiv2022

Limits of real numbers in the binary signed digit representation

We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digits. The main objective of this paper is the formalisation of a constructive proof that real numbers are closed with respect to limits. All the proofs of the main theorem and the first application are implemented in the Minlog proof system and the extracted terms are further translated into Haskell. We compare two approaches. The first approach is a direct proof. In the second approach we make use of the representation of reals by a Cauchy-sequence of rationals. Utilizing translations between the two represenation and using the completeness of the Cauchy-reals, the proof is very short. In both cases we use Minlog's program extraction mechanism to automatically extract a formally verified program that transforms a converging sequence of reals, i.e.~a sequence of streams of binary signed digits together with a modulus of convergence, into the binary signed digit representation of its limit. The correctness of the extracted terms follows directly from the soundness theorem of program extraction. As a first application we use the extracted algorithms together with Heron's method to construct an algorithm that computes square roots with respect to the binary signed digit representation. In a second application we use the convergence theorem to show that the signed digit representation of real numbers is closed under multiplication.

math.LO↗

arXiv2021

Rates of convergence for asymptotically weakly contractive mappings in normed spaces

We study Krasnoselskii-Mann style iterative algorithms for approximating fixpoints of asymptotically weakly contractive mappings, with a focus on providing generalised convergence proofs along with explicit rates of convergence. More specifically, we define a new notion of being asymptotically $ψ$-weakly contractive with modulus, and present a series of abstract convergence theorems which both generalise and unify known results from the literature. Rates of convergence are formulated in terms of our modulus of contractivity, in conjunction with other moduli and functions which form quantitative analogues of additional assumptions that are required in each case. Our approach makes use of ideas from proof theory, in particular our emphasis on abstraction and on formulating our main results in a quantitative manner. As such, the paper can be seen as a contribution to the proof mining program.

math.FA↗

arXiv2021

Logic for exact real arithmetic

Continuing earlier work of the first author with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.

math.LO↗

arXiv2019

An algorithmic approach to the existence of ideal objects in commutative algebra

The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, which focuses on the elimination of ideal objects via syntactic methods. In this paper, we take an alternative approach based on Kreisel's no counterexample interpretation and sequential algorithms. We first give a computational interpretation to an abstract maximality principle in the countable setting via an intuitive, state based algorithm. We then carry out a concrete case study, in which we give an algorithmic account of the result that in any commutative ring, the intersection of all prime ideals is contained in its nilradical.

cs.LO↗