Cover Image

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bryce, Aaron, Gore', Rajeev
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Peano Arithmetic and $μ$MALL
by: Manighetti, Matteo, et al.
Published: (2023)

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
by: Ito, Sohei, et al.
Published: (2025)

Constructive Ordinal Exponentiation
by: de Jong, Tom, et al.
Published: (2025)

Towards an Analysis of Proofs in Arithmetic
by: Leitsch, Alexander, et al.
Published: (2025)

Tableau methodology for propositional logics
by: Jarmuzek, T., et al.
Published: (2025)

Verified and Optimized Implementation of Orthologic Proof Search
by: Guilloud, Simon, et al.
Published: (2025)

Translating Informal Proofs into Formal Proofs Using a Chain of States
by: Wang, Ziyu, et al.
Published: (2025)

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
by: Pacheco, Leonardo
Published: (2026)

Peano Arithmetic, games and descent recursion
by: Frittaion, Emanuele
Published: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

A Formally Verified Lightning Network
by: Fabiański, Grzegorz, et al.
Published: (2025)

Formally Verified Animation for RoboChart using Interaction Trees
by: Ye, Kangfeng, et al.
Published: (2023)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
by: Komel, Anja Petković, et al.
Published: (2025)

A Formal Proof of R(4,5)=25
by: Gauthier, Thibault, et al.
Published: (2024)

Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
by: Stevens, Lukas, et al.
Published: (2025)

Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
by: Atserias, Albert, et al.
Published: (2024)

Formally Verified Approximate Policy Iteration
by: Schäffeler, Maximilian, et al.
Published: (2024)

The Arithmetical Hierarchy: A Realizability-Theoretic Perspective
by: Kihara, Takayuki
Published: (2024)

Proofs that Modify Proofs, 1/2
by: Towsner, Henry
Published: (2025)

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
by: Kohlen, Bram, et al.
Published: (2025)

Pseudo-Formalization for Automatic Proof Verification
by: Barkallah, Slim, et al.
Published: (2026)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Unravelling Cyclic First-Order Arithmetic
by: Leigh, Graham E., et al.
Published: (2025)

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
by: Dvorak, Martin, et al.
Published: (2025)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
by: Bryant, Dustin, et al.
Published: (2025)

A Dichotomy Theorem for Ordinal Ranks in MSO
by: Niwiński, Damian, et al.
Published: (2025)

A Formal Proof of Complexity Bounds on Diophantine Equations
by: Bayer, Jonas, et al.
Published: (2025)

On proving consistency of equational theories in Bounded Arithmetic
by: Beckmann, Arnold, et al.
Published: (2022)

Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
by: Mohanty, Hansa, et al.
Published: (2025)

Formally Verified Certification of Unsolvability of Temporal Planning Problems
by: Wang, David, et al.
Published: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda
by: Wißmann, Thorsten, et al.
Published: (2024)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
by: Bryant, Randal E., et al.
Published: (2025)

The Proof Analysis Problem
by: Arteche, Noel, et al.
Published: (2025)

Abstraction-Based Proof Production in Formal Verification of Neural Networks
by: Elboher, Yizhak Yisrael, et al.
Published: (2025)

Proof-theoretic Semantics for Second-order Logic
by: Gheorghiu, Alexander V., et al.
Published: (2025)

Proof-theoretic Semantics for the Logic of Bunched Implications
by: Gu, Tao, et al.
Published: (2023)

Proof-theoretic Semantics for First-order Logic
by: Gheorghiu, Alexander V.
Published: (2024)

Cyclic Proofs for iGL via Corecursion
by: Miranda, Borja Sierra
Published: (2023)