跳到正文
研踪PaperTrail

论文库

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

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

全站更新概况

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

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

统计口径与数据新鲜度

统计 2026-11-14 02:13 — 2026-11-15 02:13(北京时间) · 点击数字查看对应简报;AI 相关包含在新增论文内。

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

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

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

浏览论文库

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

找到 53 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-15 01:32(北京时间)
版本更新 · v3arXiv:2509.04192

Domain size asymptotics for Markov logic networks

Vera Koponen

原文摘要

A Markov logic network (MLN) $\mathbb{M}$ determines a probability distribution $\mathbb{P}_n^\mathbb{M}$ on the set $\mathbf{W}_n$ of structures, or ``possible worlds'', with domain $\{1, \ldots, n\}$. We study the properties of such distributions as $n$ tends to infinity. We show that with mild assumptions on an MLN $\mathbb{M}$ with one soft constraint with an arbitrary positive weight the distribution $\mathbb{P}_n^\mathbb{M}$ will behave quite differently from the uniform distribution $\mathbb{P}_n^{uni}$ on $\mathbf{W}_n$ for all sufficiently large $n$. For a language with only one relation symbol $R$ which has arity 1 we give an almost complete characterization of the possible asymptotic behaviours of $\mathbb{P}_n^\mathbb{M}$ as $n \to \infty$, where $\mathbb{M}$ may be any MLN for this language. The asymptotic behaviour depends on the soft constraints and weights of the MLN. This characterization is used to show that if the language under consideration contains at least one relation symbol of arity 1 then the following holds: (a) There is an MLN $\mathbb{M}$ such that for every lifted Bayesian network (LBN) $\mathbb{G}$ there are infinitely many $n$ such that $\mathbb{M}$ and $\mathbb{G}$ determine different distributions on $\mathbf{W}_n$. (b) There is an LBN $\mathbb{G}$ such that for every MLN $\mathbb{M}$ there are infinitely many $n$ such that $\mathbb{G}$ and $\mathbb{M}$ determine different distributions on $\mathbf{W}_n$. We also show that, in the limit, the weight dimension and the domain size dimension may behave completely differently.

cs.AI · cs.LO · math.LO

版本更新 · v3arXiv:2604.10669

A Linear Temporal Logic of Frequencies on Series of Events

Melissa Antonelli, Alessandro Giuseppe Buda, Leonardo Ceragioli, Ferdinando Fugazza Calda, Giuseppe Primiero

原文摘要

This paper introduces LTLFS, a linear temporal logic for reasoning about frequencies in finite series of probabilistic events. The logic conservatively extends linear temporal logic over finite traces with measure-sensitive operators that compare the empirical distribution observed at any point in a series with an independently specified target distribution. Its semantics integrates the actual sequence of events, the probability distribution governing individual outcomes, and the set of finite assignments compatible with the target frequency. This supports two complementary tasks: verifying whether an observed partial distribution is compatible with the benchmark, and predicting whether and with what probability the completed series can still satisfy it. The language can express observed and attainable frequencies, the probability of realizing a desired final distribution, and conditional probabilities for subsequent outcomes under the assumption that the benchmark is met. We establish formal properties of the operators and characterize their interaction with the temporal structure. A running example concerning representational fairness in sequential outputs from a generative AI system illustrates how the framework can distinguish temporary deviations from irrecoverable violations and support early, logically interpretable intervention. LTLFS thereby provides a symbolic foundation for runtime monitoring of evolving quantitative requirements, with applications to explainable and responsible AI.

cs.LO · math.LO

版本更新 · v5arXiv:2609.36279

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Christoph Benzmüller

