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: 91,219

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

Type two cuts, bad cuts and very bad cuts.Renling Jin - 1997 - Journal of Symbolic Logic 62 (4):1241-1252.
Strictly positive measures on Boolean algebras.Mirna Džamonja & Grzegorz Plebanek - 2008 - Journal of Symbolic Logic 73 (4):1416-1432.
Effective Cut-elimination for a Fragment of Modal mu-calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
A real of strictly positive effective packing dimension that does not compute a real of effective packing dimension one.Chris J. Conidis - 2012 - Journal of Symbolic Logic 77 (2):447-474.
Normal derivations and sequent derivations.Mirjana Borisavljevi - 2008 - Journal of Philosophical Logic 37 (6):521 - 548.
On the role of implication in formal logic.Jonathan P. Seldin - 2000 - Journal of Symbolic Logic 65 (3):1076-1114.
Cuts in hyperfinite time lines.Renling Jin - 1992 - Journal of Symbolic Logic 57 (2):522-527.
Gentzen formulations of two positive relevance logics.Aleksandar Kron - 1980 - Studia Logica 39 (4):381 - 403.
Gentzen formulations of two positive relevance logics.Aleksandar Kron - 1981 - Studia Logica 40 (3):381 - 403.
Geometry Axioms.Harvey M. Friedman - unknown
The elimination argument.Andrew M. Bailey - 2014 - Philosophical Studies 168 (2):475-482.
Bilateralism in Proof-Theoretic Semantics.Nissim Francez - 2013 - Journal of Philosophical Logic (2-3):1-21.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.

Analytics

Added to PP
2013-10-27

Downloads
21 (#695,936)

6 months
3 (#902,269)

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.
Fragments of HA based on b-induction.Kai F. Wehmeier - 1998 - Archive for Mathematical Logic 37 (1):37-50.

View all 8 references / Add more references