Cyclic Arithmetic Is Equivalent to Peano Arithmetic

DOI10.1007/978-3-662-54458-7_17zbMath1486.03095OpenAlexW2611879577MaRDI QIDQ2988374

Alex K. Simpson

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54458-7_17

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Structure of proofs (03F07) Second- and higher-order arithmetic and fragments (03F35)

Related Items (14)

Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cyclic hypersequent system for transitive closure logic ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Abstract cyclic proofs ⋮ Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs ⋮ Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent ⋮ Non-well-founded deduction for induction and coinduction ⋮ NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC ⋮ Integrating induction and coinduction via closure operators and proof cycles

Uses Software

• Cyclist

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Games for the \(\mu\)-calculus
• On the proof theory of the modal mu-calculus
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Sequent calculi for induction and infinite descent
• Cyclic proofs of program termination in separation logic
• On the Proof Theory of Regular Fixed Points
• On global induction mechanisms in aμ-calculus with explicit approximations
• A Proof System for Compositional Verification of Probabilistic Concurrent Processes
• Automated Cyclic Entailment Proofs in Separation Logic
• The Logical Strength of Büchi's Decidability Theorem
• A Proof System for the Linear Time μ-Calculus
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: Cyclic Arithmetic Is Equivalent to Peano Arithmetic