原文摘要

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument, reaches beyond the modal object language: its quantifiers range over domains containing the nominals and satisfaction operators of hybrid logic. A proof using one proves a theorem of the embedding, not necessarily of the modal logic. Whether a result is one of the modal logic can be settled by replaying it in an explicit calculus, or, more cheaply and for all results at once, by analysing what the embedding's proofs substitute. Every statement the Notes prove has a proof in the embedding substituting nothing outside the object language, 294 of them explicit. The Notes' own proofs substitute none either; what it flags are terms a prover introduced. A soundness theorem over general models closed under the object language, and a sentence of that language the embedding proves but which fails in such a model, fix what the certificate says. The Notes' three open questions are settled too, without nominals, but by the empty instance of the conjunction axiom, too cheaply to convince. Generalised to Gödel's "any number of summands", the axiom covers the empty conjunction and the singleton. This article restricts it to at least two different conjuncts, a non-degenerate reading of Gödel's footnote, and settles them again without nominals. In effect only the empty conjunction is excluded; the singleton comes back with the other axioms. In one variant the restriction refutes the possible existence of a God-like being; the answers return, with no side condition, once the Notes' non-emptiness clause is confined to Gödel's essence. Every theorem here is verified in Isabelle/HOL and independently in Lean 4, the separating model in its propositional part; the countermodels are Nitpick's, checked by the build.

cs.LO · cs.AI · math.LO

版本更新 · v5arXiv:2501.03789

Structures preserved by primitive actions of $S_ω$

Manuel Bodirsky, Bertalan Bodor

原文摘要

We present a dichotomy for structures $A$ that are preserved by primitive actions of $S_ω = \text{Sym}({\mathbb N})$: such a structure primitively positively constructs all finite structures and the constraint satisfaction problem is NP-complete, or the constraint satisfaction problem for $A$ is in P. To prove our result, we study the first-order reducts of the Johnson graph $J(k)$, for $k \geq 2$, whose automorphism group $G$ equals the action of $\text{Sym}({\mathbb N})$ on the set $V$ of $k$-element subsets of $\mathbb N$. We use the fact that $J(k)$ has a finitely bounded homogeneous Ramsey expansion and that $G$ is a maximal closed subgroup of $\text{Sym}(V)$.

math.LO · cs.CC

新论文 · v1arXiv:2611.01501

Order-Invariant CFO Contains Local-Order-Invariant FO

Derek R. Aoki

原文摘要

Order-invariant cluster first-order logic (CFO) and local-order-invariant first-order logic are two fragments of order-invariant first-order logic, both motivated by the study of invariant logics on classes of bounded degree. Our main result is that order-invariant CFO contains local-order-invariant FO on arbitrary classes of finite structures, settling the conjecture of Ghasemi and Grange that order-invariant CFO contains plain FO. By combining this with a collapse result of Ghasemi and Grange, we obtain the equivalence of FO, local-order-invariant FO, and order-invariant CFO on classes of finite colored graphs of bounded degree. The proof makes use of Gaifman normal form, which allows our translation from local-order-invariant FO to order-invariant CFO to be effective. Combined with the fixed-parameter tractability of model-checking for order-invariant CFO on bounded-degree colored graph classes, this shows that model-checking for local-order-invariant FO on bounded-degree colored graph classes is fixed-parameter tractable. To generalize our collapse and model-checking results beyond colored graphs, we use a method based on first-order interpretations which also yields a collapse of order-invariant FO to FO when restricted to graph classes of bounded shrub-depth. Finally, we give an application to the database-motivated frozen-witness logic of Abiteboul, Simon, and Vianu by showing that local-order-invariant FO contains deterministic frozen-witness FO, and thus that deterministic frozen-witness FO collapses to FO on classes of finite structures of bounded degree.

math.LO · cs.LO

版本更新 · v4arXiv:2510.24993

Morita Rigidity for Kleene Algebras

Luke Serafin

原文摘要

We introduce Morita equivalence to the study of Kleene algebras and modules. Classical characterizations of Morita-equivalent semirings such as having equivalent categories of modules and one semiring being a full idempotent corner of a finite matrix semiring over the other transfer easily to this new context. We also observe that Morita equivalence can be applied to extending and restricting scalars in Lindenbaum--Tarski algebras of propositional dynamic logics, and that an appropriately-defined category of generalized finite automata satisfies the property that when the underlying Kleene algebras are Morita equivalent then the corresponding categories of generalized automata are equivalent. But the signature results which we obtain relate to rigidity of Kleene algebras in this context. Specifically, every semiring that is Morita-equivalent to the semiring reduct of a Kleene algebra has a unique expansion to a Kleene algebra, and semiring bimodules witnessing Morita-equivalence of semirings which are reducts of Kleene algebras are already Kleene bimodules.

