The Term Model of ρ-Arithmetic
This paper completes M3: defining the multi-sorted first-order formal theory T_ρ of ρ-arithmetic, and constructing its term model inside ZFC.
T_ρ has three sorts: H (history terms), N (natural numbers), W (cost values). N-sort satisfies PA. W-sort has Presburger arithmetic signature (addition + order + induction, no multiplication) — cost computation is purely additive. The pure Σ_W-language reduct is Presburger arithmetic (complete, decidable), but T_ρ as a whole is incomplete (due to PA in N-sort). val and ρ are introduced via recursive equations, uniquely determined in the term model by the universal property of initial algebras. T_ρ is a recursively enumerable first-order theory.
Term model: H = T_Σ (free term algebra), N = ℕ, W = ℕ. Within the term model (not in general models), the fibers Hist(n) are countably infinite, the compact subsets Hist*(n) are finite, and the compactification lemma holds.
1. Design Principles
1.1 Strict Alignment with ZFC
All axiom schemata and induction principles use standard ZFC tools. No new meta-theoretical frameworks are introduced. The term model M_c̄ is a concrete set-theoretic object inside ZFC.
1.2 Theory/Model Separation
Sections 2–3 give only the formal theory T_ρ (axioms and signatures). Sections 4–5 construct the term model and verify axiom satisfaction. Section 6 establishes fiber structure within the term model. This separation ensures clarity: formal theory is presented first, then its models.
1.3 Three Sorts, Three Standard Axiom Sources
H-sort: Structural induction schema (paralleling PA induction). N-sort: PA axiom schema. W-sort: Presburger arithmetic signature (no multiplication). The pure Σ_W-language reduct is Presburger arithmetic (complete, decidable), but the full theory T_ρ is not.
2. Formal Language
2.1 Sorts
Three sorts: H (history), N (number), W (weight/cost).
2.2 Signature
2.3 Language-Definable Derived Symbols
≡_E (extensional equality) and Hist(n) are definable within T_ρ's language (model-independent). Hist*(n), ρ_E, ρ_val are term-model objects introduced in Section 6.
3. Formal Theory T_ρ (Axioms)
3.1 H-sort Axioms (Generation and Structural Induction)
G5 Structural Induction Schema: For each first-order formula φ(x, ȳ) with parameters of any sort:
G6: Constructor injectivity: succ(h₁) = succ(h₂) ⟹ h₁ = h₂, and similarly for add and mul.
G7: Constructor disjointness: distinct constructors never produce equal terms.
3.2 N-sort Axioms
Standard Peano axioms: zero exists, successor is injective and never returns to zero, addition and multiplication are associative and commutative with standard properties, N-sort induction schema holds.
3.3 W-sort Axioms (Presburger Arithmetic)
Presburger signature: S_W(w) ≠ 0_W, S_W injective, recursive axioms for +_W defining it via ∃u(w+u=v), order ≤_W via ∃u(w+u=v), W-sort induction schema. Non-zero friction axioms: c_S ≠ 0_W ∧ c_⊕ ≠ 0_W ∧ c_⊗ ≠ 0_W. Note: N has multiplication (needed for val of mul), W does not (ρ uses only addition and constants).
3.4 Cross-Sort Recursive Equations
4. Construction of the Term Model
4.1 Carrier Sets
H-sort: T_Σ, the free Σ_H-term algebra. In ZFC, this is the set of all finite labeled rooted trees over signature Σ_H, countable.
N-sort: ℕ (ω), the standard natural numbers in ZFC.
W-sort: ℕ (same ω, but with different semantic role: Presburger structure with no multiplication).
4.2 Parameterization
For any (c_S, c_⊕, c_⊗) ∈ ℕ³ with all components > 0, the term model M_c̄ exists. Default: c_S = 1, c_⊕ = 1, c_⊗ = 2.
5. Axiom Satisfaction
5.1 H-sort
G5: Satisfied via minimality of T_Σ in ZFC. Structural induction on T_Σ follows from the fact that T_Σ is the least set containing 0_H and closed under succ, add, mul.
G6–G7: Free algebra properties: distinct constructors produce syntactically different terms.
5.2 N-sort and W-sort
ℕ satisfies PA and Presburger axioms by standard results in ZFC. Full-language induction schema verified via ω's inductive property.
5.3 val and ρ — Two Canonical Projections
Theorem (Initial Algebra Universality). T_Σ is the initial Σ_H-algebra. val: T_Σ → 𝔑 is the unique Σ_H-homomorphism to the N-sort algebra (viewing ℕ with its Σ_H-structure: 0_N, S_N, +_N, ×_N). ρ: T_Σ → A_c̄ is the unique Σ_H-homomorphism to the cost algebra A_c̄ = (ℕ; 0, x↦x+c_S, (x,y)↦x+y+c_⊕, (x,y)↦x+y+c_⊗).
Proof idea: By recursion on T_Σ's tree structure, we define val and ρ bottom-up. Uniqueness follows from initiality.
Significance: val projects to extensional values; ρ projects to operative costs. Both are canonical because they are the unique homomorphisms from the initial algebra.
5.4 Term-Model Existence Theorem
Theorem. In ZFC, for any positive integer parameters (c_S, c_⊕, c_⊗), M_c̄ satisfies all axioms and equations of T_ρ.
6. Fiber Structure of the Term Model
6.1 Hist(n) Is Countably Infinite
Theorem. |Hist(n)| = ℵ₀ (countably infinite).
Proof of Countability: Hist(n) ⊆ T_Σ. Since T_Σ is countable (finite-tree encoding in ℕ), Hist(n) is countable.
Proof of Infinitude: Define injection f: ω → Hist(n) by f(k) = succ^k(h_n^std), where h_n^std is the standard history (n nested successors). By G6 (injectivity of succ), f is injective. By G2 (closure under successor), all f(k) ∈ Hist(n). ∎
6.2 Hist*(n) Is Finite
Definition (Compact): A history term h is compact iff no subterm of h is a trivial operation (adding zero, multiplying by one, multiplying by zero).
Definition: Hist*(n) = {h ∈ Hist(n) : h is compact}.
Theorem. Hist*(n) is non-empty and finite.
Proof (sketch): Non-emptiness: h_n^std is compact. Finiteness: compactness requires every add child to have val > 0 and every mul child to have val > 1 (Paper 6 §2). Each child's val is strictly less than parent's val, so tree depth is bounded by n. Finite depth + finite branching ⟹ finite set. ∎
6.3 Compactification Lemma
Theorem. For every h ∈ Hist(n), there exists h* ∈ Hist*(n) with ρ(h*) ≤_W ρ(h).
Proof: Apply six cross-sort semantic reduction rules R₁–R₆ bottom-up until no more apply (termination by well-foundedness of ℕ):
Each rule strictly decreases ρ (by non-zero friction + Presburger monotonicity). The result h* is compact. ∎
Note: Compactification asserts existence, not uniqueness of normal forms. succ(succ(0_H)) and add(succ(0_H), succ(0_H)) are both in Hist*(2) but distinct.
6.4 ρ_E and ρ_val (Term-Model Objects)
Definition:
Well-defined because Hist*(n) is finite and non-empty (§6.2).
Theorem (Compactification Characterization): By §6.3, ρ_E(n) = inf_{Hist(n)} ρ. The minimum over the countably infinite Hist(n) equals the minimum over its finite subset Hist*(n).
Definition:
Note: ρ_E and ρ_val are term-model objects; not guaranteed to exist in general T_ρ-models where Hist(n) may not be finite.
7. Categorical Properties
T_Σ is the initial Σ_H-algebra. val and ρ are its two canonical projections (universal morphisms in the category of Σ_H-algebras). This categorical perspective unifies their definitions.
8. Derived Theorems from Papers 5–6
8.1 Structural Theorems (All Parameters)
From Paper 5: val surjective, ≡_E congruence, T_Σ/≡_E ≅ 𝔑. From Paper 6: ρ_E recurrence and δ monotonicity.
8.2 Default Parameters (c_S=1, c_⊕=1, c_⊗=2)
Addition Domination Lemma: For all n ≥ 2, addition paths are dominated by successor paths.
Prime Fixed-Point Theorem: If n is prime, then δ(n) = δ(n-1).
ρ_E Recurrence: ρ_E(n) = min(ρ_E(n-1) + 1, min_{ab=n, a,b>1} (ρ_E(a) + ρ_E(b) + 2)).
9. Open Problems
- Growth rate of |Hist*(n)|. What is the density of compact terms in Hist(n)?
- Full relative consistency formalization: Con(ZFC) ⇒ Con(T_ρ) — covered in Paper 8.
- Non-standard models of T_ρ. Do non-standard models exist? What are their H-sort fibers?
- Uniqueness of val/ρ in non-initial-algebra models. In non-standard models, are val and ρ still uniquely determined?
- Homomorphisms from T_Σ to other Σ_H-algebras. What is the general structure of morphism-pairs?
← ZFCρ Paper VI: Recursive Definition of ρ and Expression Compression Complexity
ZFCρ Paper VIII: Proof-Theoretic Equivalence and Conservative Extension →
ZFCρ Series · Mathematical Foundations · Back to Papers
本文完成M3：定义ρ-算术的多排序一阶形式理论T_ρ，并在ZFC内部构造其项模型。
T_ρ有三个排序：H（历史项）、N（自然数）、W（代价值）。N-sort满足PA。W-sort的签名是Presburger算术签名（加法+序+归纳，无乘法）——代价的计算是纯加法的线性累积。W-sort的纯Σ_W-语言reduct是Presburger算术（完备，可判定），但整个T_ρ因包含N-sort的PA而不完备。val和ρ通过递归方程引入，在项模型中由初始代数泛性质唯一确定。T_ρ是可递归枚举的一阶理论。
项模型：H = T_Σ（自由项代数），N = ℕ，W = ℕ。在项模型中（而非一般模型中），val的纤维Hist(n)可数无穷，紧凑子集Hist*(n)有限，紧凑化引理成立，ρ_E良定义。
1. 设计原则
1.1 严格对齐ZFC
所有公理模式和归纳原则都使用标准ZFC工具。不引入新的元理论框架。项模型M_c̄是ZFC内的具体集合论对象。
1.2 理论与模型的分离
第2–3节只给出形式理论T_ρ（公理和签名）。第4–5节构造项模型并验证公理满足性。第6节确定项模型内的纤维结构。这个分离确保了清晰性：形式理论先呈现，然后讨论其模型。
1.3 三个排序，三个标准公理来源
H-sort：结构归纳模式（平行PA归纳）。N-sort：PA公理模式。W-sort：Presburger算术签名（无乘法）。W-sort的纯Σ_W-语言reduct是Presburger算术（完备，可判定），但整个T_ρ不完备。
2. 形式语言
2.1 排序
三个排序：H（历史）、N（数）、W（权/代价）。
2.2 签名
2.3 语言可定义的导出符号
≡_E（外延等式）和Hist(n)可在T_ρ的语言内定义（与模型无关）。Hist*(n)、ρ_E、ρ_val是第6节介绍的项模型对象。
3. 形式理论T_ρ（公理）
3.1 H-sort公理（生成和结构归纳）
G5结构归纳模式：对于任何一阶公式φ(x, ȳ)及任意排序的参数：
G6：构造器单射性：succ(h₁) = succ(h₂) ⟹ h₁ = h₂，add和mul类似。
G7：构造器不相交性：不同的构造器产生的项永不相等。
3.2 N-sort公理
标准Peano公理：零的存在、后继的单射性和非零返性、加法乘法的标准性质、N-sort归纳模式。
3.3 W-sort公理（Presburger算术）
Presburger签名：S_W(w) ≠ 0_W，S_W单射，+_W通过∃u(w+u=v)递归定义，≤_W通过同样方式定义，W-sort归纳模式。非零摩擦公理：c_S ≠ 0_W ∧ c_⊕ ≠ 0_W ∧ c_⊗ ≠ 0_W。注意：N有乘法（val(mul需要），W没有（ρ只用加法和常数）。
3.4 跨排序递归方程
4. 项模型的构造
4.1 承载集
H-sort：T_Σ，自由Σ_H-项代数。在ZFC中，这是签名Σ_H上所有有限标记根树的集合，可数。
N-sort：ℕ（ω），ZFC中的标准自然数。
W-sort：ℕ（同一个ω，但语义角色不同：Presburger结构，无乘法）。
4.2 参数化
对任何(c_S, c_⊕, c_⊗) ∈ ℕ³且所有分量 > 0，项模型M_c̄存在。默认：c_S = 1, c_⊕ = 1, c_⊗ = 2。
5. 公理满足性
5.1 H-sort
G5：通过T_Σ在ZFC中的最小性满足。T_Σ上的结构归纳源于T_Σ是包含0_H并在succ、add、mul下闭包的最小集合这一事实。
G6–G7：自由代数的性质：不同的构造器产生语法上不同的项。
5.2 N-sort和W-sort
ℕ满足PA和Presburger公理（ZFC中的标准结果）。完整语言归纳模式通过ω的归纳性质验证。
5.3 val和ρ——两个规范投影
定理（初始代数泛性）。T_Σ是初始Σ_H-代数。val: T_Σ → 𝔑是到N-sort代数的唯一Σ_H-同态（看作带Σ_H-结构的ℕ：0_N, S_N, +_N, ×_N）。ρ: T_Σ → A_c̄是到代价代数的唯一Σ_H-同态，其中A_c̄ = (ℕ; 0, x↦x+c_S, (x,y)↦x+y+c_⊕, (x,y)↦x+y+c_⊗)。
证明思路：在T_Σ的树结构上递归定义val和ρ，自底向上。唯一性源于初始性。
意义：val投影到外延值；ρ投影到操作代价。两者都是规范的，因为它们是从初始代数出发的唯一同态。
5.4 项模型存在定理
定理。在ZFC中，对任何正整数参数(c_S, c_⊕, c_⊗)，M_c̄满足T_ρ的所有公理和方程。
6. 项模型的纤维结构
6.1 Hist(n)可数无穷
定理。|Hist(n)| = ℵ₀（可数无穷）。
可数性证明：Hist(n) ⊆ T_Σ。由于T_Σ可数（有限树编码到ℕ），Hist(n)可数。
无穷性证明：定义单射f: ω → Hist(n)，f(k) = succ^k(h_n^std)，其中h_n^std是标准历史（n重后继嵌套）。由G6（后继单射性），f单射。由G2（后继闭包），所有f(k) ∈ Hist(n)。∎
6.2 Hist*(n)有限
定义（紧凑）：历史项h是紧凑的，当且仅当h的任何子项都不是平凡操作（加零、乘一、乘零）。
定义：Hist*(n) = {h ∈ Hist(n) : h是紧凑的}。
定理。Hist*(n)非空且有限。
证明（草图）：非空性：h_n^std是紧凑的。有限性：紧凑性要求每个add子项的val > 0，每个mul子项的val > 1（Paper 6 §2）。每个子项的val严格小于父项的val，所以树深度被n有界。有限深度 + 有限分支 ⟹ 有限集。∎
6.3 紧凑化引理
定理。对每个h ∈ Hist(n)，存在h* ∈ Hist*(n)使得ρ(h*) ≤_W ρ(h)。
证明：自底向上应用六条跨排序语义化简规则R₁–R₆直到不可再化（通过ℕ的良基性保证终止）：
每条规则严格减小ρ（非零摩擦 + Presburger单调性）。结果h*是紧凑的。∎
注：紧凑化证明存在性，不证明唯一性。succ(succ(0_H))和add(succ(0_H), succ(0_H))都在Hist*(2)中但互不相同。
6.4 ρ_E和ρ_val（项模型对象）
定义：
由Hist*(n)的有限性和非空性良定义（§6.2）。
定理（紧凑化刻画）：由§6.3，ρ_E(n) = inf_{Hist(n)} ρ。可数无穷集Hist(n)的下确界等于其有限子集Hist*(n)的最小值。
定义：
注：ρ_E和ρ_val是项模型对象；在一般T_ρ-模型中不保证存在（因为Hist(n)可能不有限）。
7. 范畴性质
T_Σ是初始Σ_H-代数。val和ρ是其两个规范投影（Σ_H-代数范畴中的泛态射）。这个范畴视角统一了它们的定义。
8. Paper 5–6的导出定理
8.1 结构定理（所有参数）
Paper 5：val满射、≡_E同余、T_Σ/≡_E ≅ 𝔑。Paper 6：ρ_E递推和δ单调性。
8.2 默认参数（c_S=1, c_⊕=1, c_⊗=2）
加法支配引理：对所有n ≥ 2，加法路径被后继路径支配。
素数不动点定理：若n是素数，则δ(n) = δ(n-1)。
ρ_E递推：ρ_E(n) = min(ρ_E(n-1) + 1, min_{ab=n, a,b>1} (ρ_E(a) + ρ_E(b) + 2))。
9. 开放问题
- |Hist*(n)|的增长率。紧凑项在Hist(n)中的密度是多少？
- 完整的相对一致性形式化：Con(ZFC) ⇒ Con(T_ρ)——Paper 8涵盖。
- T_ρ的非标准模型。非标准模型是否存在？它们的H-sort纤维是什么？
- 非初始代数模型中val/ρ的唯一性。在非标准模型中，val和ρ仍是唯一确定的吗？
- 从T_Σ到其他Σ_H-代数的同态。态射对的一般结构是什么？