Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA

Basic Information

• Paper ID: 2507.11643
• Title: Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA
• Authors: Vladimir Kanovei, Vassily Lyubetsky
• Classification: math.LO (Mathematical Logic)
• Publication Date: October 13, 2025
• Paper Link: https://arxiv.org/abs/2507.11643

Abstract

This paper establishes equiconsistency between the theories Z⁻, ZF⁻, ZFC⁻ (where the superscript minus denotes the absence of the Power Set axiom) and PA₂, PA₂⁻ (where the superscript minus denotes the absence of the countable choice axiom schema). The methods employed include the interpretation of set theory without the power set axiom in PA₂⁻ via well-founded trees, and the application of Gödel constructibility within the aforementioned power-set-free set theory.

Research Background and Motivation

Core Problem

This paper addresses a fundamental question in mathematical logic: establishing equiconsistency relationships between several important mathematical theoretical systems. Specifically, it aims to establish equiconsistency among:

• Set-theoretic systems without the power set axiom: Z⁻, ZF⁻, ZFC⁻
• Second-order arithmetic systems: PA₂, PA₂⁻

Significance of the Problem

1. Relationships among foundational mathematical theories: These theories constitute important foundations of modern mathematics, and understanding their logical relationships is of fundamental significance for research in mathematical foundations.
2. Central role of consistency problems: In mathematical logic, consistency is the most basic property of a theory, and equiconsistency relationships reveal the relative strength of different theoretical systems.
3. Historical significance: This result has been known since at least the late 1960s, but has apparently never been published with a complete, self-contained proof.

Limitations of Existing Methods

The authors note that although this theorem has been known since at least the late 1960s, no self-contained and relatively complete proof has apparently ever been published. This serves as the primary motivation for the present paper—to provide such a complete proof.

Core Contributions

1. Complete proof: Provides the first self-contained and complete proof of Theorem 1.1 (the main equiconsistency result)
2. Construction of intermediate theory TMC: Introduces an intermediate theory TMC that extends Z⁻ with three additional axioms
3. Establishment of interpretation relationships: Interprets TMC in PA₂⁻ via well-founded tree structures, and interprets ZFC⁻ in PA₂
4. Application of Gödel constructibility: Develops constructibility theory within the TMC framework and establishes an interpretation of ZFC⁻ in TMC
5. Provision of concrete models: Provides construction of concrete sets or classes L* satisfying ZFC⁻

Detailed Methodology

Task Definition

Prove equiconsistency of the following theories:

• Input theories: PA₂⁻, PA₂, Z⁻, ZFC⁻, ZF⁻
• Output: Establish mutual interpretation relationships among these theories
• Constraints: The proof must be self-contained and independent of unpublished results

Core Architecture

Part One: Tree Structure Interpretation

1. Definition of structure V: Define structure V = ⟨WFT; ∼=, ∼∈⟩ in PA₂⁻, where:
   • WFT is the set of all well-founded trees T ⊆ ω<ω
   • ∼= is the bisimulation equivalence relation between trees
   • ∼∈ is the membership relation defined based on ∼=
2. Establishment of interpretation:
   • Theorem 5.2 proves that V satisfies TMC under PA₂⁻
   • V satisfies ZFC⁻ under PA₂

Part Two: Constructibility Method

1. Intermediate theory TMC: Contains three key axioms
   • Transitive Superset Axiom (TrSups): Every set has a transitive superset
   • Mostowski Collapse Axiom (MostColl): Every well-founded relation admits a transitive model
   • Countability Axiom (Countability): All sets are at most countable
2. Constructible hierarchy: Develops Gödel's constructible hierarchy in TMC:

   L₀[u] = ω ∪ {u}
   Lₐ₊₁[u] = Def Lₐ[u]
   Lλ[u] = ⋃ₐ<λ Lₐ[u]
   L[u] = ⋃ₐ∈Ord Lₐ[u]
   

Technical Innovations

Key Theorem 8.6

Under condition F(u,Ω,K), the set K satisfies ZFC⁻, where F(u,Ω,K) defines two cases:

• Case A: Ω = Ord, K = Lu, and ω₁^Lu does not exist
• Case B: Ω = ω₁^Lu exists, K = L_Ωu

Main Technical Theorem 1.2

L* = {
  L,                    if ω₁^L does not exist
  L_Ω = ⋃ₐ<Ω Lₐ,      if ω₁^L = Ω exists
}