cs.LO · math.LO

版本更新 · v2arXiv:2604.22020

Interpolation above S4

Simon Santschi, Niels C. Vooijs

原文摘要

We complete Maksimova's classification of Craig and deductive interpolation in normal extensions of S4. In particular, we prove Craig interpolation for the six extensions of S4 for which the status of the property was still open. The proof strategy builds upon the ideas of Smoryński, but employs a novel approach using Fine's frame formulas for splitting clusters in transitive models.

math.LO · cs.LO

版本更新 · v3arXiv:2502.18259

Generalization of terms via universal algebra

Tommaso Flaminio, Sara Ugolini

原文摘要

We provide a new foundational approach to the generalization of terms up to equational theories. We interpret generalization problems in a universal-algebraic setting making a key use of projective and exact algebras in the variety associated to the considered equational theory. We prove that the generality poset of a problem and its type (i.e., the cardinality of a complete set of least general solutions) can be studied in this algebraic setting. Moreover, we identify a class of varieties where the study of the generality poset can be fully reduced to the study of the congruence lattice of the 1-generated free algebra. We apply our results to varieties of algebras and to (algebraizable) logics. In particular we obtain several examples of unitary type: abelian groups; commutative monoids and commutative semigroups; all varieties whose 1-generated free algebra is trivial, e.g., lattices, semilattices, varieties without constants whose operations are idempotent; Boolean algebras, Kleene algebras, and Gödel algebras, which are the equivalent algebraic semantics of, respectively, classical, 3-valued Kleene, and Gödel-Dummett logic. Finally, we prove that the variety of MV-algebras, the equivalent algebraic semantics of Lukasiewicz logic, has nullary type.

math.LO · cs.LO

版本更新 · v2arXiv:1912.00012

Negative Translations for Affine and Lukasiewicz Logic

Rob Arthan, Paulo Oliva

原文摘要

We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in \emph{affine logic} the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and {\it vice versa}. By contrast, in the setting of \emph{Łukasiewicz logic}, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, Gödel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Łukasiewicz logic but are all equivalent.

cs.LO · math.LO

新论文 · v1arXiv:2610.39774

Step Recursion: Exact Membership Spectra, Mixed Strides, and Collapse

Kirill Osipov

原文摘要

For a strictly increasing $G:\mathbb{N}\to\mathbb{N}$ with $G(0)\geq 1$, we study minimal-basis function algebras generated by recursion along generalized inverses of its iterates. Bounded recursion requires an earlier pointwise majorant; unbounded recursion has no such requirement. If the orbit $G^{[t]}(0)$ has no polynomial upper bound, we obtain exact fixed-function membership spectra, reverse-divisibility inclusion, and indexed intersections that need not be single-stride algebras. Every finite divisibility-downset is realized in both regimes, and mixed strides admit fixed functions expressing any finite monotone Boolean condition on their additive stride monoid. For every generator, the realized bounded spectra form a bounded meet-semilattice: a construction sharing a bounding input coordinate realizes finite intersections without an unrestricted selector. Polynomial orbit growth is equivalent to definability of each of ordinary predecessor, unary doubling, and addition in any fixed unbounded stride algebra. In this case the algebra is ordinary primitive recursion relative to its inverse map, giving full collapse for primitive-recursive $G$. Ordinary predecessor belongs to a bounded stride algebra exactly when the orbit is polynomially bounded and $G$ has bounded successive differences; equivalently, ordinary bounded recursion embeds. A locality obstruction explains the additional bounded requirement, and two primitive-recursive generators with quadratic orbits have opposite bounded collapse behavior.

cs.LO · math.LO

新论文 · v1arXiv:2610.39760

