跳到正文
研踪PaperTrail

论文库

检索计算机领域论文，按研究方向、作者或关键词筛选。

部分采集异常
正在读取账号与研究记录…

全站更新概况

+0新增论文
+0其中 AI 相关
+2已有论文修订
+101新增 AI 导读

arXiv 最近完成扫描：2026-11-15 00:32 · 全站最近入库：2026-11-14 15:09各信源进度 →

统计口径与数据新鲜度

统计 2026-11-14 01:05 — 2026-11-15 01:05（北京时间） · 点击数字查看对应简报；AI 相关包含在新增论文内。

最近完成检查：2026-11-15 00:32最近发现新增版本：2026-11-14 15:09库内论文最新更新时间：2026-11-13 02:59

每分钟刷新已保存的数据。空检查不代表采集异常；新收录可能包含历史论文。AI 导读按新增版本计数。

23,348 已收录论文19,580 AI 相关6,729 有修订112 HF 社区发现

浏览论文库

研究日报 / 周报 →按信源浏览 →

时间范围跟随排序：版本更新、本站收录或首次发表。最新收录可能包含历史论文。部分信源异常，查看状态 →

找到 4 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-15 00:30（北京时间）
版本更新 · v2arXiv:2611.00176

Coinduction in Grounded Arithmetic

Bryan Ford

原文摘要

A grounded arithmetic counts a sentence true only when a terminating process establishes it; a sentence no such process settles has no value. Such a logic can state that an event happens, but not that it never happens under unbounded choice. This paper extends such a logic so that it can. The base is Reflective Grounded Arithmetic (RGA) with Inductive Grounded Arithmetic (IGA)'s least-fixed-point reading and ground induction. It adds a separate greatest-fixed-point former $ν$ with Park's coinduction rule, proves that one former cannot carry both ground induction and coinduction, and adds a dichotomy rule: the classical disjunction between a least-fixed-point atom and the greatest-fixed-point atom of its dual, under a derivable premise that the body's leaves are decided. The systems are sound for an explicit model reading every $ν$-body at its greatest fixed point, hence consistent; they agree with the least model where it has a value and prove sentences it leaves without one. The dichotomy trades the underivable hypothesis that an order is well-founded for the derivable one that its steps are decided, at the price of a change of model. With ground induction the dichotomy derives the omniscience rule of the sibling system OGA, so the system has no semantics whose certificates for universals are its own proofs; without the dichotomy it has one, though unsound for the least model. The systems prove, as single sentences, that every decided tree is well-founded or has an infinite branch given by a term, total in the new model; that random assignment terminates while its divergent twin runs forever; that a fair loop terminates and the alternating-bit protocol delivers every message; that open games are determined; that the termination gap in Nakata and Uustalu's trace semantics closes; and that Cinderella wins the bucket game at capacity three. Isabelle/HOL checks every result.

math.LO · cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2608.16140

Internal Reasoning and Consistency in Reflective Grounded Arithmetic

Bryan Ford

原文摘要

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic allowing direct expression of any general-recursive computation. Every RGA term is a program and truth is grounded evaluation, with a proof certificate at each universal quantifier. This paper shows, in a machine-checked Isabelle/HOL development, that such a system is powerful enough to carry out its own metamathematics. A fuel-indexed decider of RGA's grounded semantics and checkers for RGA's proofs are compiled primitive-recursive RGA terms. RGA proves internally that its decider never affirms 0 = 1, and that every well-formed term it affirms has an RGA proof accepted by a transparent test. RGA proves that, for each valid RGA proof, its conclusion is true. RGA proves that each grounded-true well-formed term is provable. RGA proves that no proof in either of two decided classes of RGA proofs derives 0 = 1. RGA's truth predicate also serves as a medium for proof by reflection, of the kind that adds nothing to the system. RGA derives disquotation for quantifier-free formulas as rules in every context, at a free variable, and proves, as one sentence, that whenever its normalizer for polynomials in one variable gives two terms the same normal form, the equation between them is true at every value of the variable. Each such polynomial identity then follows from that sentence by closed evaluation and disquotation, with no reflection rule. A companion paper proves Gödel's incompleteness theorems for RGA and its extensions.

math.LO · cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.13697

Gödel's Incompleteness Theorems in Grounded Arithmetic

Bryan Ford

原文摘要

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic in which every term is a program and truth is grounded evaluation. RGA discharges a hypothesis only when it proves the hypothesis decided. This paper shows, in a machine-checked Isabelle/HOL development, how Gödel's incompleteness theorems hold for RGA and for systems built on it. RGA's implication is material and RGA has the disjunction property, so the implications the textbook proof of the second theorem uses fail while its entailments and rules hold: Gödel's proof survives as entailments. RGA does not prove its consistency sentence Con, and RGA derives its own second theorem as the entailment $\mathit{Con}\vdash\neg\mathit{Pr}(\ulcorner\mathit{Con}\urcorner)$ and as one sentence quantified over proofs. The second theorem is then proved once, for every Gödel extension of RGA: an entailment relation on RGA's language, closed under RGA's rules, with a checker that meets three structural conditions, NEC, D3 and EXPL as proof transformers, D1 as closed acceptance, and consistency. D2 is not among the conditions. RGA with its checker is one instance. Inductive Grounded Arithmetic (IGA), RGA with ground induction, is another, its checker adding one rule detector, and IGA does not derive its consistency sentence for it. Adoption, a reflection rule whose premise is a derived warrant that the checker accepts computed proofs of every instance of a universal, gives consistent extensions RGA$^+$ and IGA$^+$. RGA$^+$ derives RGA's consistency sentence and IGA$^+$ derives RGA's and IGA's, so each strictly extends its base, and IGA$^+$ both. The second theorem holds at every adopted notation claim, and adopting Turing's code for that claim's checker derives its consistency sentence, so no claim certifies itself. Whether IGA alone derives RGA's consistency sentence is open, and the paper names what two routes to an answer need.

math.LO · cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2610.34548

Inductive Grounded Arithmetic: Goodstein, the Hydra, and $Γ_0$

Bryan Ford

原文摘要

What does a recursive definition mean when the logic is grounded, so a sentence is true only if a terminating process makes it so? Kripke's answer for the special case of truth was the least fixed point. This paper takes that answer as a rule. Reflective Grounded Arithmetic (RGA) already writes any recursive definition as one self-referential term, paradoxes included. Inductive Grounded Arithmetic (IGA) adds the elimination rule for every positive one, so that accessibility, the winning positions of a game, and grounded truth itself each come with their own induction principle. The rule is sound for the omega model and the system is consistent, both machine-checked in Isabelle/HOL. With the rule, IGA proves Goodstein's theorem outright, in a logic without implication at an undecided hypothesis, and the Kirby-Paris hydra game for primitive recursive strategies, both with every step of the arithmetic a grounded derivation. It proves the Cantor normal forms well-founded, from which the well-foundedness of the standard $\varepsilon_0$ notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every $\varphi(n,0)$. It defines Kripke truth for RGA's own language as one fixed point that agrees with the omega model exactly. Two equivalences locate what the classical world has and the grounded one does not. IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order, and bivalence of accessibility for an order is sound exactly when the order is well-founded; so $Γ_0$ lies at most one instance of excluded middle away, at the accessibility predicate of the notation, and that instance, the well-foundedness sentence and one membership claim in a primitive-recursive form of Kleene's $\mathcal O$ are interderivable over IGA.

math.LO · cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