Quick cut-elimination for strictly positive cuts

Annals of Pure and Applied Logic 162 (10):807-815 (2011)
  Copy   BIBTEX

Abstract

In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2011.03.002

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,953

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Intuitionistic Fixed Point Theories for Strictly Positive Operators.Christian Rüede & Thomas Strahm - 2002 - Mathematical Logic Quarterly 48 (2):195-202.
A cut-elimination proof in intuitionistic predicate logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.
Cut elimination for a simple formulation of epsilon calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.
Epsilon substitution for transfinite induction.Henry Towsner - 2005 - Archive for Mathematical Logic 44 (4):397-412.
Gentzen’s consistency proof without heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Epsilon substitution for $$\textit{ID}_1$$ ID 1 via cut-elimination.Henry Towsner - 2018 - Archive for Mathematical Logic 57 (5-6):497-531.
Revisiting the conservativity of fixpoints over intuitionistic arithmetic.Mattias Granberg Olsson & Graham E. Leigh - 2023 - Archive for Mathematical Logic 63 (1):61-87.
Cut elimination for the unified logic.Jacqueline Vauzeilles - 1993 - Annals of Pure and Applied Logic 62 (1):1-16.
Cut normal forms and proof complexity.Matthias Baaz & Alexander Leitsch - 1999 - Annals of Pure and Applied Logic 97 (1-3):127-177.
Algebraic proof theory for substructural logics: cut-elimination and completions.Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui - 2012 - Annals of Pure and Applied Logic 163 (3):266-290.

Analytics

Added to PP
2013-10-27

Downloads
23 (#704,118)

6 months
4 (#862,849)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Proof theory of weak compactness.Toshiyasu Arai - 2013 - Journal of Mathematical Logic 13 (1):1350003.
Intuitionistic fixed point theories over set theories.Toshiyasu Arai - 2015 - Archive for Mathematical Logic 54 (5-6):531-553.

Add more citations

References found in this work

Fragments of $HA$ based on $\Sigma_1$ -induction.Kai F. Wehmeier - 1997 - Archive for Mathematical Logic 37 (1):37-49.
Fragments of Heyting arithmetic.Wolfgang Burr - 2000 - Journal of Symbolic Logic 65 (3):1223-1240.
An intuitionistic fixed point theory.Wilfried Buchholz - 1997 - Archive for Mathematical Logic 37 (1):21-27.

View all 8 references / Add more references