The provably total recursive functions and the MRDP theorem in Basic Arithmetic and its extensions

Division by zero

For any sufficiently strong theory of arithmetic, the set of Diophantine equations provably unsolvable in the theory is algorithmically undecidable, as a consequence of the MRDP theorem. In contrast, we show decidability of Diophantine equations provably unsolvable in Robinson's arithmetic Q. The argument hinges on an analysis of a particular class of equations, hitherto unexplored in Diophantine literature. We also axiomatize the universal fragment of Q in the process.

KPl的可证全集合递归函数

The Provably Total Set-Recursive Functions of KPl

通过相对化序数分析，刻画了KPl及其相关理论的可证全集合递归从ω函数。

Formalizing computability theory via partial recursive functions

We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply Gödel numberings where needed and e…

Aurellion函数：超越Knuth记号的一种递归快速增长层级

The Aurellion Function: A Recursive Fast-Growing Hierarchy Beyond Knuth Notation

本文提出Aurellion函数，一种基于Knuth上箭头记号的递归快速增长层级，证明其支配Peano算术中所有可证明全函数，并将其定位于证明论序数Γ₀附近，同时探讨超限扩展以连接大数构造与序数分析。

Classifying the provably total set functions of KP and KP(P)

This article is concerned with classifying the provably total set-functions of Kripke-Platek set theory, KP, and Power Kripke-Platek set theory, KP(P), as well as proving several (partial) conservativity results. The main technical tool used in this paper is a relativisation technique where ordinal analysis is carried out relative to an arbitrary but fixed set x. A classic result from ordinal analysis is the characterisation of the provably recursive functions of Peano Arithmetic, PA, by means of the fast growing hierarchy [10]. Whilst it is possible to formulate the natural numbers within KP,…

数理逻辑导论

An Introduction to Mathematical Logic

本文是面向数学本科生的数理逻辑导论，涵盖命题与一阶逻辑、Gödel不完备性定理、证明论、可计算性、模型论及集合论基础，课程含28次讲座与14次习题课。