Cyclic arithmetic is equivalent to Peano arithmetic
From MaRDI portal
Recommendations
- Equivalence of inductive definitions and cyclic proofs under arithmetic
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
- Automated Reasoning with Analytic Tableaux and Related Methods
- A complete cyclic proof system for inductive entailments in first order logic
- Sequent calculi for induction and infinite descent
Cites work
- scientific article; zbMATH DE number 6680140 (Why is no real title available?)
- scientific article; zbMATH DE number 1956528 (Why is no real title available?)
- scientific article; zbMATH DE number 2087442 (Why is no real title available?)
- A Proof System for Compositional Verification of Probabilistic Concurrent Processes
- A Proof System for the Linear Time μ-Calculus
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated cyclic entailment proofs in separation logic
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Cyclic proofs of program termination in separation logic
- Games for the -calculus
- Infinitary proof theory: the multiplicative additive case
- On global induction mechanisms in aμ-calculus with explicit approximations
- On the Proof Theory of Regular Fixed Points
- On the proof theory of the modal mu-calculus
- Sequent calculi for induction and infinite descent
- The logical strength of Büchi's decidability theorem
Cited in
(35)- Uniform interpolation from cyclic proofs: the case of modal mu-calculus
- Cyclic proofs and size-change termination
- Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
- From GTC to \textsc{Reset}: generating reset proof systems from cyclic proof systems
- scientific article; zbMATH DE number 7155168 (Why is no real title available?)
- Automatic structures and the problem of natural well-orderings
- Coinduction in Flow: The Later Modality in Fibrations
- Cyclic hypersequent system for transitive closure logic
- NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC
- Local validity for circular proofs in linear logic with fixed points
- A complete cyclic proof system for inductive entailments in first order logic
- Cyclic proofs for arithmetical inductive definitions
- scientific article; zbMATH DE number 7089071 (Why is no real title available?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
- Cyclic implicit complexity
- Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
- Infinitary cut-elimination via finite approximations
- Computational expressivity of (circular) proofs with fixed points
- Non-well-founded deduction for induction and coinduction
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
- Integrating induction and coinduction via closure operators and proof cycles
- Abstract cyclic proofs
- Fragments of arithmetic and cyclic proofs
- The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
- Equivalence of inductive definitions and cyclic proofs under arithmetic
- Abstract cyclic proofs
- Cyclic implicit complexity
- Algorithmic complexity of theories with Kleene iteration
- Herbrand schemes for cyclic proofs
- Circular (Yet Sound) Proofs in Propositional Logic
- Herbrand schemes for first-order logic
- Peano arithmetic and MALL
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Proof systems for the modal \(\mu \)-calculus obtained by determinizing automata
This page was built for publication: Cyclic arithmetic is equivalent to Peano arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988374)
