Notes on Systems of Very Weak Unary Dyadic Arithmetic
Pith reviewed 2026-07-01 07:55 UTC · model grok-4.3
The pith
Weak theories of unary concatenation on dyadic strings are mutually interpretable with Robinson arithmetic R, WT, and WD.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The central claim is that the newly introduced unary-concatenation theories are mutually formally interpretable with WT, WD, and R, and that binary concatenation is first-order definable from unary concatenation in the presence of the initial-segment relation plus either the end-segment relation or the inverse operation on words.
What carries the argument
Mutual formal interpretability mappings constructed from the specific first-order definitions of the unary concatenation theories.
If this is right
- The unary concatenation theories are essentially undecidable.
- Binary concatenation is first-order definable from unary concatenation given the initial segment relation and either the end segment relation or the word inverse.
- Properties provable in any one of WT, WD, R, or the new unary theories transfer to the others via the interpretability mappings.
Where Pith is reading between the lines
- The same definability technique might be used to compare other weak string-based theories that differ only in their choice of concatenation primitives.
- The results suggest that essential undecidability appears already at the level of unary operations on strings once modest ordering or inversion predicates are added.
- One could test whether the interpretability mappings remain total when the language is further restricted by removing the successor or the empty-string constant.
Load-bearing premise
The chosen first-order definitions of the unary theories suffice to build the required interpretability translations to WT, WD, and R.
What would settle it
An explicit model of one unary-concatenation theory in which Robinson arithmetic R fails to be interpretable, or a counterexample to the claimed first-order definition of binary concatenation from unary concatenation plus the stated relations.
read the original abstract
We introduce several very weak first-order theories of unary concatenation of dyadic strings and investigate their relationships to other previously studied veey weak first-order theories, namely the theory WT of binary trees of Kristiansen and Murwanashyaka, the theory WD of binary concatenation of Murwanashyaka, and Robinson's very weak arithmetic R. We prove that all these theories are mutually formally interpretable with the theories of unary concatenation studied in the paper, thus establishing essential undecidability of the latter. In the process we show that binary concatenation is first-order definable from unary concatenation modulo the presence of the initial segment relation plus either the end segment relation or the inverse operation on words, thus giving a positive solution to a problem posed by Karlov.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper introduces several very weak first-order theories of unary concatenation of dyadic strings. It proves that these theories are mutually formally interpretable with WT (binary trees), WD (binary concatenation), and Robinson's R, thereby establishing essential undecidability of the new theories. It also shows that binary concatenation is first-order definable from unary concatenation together with the initial segment relation plus either the end segment relation or the inverse operation on words, positively answering a question of Karlov.
Significance. If the explicit constructions and interpretability mappings hold, the results connect previously studied weak theories and provide a concrete solution to an open definability question using only standard first-order logic. The explicit, parameter-free nature of the definitions and mappings is a positive feature for reproducibility in this area of logic.
minor comments (2)
- Abstract, line 3: 'veey weak' is a typographical error for 'very weak'.
- The manuscript would benefit from a brief overview table or diagram summarizing the interpretability directions between the new unary theories, WT, WD, and R.
Simulated Author's Rebuttal
We thank the referee for the careful reading and the positive recommendation of minor revision. The report contains no specific major comments to address.
Circularity Check
No significant circularity
full rationale
The paper's central results consist of explicit first-order definitions of unary concatenation theories and the construction of mutual interpretability mappings to WT, WD, and R inside standard first-order logic. These mappings are built directly from the introduced axioms and relations (initial segment, end segment, inverse) without reducing to fitted parameters, self-referential definitions, or load-bearing self-citations. The definability of binary concatenation from unary concatenation plus the listed relations is likewise given by concrete formulas that solve Karlov's question by direct construction rather than by renaming or importing uniqueness from prior author work. No step in the derivation chain collapses to an input by construction or relies on an unverified self-citation chain; the argument remains self-contained against external benchmarks in logic.
Axiom & Free-Parameter Ledger
Reference graph
Works this paper leans on
-
[1]
String Theory
Corcoran, J., Frank, W. and Maloney, M.: “String Theory”, in Journal of Symbol Logic, vol. 39, pp. 625-631 (1974)
1974
-
[2]
Mutual interpretability of weak essentially undecidable theories
Damnjanovic, Z.: “Mutual interpretability of weak essentially undecidable theories”, Journal of Symbolic Logic vol. 87(4), pp.1374-1395 (2022)
2022
-
[3]
On interpretability between some weak essentially undecidable theories
Kristiansen, L. and Murwanashyaka, J.: “On interpretability between some weak essentially undecidable theories”, in Beyond the Horizon of Computability, M. Anselmo et al. (eds.), LNCS vol. 12098, pp.63-74, Springer, 2020
2020
-
[4]
Hermes, H.: Semiotik, Eine Theorie der Zeichengestalten als Grundlage für Untersuchungen von formalisierten Sprachen, in Forschungen zur Logik und zur Grundlagen der exakten Wissenschaften, n.s. no. 5, Leipzig, 1938
1938
-
[5]
Algorithmic properties of some fragments of concatenation theory
Karlov, B.: “Algorithmic properties of some fragments of concatenation theory”, in Journal of Physics: Conference Series 1902 012117 (2021)
1902
-
[6]
Weak essentially undecidable theories of concatenation
Murwanashyaka, J.: “Weak essentially undecidable theories of concatenation”, in Archive for Mathematical Logic 61 (7-8), pp. 939–976 (2022)
2022
-
[7]
Die wahrheitsbegriff in den formalisierten Sprachen
Tarski, A.: “Die wahrheitsbegriff in den formalisierten Sprachen”, Studia Philosophica , pp.261-405 (1935). Eng. trans. “The concept of truth in formalized languages”, in Logic, Semantics, Metamathematics, 2nd ed., Indianapolis, IN: Hackett, 1983
1935
-
[8]
Growing commas: a study of sequentiality and concatenation
Visser, A.: “Growing commas: a study of sequentiality and concatenation”, Notre Dame Journal of Formal Logic, vol. 50, pp.61-85 (2009)
2009
-
[9]
Why the theory R is special
Visser, A.: “Why the theory R is special”, in N. Tennant (ed.), Foundational Adventures: Essays in Honour of Harvey Friedman, pp. 7-23, London, College Publications, 2014. 98
2014
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.