Generation Axioms and Structural Induction: Proof Tools for ρ-Arithmetic
Paper 4 provided the term grammar and two-level equality for ρ-arithmetic, but no tools for proving theorems inside the system. This paper supplies those tools.
First, Paper 4's recursive grammar is lifted to explicit generation axioms (G1–G7), covering zero existence, constructor closure, minimality, injectivity, and disjointness. These axioms make the history-term space the free Σ-term algebra T_Σ over the signature Σ = {0, succ, add, mul}.
Second, the structural induction principle on history terms is defined — a four-branch induction along tree structure (base + successor + addition + multiplication), whose legitimacy follows directly from the minimality axiom G5. Structural induction strictly generalizes PA's mathematical induction: the latter is the degenerate form of the former restricted to pure successor chains.
Third, structural induction is used to prove the first batch of theorems inside ρ-arithmetic: val is a surjective Σ-homomorphism from T_Σ to the standard natural-number Σ-structure ℕ; extensional equality ≡_E = ker(val) is a Σ-congruence; the quotient algebra T_Σ / ≡_E is isomorphic to ℕ; Hist(n) is non-empty for all n; and standard histories are unique.
This paper proves no number-theoretic theorem. Its goal is to turn ρ-arithmetic from a "syntactic specimen" into a "system in which theorems can be proved."
1. Introduction
1.1 From Syntax to Axioms
Paper 4 defined the recursive grammar h ::= 0 | succ(h) | add(h₁, h₂) | mul(h₁, h₂). This grammar implicitly specifies which history terms are legitimate. But "implicit" is not enough — a formal system requires explicit axioms to delimit the legitimacy of its objects and exclude pathological models.
1.2 Positioning via Universal Algebra
In the language of universal algebra, the history-term space defined by Paper 4 is the free term algebra T_Σ over the signature Σ = {0^(0), succ^(1), add^(2), mul^(2)}. val is a Σ-homomorphism from T_Σ to the standard natural-number Σ-structure 𝔑 = (ℕ, 0, S, +, ×).
PA is a first-order theory about 𝔑 — a set of first-order axioms whose standard model is 𝔑. The term model T_Σ of ρ-arithmetic is not a replacement for PA but its "pre-quotient ancestor" — PA is recovered at the structural level after quotienting T_Σ by the congruence ≡_E.
2. Generation Axioms
2.1 Axiom G1: Existence of Zero
0 is a history term.
2.2 Axiom G2: Closure under Successor
If h is a history term, then succ(h) is a history term.
2.3 Axiom G3: Closure under Addition
If h₁, h₂ are history terms, then add(h₁, h₂) is a history term.
2.4 Axiom G4: Closure under Multiplication
If h₁, h₂ are history terms, then mul(h₁, h₂) is a history term.
2.5 Axiom G5: Minimality
History terms are exactly those generated by G1–G4; there are no others.
This axiom ensures the history-term space contains no "ghost terms." It corresponds to PA's minimality condition ("natural numbers are exactly those generated by 0 and successor, nothing else"). In universal algebra, it is equivalent to requiring the history-term space to be the free Σ-term algebra T_Σ.
2.6 Axiom G6: Injectivity of Constructors
Constructors are injective: different inputs produce different outputs.
2.7 Axiom G7: Disjointness of Constructors
Distinct constructors never produce equal terms.
3. Structural Induction Principle
3.1 Statement
Structural Induction on History Terms.
Let P be a property of history terms. If:
(SI-Base) P(0) holds;
(SI-Succ) For all history terms h, if P(h) holds, then P(succ(h)) holds;
(SI-Add) For all history terms h₁, h₂, if P(h₁) and P(h₂) hold, then P(add(h₁, h₂)) holds;
(SI-Mul) For all history terms h₁, h₂, if P(h₁) and P(h₂) hold, then P(mul(h₁, h₂)) holds;
then P(h) holds for all history terms h.
3.2 Legitimacy
The legitimacy of structural induction follows directly from G5 (minimality): history terms are exactly those generated by G1–G4, so any property preserved by each generation step holds for all history terms.
3.3 Relation to PA Mathematical Induction
PA's mathematical induction: if P(0) and ∀n(P(n) → P(S(n))), then ∀n P(n).
This is the degenerate form of structural induction restricted to two constructors (0 and succ). PA induction has two branches (base + successor step); structural induction has four (base + successor + addition + multiplication).
Structural induction handles properties that PA induction cannot. PA induction ranges over natural numbers — extensional objects. Structural induction ranges over history terms — objects with full tree structure. Properties involving the internal structure of history terms (e.g., "term h has no mul root node") are inexpressible in PA (which has no concept of history terms) but provable by structural induction.
4. First Batch of Theorems
4.1 Theorem 1: Well-Definedness of val
Proposition. val is well-defined on all history terms h ∈ T_Σ.
Proof. By structural induction on h. ∎
4.2 Theorem 2: val Is a Σ-Homomorphism
Proposition. val: T_Σ → 𝔑 is a Σ-homomorphism.
4.3 Theorem 3: val Is Surjective
Proposition. For all n ∈ ℕ, there exists h ∈ T_Σ with val(h) = n.
Proof. By PA induction on n. ∎
4.4 Theorem 4: ≡_E Is a Σ-Congruence
Proposition. Extensional equality ≡_E (defined as h₁ ≡_E h₂ iff val(h₁) = val(h₂)) is a Σ-congruence on T_Σ.
4.5 Core Theorem (Theorem 5): Quotient Algebra Isomorphism
Proposition. T_Σ / ≡_E ≅ 𝔑.
Proof. val is a surjective Σ-homomorphism from T_Σ to 𝔑 (Theorems 2+3). ≡_E = ker(val) is a Σ-congruence (Theorem 4). By the First Isomorphism Theorem of universal algebra, T_Σ / ker(val) ≅ Im(val) = 𝔑. ∎
Significance. This theorem precisely answers "what is the relationship between ρ-arithmetic and PA?": PA is a theory about 𝔑; 𝔑 ≅ T_Σ / ≡_E; therefore all theorems of PA automatically hold at the extensional-equality level of T_Σ. ρ-arithmetic retains the full structure of T_Σ; PA sees only its quotient.
4.6 Theorem 6: Uniqueness of Standard History
Proposition. For all n ∈ ℕ, the standard history h_n^std (n nested applications of succ) is the unique element of Hist(n) containing only 0 and succ constructors.
5. Discussion
5.1 What Structural Induction Can Do
Structural induction proves properties of individual history terms h: well-definedness of val, specific structural features (whether a term contains a certain type of subterm), tree-depth bounds, etc. For properties involving Hist(n) as a whole (e.g., the growth rate of |Hist(n)|), structural induction does not directly apply — a mixed strategy combining PA induction (on n) and structural induction (on terms in Hist(n)) is needed.
6. Conclusion
ρ-arithmetic has now progressed from syntax (Paper 4) to axiomatization and proof tools (this paper). The system can now prove theorems internally — it is no longer merely a syntactic specimen but a functioning formal system.
← ZFCρ Paper IV: A Draft Term Model for ρ-Arithmetic
ZFCρ Paper VI: Recursive Definition of ρ and Expression Compression Complexity →
ZFCρ Series · Mathematical Foundations · Back to Papers
Paper 4给出了ρ-算术的项文法和两层等式，但没有给出在ρ-算术内部证明定理的工具。本文补上这一步。
首先，将Paper 4的递归文法提升为显式的生成公理（G1–G7），涵盖零的存在、构造器封闭、最小性、单射性和不相交性。这些公理使历史项空间成为签名 Σ = {0, succ, add, mul} 上的自由 Σ-项代数 T_Σ。
其次，定义历史项上的结构归纳原则——沿树结构的四分支归纳（基础+后继+加法+乘法），直接从最小性公理G5获得合法性。结构归纳严格泛化了PA的数学归纳法：后者是前者在纯后继链上的退化形式。
最后，用结构归纳在ρ-算术内部证明第一批定理：val是从 T_Σ 到标准自然数 Σ-结构 (ℕ, 0, S, +, ×) 的满射 Σ-同态；外延等式 ≡_E = ker(val) 是 Σ-同余关系；商代数 T_Σ / ≡_E 与标准自然数 Σ-结构同构；Hist(n) 对所有 n 非空；标准历史唯一。
本文不证明任何数论定理。它的目标是让ρ-算术从"语法标本"变成"可以在其中证明定理的系统"。
1. 引言
1.1 从语法到公理
Paper 4定义了历史项的递归文法 h ::= 0 | succ(h) | add(h₁, h₂) | mul(h₁, h₂)。这个文法隐式地规定了什么是合法的历史项。但"隐式"不够——一个形式系统需要显式的公理来界定其对象的合法性，排除病态模型。
1.2 项代数的定位
在通用代数（Universal Algebra）的语言中，Paper 4定义的历史项空间是签名 Σ = {0^(0), succ^(1), add^(2), mul^(2)} 上的自由项代数 T_Σ。val是从 T_Σ 到标准自然数 Σ-结构 𝔑 = (ℕ, 0, S, +, ×) 的 Σ-同态。
PA是关于 𝔑 的一阶理论——一组用一阶逻辑句子表述的公理，𝔑 是其标准模型。ρ-算术的项模型 T_Σ 不是PA的替代品，而是PA的"去商化前身"——PA在 T_Σ 通过同余关系 ≡_E 取商之后的结构层面恢复。
2. 生成公理
2.1 公理G1：零的存在
0 是历史项。
2.2 公理G2：后继封闭
若 h 是历史项，则 succ(h) 是历史项。
2.3 公理G3：加法封闭
若 h₁, h₂ 是历史项，则 add(h₁, h₂) 是历史项。
2.4 公理G4：乘法封闭
若 h₁, h₂ 是历史项，则 mul(h₁, h₂) 是历史项。
2.5 公理G5：最小性
历史项恰好是由G1–G4生成的项，没有其他历史项。
这条公理保证历史项空间不包含"幽灵项"——它对应PA中"自然数恰好是0和后继生成的，没有其他自然数"的最小性条件。在通用代数中，它等价于要求历史项空间是自由 Σ-项代数 T_Σ。
2.6 公理G6：构造器的单射性
构造器是单射的：不同的输入产生不同的输出。
2.7 公理G7：构造器的不相交性
不同构造器产生的项永远不相等。
3. 结构归纳原则
3.1 原则陈述
结构归纳原则（Structural Induction on History Terms）。
设 P 是历史项上的性质。若满足以下四个条件：
(SI-Base) P(0) 成立；
(SI-Succ) 对所有历史项 h，若 P(h) 成立，则 P(succ(h)) 成立；
(SI-Add) 对所有历史项 h₁, h₂，若 P(h₁) 且 P(h₂) 成立，则 P(add(h₁, h₂)) 成立；
(SI-Mul) 对所有历史项 h₁, h₂，若 P(h₁) 且 P(h₂) 成立，则 P(mul(h₁, h₂)) 成立；
则 P(h) 对所有历史项 h 成立。
3.2 合法性
结构归纳的合法性直接来自生成公理G5（最小性）：历史项恰好是G1–G4生成的，因此对G1–G4的每一步都保持的性质，必然对所有历史项成立。
3.3 与PA数学归纳法的关系
PA的数学归纳法：若 P(0) 且 ∀n(P(n) → P(S(n)))，则 ∀n P(n)。
这是结构归纳在只有两个构造器（0 和 succ）的特殊情况下的退化形式。PA归纳只有两个分支（基础+后继步），结构归纳有四个分支（基础+后继+加法+乘法）。
结构归纳可以处理PA归纳无法处理的性质。 PA归纳的归纳变量是自然数——一个外延对象。结构归纳的归纳变量是历史项——一个带有完整树结构的对象。涉及历史项内部结构的性质（例如"项h不含mul根节点"）在PA中不可表述（PA没有历史项的概念），但可以用结构归纳来证明。
4. 第一批定理
4.1 定理1：val的良定义性
命题。val对所有历史项 h ∈ T_Σ 良定义。
证明。对 h 做结构归纳。∎
4.2 定理2：val是 Σ-同态
命题。val: T_Σ → 𝔑 是 Σ-同态。
4.3 定理3：val是满射
命题。对所有 n ∈ ℕ，存在 h ∈ T_Σ 使得 val(h) = n。
证明。对 n 做PA归纳。∎
4.4 定理4：≡_E 是 Σ-同余关系
命题。外延等式 ≡_E（定义为 h₁ ≡_E h₂ iff val(h₁) = val(h₂)）是 T_Σ 上的 Σ-同余关系。
4.5 核心定理（定理5）：商代数同构
命题。T_Σ / ≡_E ≅ 𝔑。
证明。val是从 T_Σ 到 𝔑 的满射 Σ-同态（定理2+3）。≡_E = ker(val) 是 Σ-同余（定理4）。由通用代数的第一同构定理，T_Σ / ker(val) ≅ Im(val) = 𝔑。∎
意义。这个定理精确地回答了"ρ-算术与PA是什么关系"：PA是关于 𝔑 的理论；𝔑 同构于 T_Σ / ≡_E；因此PA的所有定理在 T_Σ 的外延等式层自动成立。ρ-算术保留了 T_Σ 的完整结构，PA只看到了它的商。
4.6 定理6：标准历史的唯一性
命题。对所有 n ∈ ℕ，标准历史 h_n^std（n次succ嵌套）是 Hist(n) 中唯一只包含 0 和 succ 构造器的项。
5. 讨论
5.1 结构归纳能做什么
结构归纳可以证明关于单个历史项 h 的性质：val良定义、项的特定结构特征（是否含某种子项）、树深度的上界等。对于涉及 Hist(n) 整体的性质（例如 |Hist(n)| 的增长率），结构归纳不直接适用——需要结合PA归纳（对 n）和结构归纳（对 Hist(n) 中的项）的混合策略。
6. 结论
ρ-算术已从语法（Paper 4）进展到公理化和证明工具（本文）。系统现在可以在内部证明定理——它不再仅仅是语法标本，而是一个功能完整的形式系统。