pith. sign in

arxiv: 2602.02854 · v2 · submitted 2026-02-02 · 🧮 math.LO

Categoricity for an inferential ω-logic and in L_(ω₁,ω)

John T. Baldwin , Constantin C. Br\^incu\c{s} This is my paper

Pith reviewed 2026-05-16 08:06 UTC · model grok-4.3

classification 🧮 math.LO MSC 03C35
keywords categoricityω-logicinferential rulesRobinson arithmeticPeano arithmeticL_ω1,ωmodel theoryω-rules
0
0 comments X

The pith

Adding ω-rules to first-order logic makes Robinson's Q and Peano arithmetic categorical.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends first-order logic in two ways with ω-rules and characterizes the countable structures that become categorical under each extension. In the one-sorted inferential ω-logic, Robinson's Q and Peano Arithmetic each have only one countable model. In the two-sorted generalized ω-logic, every complete sentence of L_ω1,ω defines exactly the same class of structures as some first-order theory together with the G-ω-rule. The central step is showing that the added rules fix unique truth conditions for the connectives and quantifiers.

Core claim

In the one-sorted inferential ω-logic both Robinson's system Q and Peano Arithmetic become categorical. In the two-sorted generalized ω-logic each complete L_ω1,ω sentence defines the same class of structures as a first-order theory with the appropriate G-ω-rule. These results rest on showing that the inferential rules uniquely determine certain truth-conditions for the logical connectives and quantifiers.

What carries the argument

The inferential ω-rules that license inference from all finite instances to the infinite case, together with the proof that these rules fix unique truth conditions for the logical symbols.

Load-bearing premise

That the inferential rules uniquely determine the truth-conditions for the logical connectives and quantifiers.

What would settle it

A countable non-isomorphic model of Q or of Peano Arithmetic that still satisfies every instance of the inferential ω-rules, or an explicit counterexample showing that the rules fail to fix unique truth conditions for some connective or quantifier.

read the original abstract

This paper provides two extensions of first order logic by `$\omega$-rules'. In each case we characterize the countable structures whose theory in the logic is categorical (has a unique model). In the one-sorted inferential $\omega$-logic, both Robinson's system $Q$ and Peano Arithmetic become categorical. In the two-sorted generalized $\omega$-logic we show each complete $L_{\omega_1,\omega}$ sentence defines the same class of structures as a first-order theory with the appropriate $G-\omega$-rule. The results depend on proving that the inferential rules for the logics are categorical, i.e. they uniquely determine certain truth-conditions for the logical connectives and quantifiers.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript introduces two extensions of first-order logic via ω-rules. In the one-sorted inferential ω-logic, Robinson's Q and Peano Arithmetic are shown to be categorical. In the two-sorted generalized ω-logic, every complete L_{ω1,ω} sentence is shown to define the same class of structures as a first-order theory equipped with the corresponding G-ω-rule. Both results rest on a proof that the inferential rules uniquely determine truth-conditions for the logical connectives and quantifiers.

Significance. If the rule-categoricity arguments are correct, the work supplies concrete mechanisms for restoring categoricity to arithmetic theories inside extended logics and for equating certain infinitary sentences with first-order theories plus a generalized rule. This supplies new model-theoretic characterizations that could be useful for studying non-standard models of arithmetic and the expressive power of L_{ω1,ω}.

major comments (2)
  1. [§3] §3 (one-sorted case): the uniqueness argument that the inferential rules fix the truth-conditions for the ω-rule does not contain an explicit lemma ruling out alternative satisfaction clauses that obey the rules yet permit non-standard interpretations of the natural numbers; without this, the claimed categoricity of Q and PA does not follow.
  2. [§5] §5 (two-sorted case): the reduction showing that a complete L_{ω1,ω} sentence is equivalent to a first-order theory plus G-ω-rule assumes the rules are categorical, but the text provides no model-theoretic verification that non-standard ω-interpretations are excluded by the inference system alone.
minor comments (1)
  1. [§2] The notation distinguishing the one-sorted inferential ω-rule from the two-sorted G-ω-rule is introduced only informally; a short definitional paragraph in §2 would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive comments. We agree that making the uniqueness arguments more explicit will improve the manuscript. Below we respond to each major comment.

read point-by-point responses

  1. Referee: [§3] §3 (one-sorted case): the uniqueness argument that the inferential rules fix the truth-conditions for the ω-rule does not contain an explicit lemma ruling out alternative satisfaction clauses that obey the rules yet permit non-standard interpretations of the natural numbers; without this, the claimed categoricity of Q and PA does not follow.

    Authors: The proof in §3 proceeds by assuming an arbitrary satisfaction relation that obeys the inferential rules and deriving that it must coincide with the standard Tarskian semantics on the natural numbers. This is shown by induction on formula complexity, where the ω-rule forces that if all finite instances hold, the universal quantifier holds, which in turn pins down the domain to be the standard naturals for models of Q or PA. However, we acknowledge that presenting this as a standalone lemma would make the argument clearer. In the revision, we will add an explicit Lemma 3.X stating that any rule-obeying satisfaction relation excludes non-standard ω-interpretations. revision: partial

  2. Referee: [§5] §5 (two-sorted case): the reduction showing that a complete L_{ω1,ω} sentence is equivalent to a first-order theory plus G-ω-rule assumes the rules are categorical, but the text provides no model-theoretic verification that non-standard ω-interpretations are excluded by the inference system alone.

    Authors: In §5, the equivalence relies on the categoricity result from the one-sorted case, extended to the two-sorted setting. The G-ω-rule is designed to enforce the same uniqueness for the ω-part. We will add a model-theoretic verification in the form of a proposition showing that the inference system alone forces standard interpretations of the ω-sort, thereby supporting the reduction without circularity. revision: partial

Circularity Check

0 steps flagged

No significant circularity; derivation relies on independent proof of rule categoricity

full rationale

The paper states that its main results (categoricity of Q and PA in one-sorted inferential ω-logic, and equivalence of complete L_ω1,ω sentences to first-order theories with G-ω-rule) depend on proving that the inferential rules uniquely determine truth-conditions for connectives and quantifiers. This is presented as a load-bearing lemma or theorem established within the paper itself rather than by construction from the target conclusions or by self-citation chains. No equations, definitions, or steps are exhibited that reduce a 'prediction' or categoricity claim back to fitted parameters, renamed inputs, or ansatzes smuggled via prior self-work. The abstract and description indicate standard model-theoretic arguments grounding the uniqueness of the rules, making the overall chain self-contained without the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the assumption that the added inferential rules uniquely fix truth conditions for connectives and quantifiers in countable structures; no free parameters or invented entities are mentioned.

axioms (1)
  • domain assumption Standard first-order logic axioms plus the new ω-rules determine unique truth conditions for countable models
    Invoked to prove categoricity of Q and PA and the equivalence with L_ω1,ω

pith-pipeline@v0.9.0 · 5426 in / 1198 out tokens · 46131 ms · 2026-05-16T08:06:27.529345+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Carnapian Frameworks and Categoricity of Arithmetic via Inferential $\omega$-logics

    math.LO 2026-04 unverdicted novelty 7.0

    Inferential ω-logics make arithmetic categorical in a way that answers philosophical challenges about unique models within Carnapian frameworks without presupposing the arithmetical concepts being secured.