Toshiyasu Arai
In this note let us give two remarks on proof-theory of PA. First a derivability relation is introduced to bound witnesses for provable $Σ_{1}$-formulas in PA. Second Paris-Harrington's proof for their independence result is reformulated to show a `consistency' proof of PA based on a combinatorial principle.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We give an arithmetical proof of the strong normalization of the $λ$-calculus (and also of the $λμ$-calculus) where the type system is the one of simple types with recursive equations on types. The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was not known. Our proof shows that it is not more than Peano arithmetic.
Fragments of arithmetic and cyclic proofs
本文提出一种更简单且适合证明分析与自动化归纳证明搜索的皮亚诺算术循环证明系统，并展示传统归纳受限子系统可表示为其片段。
Cyclic proofs in the equational version of Primitive recursive arithmetic
针对原始递归算术的等式版本提出循环证明系统，并利用结构证明论工具证明其等价性，无需自动机方法。
Cyclic proofs for arithmetical inductive definitions
该研究针对算术归纳定义的循环证明理论，通过元数学论证结合二阶算术中递归序数理论的形式化，证明了循环系统与归纳系统能力等价，解决了闭包序数超出元理论证明论序数的难题。
Based on the MRDP theorem, we introduce the ideas of the proof equation of a formula and universal proof equation of Peano Arithmetic (PA); and then, combining universal proof equation and Gödel's Second Incompleteness Theorem, it is proved that, if PA is consistent, then for every axiom and every theorem of PA, we can construct a corresponding undecidable proposition with Diophantine form. Finally, we present an approach that transforms seeking a proof of a mathematical (set theoretical, number theoretical, algebraic, geometrical, topological, etc) proposition into solving a Diophantine equat…
Peano Arithmetic, games and descent recursion
本文通过初等下降递归视角分析Coquand对皮亚诺算术的博弈论解释，提供其切消证明的直接实现，用下降递归函数描述获胜策略，还得到可证递归函数和泛函已知结果的新证明。
Iterating reflection over intuitionistic arithmetic
本文研究了直觉算术上反射的迭代，提出了统一反射的新证明方法，并扩展了Feferman完备性定理的应用。
Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various methods of extracting computational information from proofs in classical first-order arithmetic, and reflects on some of the relationships between them. Variants of the Gödel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory.
Definable sets in Skolem arithmetic
本文研究Skolem算术中的可定义集问题，提出全新的可定义集刻画方法，采用不同组合工具证明该理论的可判定性，旨在给出比现有证明更简洁的可判定性证明。
In 1994 Jech gave a model theoretic proof of Gödel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano Arithmetic with the role of models being taken by complete consistent extensions. In this note we take another step in the direction of replacing proof-theoretic by model-theoretic arguments. We show, without passing through the arithmetized completeness theorem, that the existence of a model of PA of complexity $Σ^0_2$ is independent of PA, where a model is ide…
Induction is typically formalized as a rule or axiom extension of the LK-calculus. While this extension of the sequent calculus is simple and elegant, proof transformation and analysis can be quite difficult. Theories with an induction rule, for example Peano arithmetic do not have a {\em Herbrand} theorem. In this work we extend an existing meta-theoretic formalism, so called proof schemata, a recursive formulation of induction particularly suited for proof analysis, to Peano arithmetic. This relationship provides a meaningful conservative reflection principle between \PA and an alternative p…
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the provability of the classical cyclic proof system and that of the classical system of Martin-Lof's inductive definitions. This paper studies the conjecture for intuitionistic logic. This paper first points out that the countermodel of FOSSACS 2017 paper by the same authors shows the conjecture for intuitionistic logic is false in general. Then this paper shows the conjecture for intuitionistic logic is true under ari…
We study reflection principles of Peano Arithmetic PA which are based on both proof and provability. Any such reflection principle in PA is equivalent to either $\Box P\!\rightarrow\! P$ ($\Box P$ stands for `$P$ is provable') or $\Box^k u\!\!:\!\!P\!\rightarrow\! P$ for some $k\geq 0$ ($t:P$ states `$t$ is a proof of $P$'). Reflection principles constitute a non-collapsing hierarchy with respect to their deductive strength $$u\!\!:\!\!P\!\rightarrow\! P\ \ \prec\ \ \Box u\!\!:\!\!P\!\rightarrow\! P\ \ \prec\ \ \Box^2 u\!\!:\!\!P\!\rightarrow\! P \ \ \prec\ \ldots\ \prec\ \ \Box P\!\rightarrow…
In this paper we introduce a system AID (Alogtime Inductive Definitions) of bounded arithmetic. The main feature of AID is to allow a form of inductive definitions, which was extracted from Buss' propositional consistency proof of Frege systems F. We show that AID proves the soundness of F, and conversely any Σ^b_0-theorem in AID yields boolean sentences of which F has polysize proofs. Further we define Σ^b_1-faithful interpretations between AID + Σb^_0 - CA and a quantified theory QALV of an equational system ALV in P. Clote. Hence ALV also proves the soundness of F.
Logic for exact real arithmetic
本文从正式证明中提取实数（以带符号数字流表示）的除法算法，利用余归纳谓词和Minlog证明助手，并在Haskell中运行验证。
A folk theorem says higher order arithmetic has the proof theoretic strength of set theory with limited power set. This paper makes the theorem precise in terms of several axiom system based on ZF.
Unravelling Cyclic First-Order Arithmetic
本文提出将 Heyting 与 Peano 算术循环证明直接嵌入纯归纳证明的方法，扩展 Springer–Dam 翻译以恢复 Das 的 CΠ_n⊆IΠ_{n+1}，并给出标号矢列演算表示。
We give proofs of Gödel's incompleteness theorems after A. Joyal. The proof uses internal category theory in an arithmetic universe, a predicative generalisation of topoi. Applications to Löb's Theorem are discussed.
In 2010, Vladimir Voevodsky gave a lecture on "What If Current Foundations of Mathematics Are Inconsistent?" Among other things he said that he was seriously suspicious that an inconsistency in PA (first-order Peano arithmetic) might someday be found. About a year later, Edward Nelson announced that he had discovered an inconsistency not just in PA, but in a small fragment of primitive recursive arithmetic. Soon, Daniel Tausk and Terence Tao independently found a fatal error, and Nelson withdrew his claim, stating that consistency of PA was an "open problem." Many mathematicians may find such …
Unlike some other formal systems, the proof system Metamath has no built-in concept of "decimal number" in the sense that arbitrary digit strings are not recognized by the system without prior definition. We present a system of theorems and definitions and an algorithm to apply these as basic operations to perform arithmetic calculations with a number of steps proportional to an arbitrary-precision arithmetic calculation. We consider as case study the formal proof of Bertrand's postulate, which required the calculation of many small primes. Using a Mathematica implementation, we were able to c…
Hindman's Theorem is a prototypical example of a combinatorial theorem with a proof that uses the topology of the ultrafilters. We show how the methods of this proof, including topological arguments about ultrafilters, can be translated into second order arithmetic.
Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
本文在可计算泛函理论TCF框架下，从构造性、算法和证明论视角重新审视初等数论标准定理，通过Minlog证明助手形式化定义和定理，并利用程序提取生成可执行的Haskell代码，重点研究提取程序的效率及其对定理表述的影响。
This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, $\widehat{\mathrm{ID}}{}_{1}^{\mathrm{i}}$, over Heyting arithmetic (HA), originally proved in full generality by Arai (2011). The proof embeds $\widehat{\mathrm{ID}}{}_{1}^{\mathrm{i}}$ into the corresponding theory over Beeson's logic of partial terms and then uses two consecutive interpretations, a realizability interpretation of this theory into the subtheory generated by almost negative fixpoints, and a direct interpretation into Heyting arithmetic with partial terms using …
Clausal Language (CL) is a declarative programming and verifying system used in our teaching of computer science. CL is an implementation of, what we call, $\mathit{PR}{+}IΣ_1$ paradigm (primitive recursive functions with $IΣ_1$-arithmetic). This paper introduces an extension of $IΣ_1$-proofs called extraction proofs where one can extract from the proofs of $Π_2$-specifications primitive recursive programs as efficient as the hand-coded ones. This is achieved by having the programming constructs correspond exactly to the proof rules with the computational content.
Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories. Turing progressions based on $n$-provability give rise to a $Π_{n+1}$ proof-theoretic ordinal. As such, to each theory $U$ we can assign the sequence of corresponding $Π_{n+1}$ ordinals $\langle |U|_n\rangle_{n>0}$. We call this sequence a \emph{Turing-Taylor expansion} of a theory. In this paper, we relate Turing-Taylor expansions of sub-theories of Peano Arithmetic to Ignatiev's universal model for the closed fragment of the polymodal provability logic ${\mathbf{GLP}}_ω$. In particular,…
Andrew Wiles' Proof of Fermat's Last Theorem, As Expected, Does Not Require a Large Cardinal Axiom. A Discussion of Colin McLarty's "The Large Structures of Grothendieck Founded on Finite-Order Arithmetic"
本文探讨了 Fermat 大定理的证明是否依赖大基数公理，指出 Colin McLarty 证明了 Grothendieck 的大工具可建立在有限阶算术强度的 ZFC 片段上，从而消除了该证明依赖强于 ZFC 基础的表象。
This short paper addresses the open problems left in a previous paper by Franco Montagna and Carles Noguera. Besides giving solutions to these two problems, some clarification concerning the role of the full vocabulary (including functional symbols) in the proofs there given is also discussed.
We generalize Cooper's method of quantifier elimination for classical Presburger arithmetic to give a new proof that all parametric Presburger families (as defined by Kevin Woods) are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial f over the integers. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic with multiplication by scalars from any ring of functions into Z.
This paper presents proof that Buss's $S^2_2$ can prove the consistency of a fragment of Cook and Urquhart's $\mathrm{PV}$ from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic $S^1_2$. Our proof relies on the notion of "computation" of the terms of $\mathrm{PV}$. In our work, we first prove that, in the system under consideration, if an equation is proved and either its left- or right-hand side is computed, then there is a corresponding computati…
Akama et al. systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem, then modify it in an appropriate way. In addition, we characterize several prenex normal form theorems with respect to semi-classical arithmetic.
In 2002 Robert Solovay proved that a subsystem BI of classical second order arithmetic, with bar induction and arithmetical countable choice, can be negatively interpreted in the neutral subsystem BSK of Kleene's intuitionistic analysis FIM using Markov's Principle MP. Combining this result with Kleene's formalized recursive realizability, he established (in primitive recursive arithmetic PRA) that FIM + MP and BI have the same consistency strength. This historical note includes Solovay's original proof, with his permission, and the additional observation that Markov's Principle can be weakene…
Conservativity of Type Theory over Higher-order Arithmetic
本文证明具有一个宇宙层次的类型理论对高阶海廷算术保守，并揭示逻辑解释（证明无关与证明相关）对保守性程度的影响，最终证明De Jongh定理。
Stabilizers and NIP arithmetic regularity
该研究为有限群NIP算术正则引理提供了无需复杂模型论工具的初等新证明，拓展了相关稳定子引理，还证明了NIP集合满足强形式多项式Bogolyubov-Ruzsa猜想。
We study the proof scheme "proof by example" in which a general statement can be proved by verifying it for a single example. This strategy can indeed work if the statement in question is an algebraic identity and the example is "generic". This article addresses the problem of constructing a practical example, which is sufficiently generic, for which the statement can be verified efficiently, and which even allows for a numerical margin of error. Our method is based on diophantine geometry, in particular an arithmetic Bézout theorem, an arithmetic Nullstellensatz, and a new effective Liouville…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。