This set or class satisfies ZFC⁻.

Experimental Setup

Theoretical Framework Verification

This is a pure theoretical mathematics work that does not involve experiments in the traditional sense. Verification methods include:

1. Logical reasoning verification: Each theorem is verified through rigorous mathematical proof
2. Consistency checking: Ensures internal consistency of each theoretical system
3. Interpretation relationship verification: Verifies that the established interpretation relationships indeed preserve the axioms and inference rules of the theories

Comparative Methods

• Simpson's approach: The authors compare similarities and differences with related interpretations in Simpson 30, VII.4
• Earlier methods: Reviews earlier interpretation methods defined in 17
• Alternative models: Discusses three other models of ZFC⁻ in Section 13

Main Results

Core Theorem

Theorem 1.1: The theories PA₂⁻, PA₂, Z⁻, ZFC⁻, ZF⁻ are equiconsistent.

Key Intermediate Results

Theorem 5.2 (Interpretation Theorem)

Within the PA₂⁻/PA₂ framework, the structure V is well-defined, and V satisfies TMC/ZFC⁻ respectively.

Theorem 1.3 (Constructibility Result)

Under TMC:

1. L ∩ P(ω) satisfies PA₂
2. L itself satisfies the separation axiom

Corollary 12.1

Under PA₂⁻, L ∩ P(ω) satisfies PA₂, which provides an interpretation of PA₂ in PA₂⁻.

Related Work

Historical Development

• Late 1960s: The result was first discovered (as mentioned in 24)
• Kreisel 24: Early related work
• Simpson 30: Related results within the ATR₀^set theoretical framework
• Marek's series of works: Related techniques in 26, 27

Relationship of This Paper to Related Work

1. Completeness: First provides a completely self-contained proof
2. Method unification: Organically combines tree interpretation methods with constructibility methods
3. Technical improvements: Simplifies certain technical details within the TMC framework

Conclusions and Discussion

Main Conclusions

1. Successfully establishes equiconsistency relationships among five important mathematical theories
2. Provides a complete, self-contained proof method
3. Demonstrates the effective combination of tree interpretation and constructibility methods

Limitations

1. Open problems: The authors raise the question of whether there exists a method for interpreting PA₂ in PA₂⁻ that avoids extensive use of set-theoretic concepts
2. Technical complexity: The proof involves multiple complex technical steps with a high threshold for understanding
3. Limited scope of application: Primarily a foundational theoretical result with limited direct applications

Future Directions

Problem 15.1

Regarding whether the axiom TrSups is truly independent of the remaining axioms of TMC.

Problem 15.2

Seeking a pure analytic proof of Theorem 14.3 in PA₂⁻ that does not explicitly or implicitly involve V or similar derived set-theoretic structures.

Application Prospects

The authors anticipate that this method could be used to strengthen recent applications of Cohen's set-theoretic forcing method in ZFC⁻ and PA₂ theories.

In-Depth Evaluation

Strengths

1. Theoretical completeness: Fills a long-standing gap in proof within this field
2. Methodological innovation: Cleverly combines two classical methods—tree interpretation and constructibility
3. Technical depth: Demonstrates profound technical expertise in mathematical logic
4. Clear exposition: Despite technical complexity, the organizational structure is clear and facilitates understanding

Weaknesses

1. High technical threshold: Requires deep background in mathematical logic for complete understanding
2. Limited practical utility: Primarily a theoretical contribution with limited direct application scenarios
3. Certain proof details: Some proofs (such as Theorem 1.3(II)) provide only outlines

Impact

1. Foundational theoretical contribution: Provides important theoretical tools for mathematical foundations research
2. Methodological value: The demonstrated technical methods can be applied to other related problems
3. Educational value: Can serve as important reference material for advanced mathematical logic courses

Applicable Scenarios

1. Mathematical foundations research: Provides tools for studying relationships among different mathematical theoretical systems
2. Logic research: Provides technical support for model theory and proof theory research
3. Computer science foundations: Provides theoretical foundations for type theory and programming language semantics

References

The paper contains 35 references, spanning from classical works by Gödel and Kleene to recent research on set-theoretic forcing methods, reflecting the historical development and latest advances in this field.

Overall Assessment: This is a high-quality mathematical logic theory paper that successfully resolves an important long-standing problem. Although the technical threshold is high, its theoretical contributions and methodological value make it an important reference in this field.