EPPA for Reducts of the Random Graph

Sofia Brenner, Jan Hubička, Matěj Konečný

原文摘要

We prove that finite two-graphs have coherent EPPA and that neither graphs modulo global complementation nor two-graphs modulo global complementation have EPPA. This completes the classification of EPPA and coherent EPPA for the reducts of the random graph, answering a question and confirming a conjecture of Evans, Hubička, Konečný and Nešetřil.

math.CO · cs.DM · math.LO

新论文 · v1arXiv:2610.39746

Step Recursion: Rational Strides and Exact Inclusion Orders over the Reals

Kirill Osipov

原文摘要

We study finite-terminating, address-only step recursion on the nonnegative reals, from zero, unit successor and projections. For reduced positive rational strides $s=a/q$ and $t=b/v$, we prove $\mathcal{C}s\subseteq\mathcal{C}t$ if and only if $q$ divides $v$, for both the bounded and unbounded algebras $\mathcal{C}\in{\mathcal{B},\mathcal{U}}$. The bounded compiler preserves earlier global majorants on every auxiliary input. Mixed rational stride sets are classified by least common denominators and supernatural denominators. Primitive-recursive translated-coordinate grid codes characterize the unbounded algebras and yield $\mathcal{U}{1/q}\cap\mathcal{U}{1/v}=\mathcal{U}{1/\gcd(q,v)}$. For bounded intersections, we prove an exact reduction: all corresponding identities hold if and only if the single identity $\mathcal{B}{1/2}\cap\mathcal{B}_{1/3}=\mathcal{B}_1$ holds, equivalently if the Boolean parts of the integer successor and addition algebras under scalar bounded recursion coincide. A Boolean reconstruction reduces general functions to predicates; a clipped fine-grid simulation with a frozen global resource bound identifies the union of predicate precision classes with the addition level. These reductions do not decide the resulting predicate equality, so literal bounded intersections remain unresolved. We also prove that unbounded-program equality is $Π^0_1$-complete and extensional bounded-algebra membership is $Σ^0_2$-complete. The model has no free real arithmetic or Zeno limits; semantic majorant validity is distinguished from syntax transformation.

cs.LO · math.LO

版本更新 · v2arXiv:2201.07007

Aspects of Muchnik's paradox in restricted betting

George Barmpalias, Lu Liu

原文摘要

Muchnik's paradox says that enumerable betting strategies are not always reducible to enumerable strategies whose bets are restricted to either even rounds or odd rounds. In other words, there are outcome sequences x where an effectively enumerable strategy succeeds, but no such parity-restricted effectively enumerable strategy does. We characterize the effective Hausdorff dimension of such $x$, showing that it can be as low as 1/2 but not less. We also show that such reals that are random with respect to parity-restricted effectively enumerable strategies with packing dimension as low as $\log\sqrt3$. Finally we exhibit Muchnik's paradox in the case of computable integer-valued strategies.

math.LO · cs.GT

新论文 · v1arXiv:2610.39108

Deciding two-variable logic with global and local Presburger quantification

Michael Benedikt, Chia-Hsuan Lu, Alex Perry, Tony Tan

原文摘要

We look at a two-variable logic over finite graphs that allows Presburger quantifiers: linear arithmetic inequalities between the number of elements that satisfy subformulas. The prior literature shows that closing two-variable logic under Presburger quantification leads to undecidability, while closing under \emph{local quantification} -- the counts are always over neighbors of a given node -- preserves decidability. Here we show decidability of satisfiability for an intermediate logic that allows both local counts and global counts, but where the linear constraints do not mix the two. The proof requires a significant extension of the prior machinery developed for two-variable logic with counting. As a corollary we obtain decidability of satisfiability for an important family of Graph Neural Networks (GNNs). GNNs are a popular graph learning formalism. For example, in a variation of GNNs considered in the past literature, local aggregation is used in each layer to create modified values at each vertex of a graph, and then global aggregation is used in a final layer to obtain a single numerical value for the graph as a whole. Our logic is motivated by the fact that mixing of local counting and global aggregation in GNNs has been shown to lead to undecidability. Our results here show that if global and local aggregation are separated, one regains decidability. Decidability of other static analysis problems, like equivalence of GNNs, follows from the decidability of satisfiability.

cs.LO · math.LO

新论文 · v1arXiv:2610.38871

Connecting Base-Extension Semantics, Beth Semantics, and Ecumenical Logic

Victor Barroso-Nascimento, Joaquim T. Waddington, Elaine Pimentel

原文摘要

We investigate the relationship between base-extension semantics, Beth semantics, and Prawitz's ecumenical logic. We first present a base-extension semantics for the propositional fragment of Prawitz's system and prove that it is sound and complete. The semantics interprets intuitionistic and classical operators directly within a common proof-theoretic framework, without reducing the classical operators to their intuitionistic counterparts by means of a translation. We then analyse the effect of incorporating Beth-style clauses into base-extension semantics. When arbitrary bases are admitted and $\bot$ is governed by atomic explosion, these clauses trivialise. By contrast, when $\bot$ is treated as a basic sentence and attention is restricted to consistent bases, the Beth-style clauses for atoms and disjunction characterise, respectively, classical atoms and classical disjunction in Prawitz's system. We also obtain equivalent, path-independent formulations of the classical clauses for atoms, disjunction, and implication. These results reveal that the consistency constraint is not merely a technical restriction: within base-extension semantics, it transforms clauses originally associated with intuitionistic semantics into semantic characterisations of classical operators.

cs.LO · math.LO

新论文 · v1arXiv:2610.37108

Finite $\mathbf{BM}$-algebras and fixed-point combinators

Takuma Imamura

原文摘要

We study algebras for the $\mathbf{BM}$-, $\mathbf{BI}$-, and $\mathbf{BMI}$-fragments of combinatory logic, where $\mathbf{B} xyz \to_{w} x\left(yz\right)$, $\mathbf{M} x \to_{w} xx$ and $\mathbf{I} x \to_{w} x$. We prove that every finite $\mathbf{BM}$-algebra $\mathcal{A}$ contains an element $Y$ satisfying $Yx = x\left(Yx\right)$ for all $x\in A$. Moreover, a single closed $\mathbf{BM}$-term represents such an element in every finite $\mathbf{BM}$-algebra. On the other hand, we show that there exists an infinite $\mathbf{BMI}$-algebra with no such element. Consequently, the variety of $\mathbf{BM}$-algebras is not generated by finite $\mathbf{BM}$-algebras. We also characterise finite $\mathbf{BI}$-algebras as finite semigroups with two distinguished left units $B$ and $I$, and finite $\mathbf{BMI}$-algebras as finite idempotent semigroups with three distinguished left units $B$, $M$ and $I$.

math.LO · cs.LO

新论文 · v1arXiv:2610.36552

A Fibrational Framework For Multi-Conclusion Logics

Oualid Merzouga

原文摘要

The fibrational framework of Licata, Shulman, and Riley gives a uniform account of substructural and modal logics for single-conclusion judgments. This thesis extends it to a multiple-output setting in which cartesian resources may be used freely, while linear resources occur exactly once on either side of the turnstile. Judgments are indexed by descriptors: directed acyclic graphs generalizing the tree-shaped expressions of the original framework. Descriptor $2$-cells encode structural transformations, and explicit gates provide weakening, contraction, coweakening, and cocontraction at linear modes. We define a sequent calculus generated by two connectives, $F$ and $U$. We prove identity, invertibility, and cut admissibility. The mode and type theories present linear-non-linear $2$-polycategories, and the projection is a local discrete fibration and a fibration, with opcartesian lifts for one-output base morphisms. Two adequacy results validate the framework: its cartesian fragment recovers the Licata--Shulman--Riley calculus, and its purely linear fragment presents classical multiplicative linear logic. Finally, we relate indexed and fibrational semantics. After developing representability correspondences for multicategories and polycategories, we establish an equivalence between multi-indexed categories over a fixed representable base and multicategorical opfibrations over it, together with its biclosed bifibrational version. We also give a one-way construction from planar poly-indexed data to a planar polycategory.

cs.LO · math.LO

版本更新 · v3arXiv:2603.24923

Normal forms in cubical type theory

Xu Huang

原文摘要

This note documents the specification of normal forms in cubical type theory. The definition is already present in the proof of normalization for cubical type theory, but we present it in a more traditional style explicitly for reference.

cs.LO · math.LO

版本更新 · v4arXiv:2608.07578

Demodalising Gödel's God? Ultrafilters, Rigidity and Modal Collapse Revisited

Christoph Benzmüller

原文摘要

Gödel's ontological argument is modal by design. Possibility and necessity are among its central concerns, and connected interpretation decisions -- extensions or intensions for the positive properties, constant or varying quantifier domains, the choice of modal logic, etc. -- subtly shape the argument and, in particular, whether the modal collapse is implied or not. It is tempting to abstract the modality away and to read the positive properties as merely forming an ultrafilter -- which, however, may replace Gödel's argument with a perhaps more manageable alternative that may have little to do with Gödel's original intention. In this spirit, Odifreddi and Gomes argue that modal collapse is an intrinsic structural feature of any theory that characterises positive properties as an ultrafilter and identifies God as its principal generator. This comment shows that the structural claim is false. There is an explicit S5 model, with constant domains, in which positivity is at every world a modal ultrafilter principally generated by a unique and necessarily existing Godlike individual, and in which the modal collapse nevertheless fails -- already for an atomic formula. What drives the collapse is not the ultrafilter structure but the rigidity of positivity -- itself a thoroughly modal condition: given only that positivity is a modal ultrafilter, modal collapse and rigidity are equivalent. Rigidity is thus exactly what the collapse adds to the ultrafilter structure, and the disagreement is whether it is to be counted part of that structure at all. Two further claims of Odifreddi and Gomes are clarified: one on the derivability of Gödel's Theorem IV, one on the extensionality of positivity. All results are machine-checked in Isabelle/HOL, which distinguishes kernel-checked proofs from model-finder output.

math.LO · cs.LO

新论文 · v1arXiv:2610.35770

The Undecidability of FO3 and the Calculus of Relations with Just One Binary Relation

Yoshiki Nakamura

原文摘要

The validity problem for first-order logic is a well-known undecidable problem. The undecidability also holds even for $\mathsf{FO}3$ and (equational formulas of) the calculus of relations. In this paper we tighten these undecidability results to the following: (1) $\mathsf{FO}3$ with just one binary relation is undecidable even without equality; and (2) the calculus of relations with just one character and with only composition, union, and complement is undecidable. Additionally we prove that the finite validity problem is also undecidable for the above two classes.

cs.LO · math.LO

版本更新 · v4arXiv:2507.15117

A meta-modal logic for bisimulations

Alfredo Burrieza, Fernando Soler-Toscano, Antonio Yuste-Ginel

原文摘要

We propose a novel modal study of bisimulations. Our contribution is threefold. First, we extend the basic modal language with a new modality $\nbi$, whose intended meaning is universal quantification over all states that are bisimilar to the current one under a given bisimulation. We show that bisimulations are definable in this object language via frame validity (for the forth and back conditions) and model validity (for the atomic harmony condition). Additionally, some other related notions (refinements, simulations, bisimulations for a restricted set of variables, and $n$-bisimulations) are also shown to be definable. Second, we provide a sound and complete axiomatisation of the class of all pairs of Kripke models that are bisimulation-related. Third, we show that the satisfiability problem of this logic is decidable and PSPACE-complete via a translation to standard modal logic $K$ under a simple frame condition. All our results are encoded and verified by Isabelle/HOL.

cs.LO · math.LO

版本更新 · v4arXiv:2403.17961

A categorical formulation of Kraus' paradox

Andrew W. Swan

原文摘要

We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.

math.CT · cs.LO · math.LO

新论文 · 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