Cut-elimination in second order logic

Bulletin of the Section of Logic 17 (3-4):159-160 (1988)
  Copy   BIBTEX

Abstract

As far as I know, the existing proofs of the cut-elimination or normal form theorem in second order logic use means which cannot be formalized in first order arithmetic, and in that sense the above proofs are not elementary . The proof of the normal form theorem for second order logic which I found is elementary.

Categories

Keywords

Reprint years

Links

PhilArchive



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

External links

  • This entry has no external links. Add one.
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

On the form of witness terms.Stefan Hetzl - 2010 - Archive for Mathematical Logic 49 (5):529-554.
On the non-confluence of cut-elimination.Matthias Baaz & Stefan Hetzl - 2011 - Journal of Symbolic Logic 76 (1):313 - 340.
Pure Second-Order Logic with Second-Order Identity.Alexander Paseau - 2010 - Notre Dame Journal of Formal Logic 51 (3):351-360.
CERES in higher-order logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.
Describing proofs by short tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
Algebraic proofs of cut elimination.Jeremy Avigad - manuscript
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Non‐elementary speed‐ups in logic calculi.Toshiyasu Arai - 2008 - Mathematical Logic Quarterly 54 (6):629-640.
Cut‐Elimination Theorem for the Logic of Constant Domains.Ryo Kashima & Tatsuya Shimura - 1994 - Mathematical Logic Quarterly 40 (2):153-172.
Cut-elimination for Weak Grzegorczyk Logic Go.Rajeev Goré & Revantha Ramanayake - 2014 - Studia Logica 102 (1):1-27.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
A cut-elimination proof in intuitionistic predicate logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.

Analytics

Added to PP
2015-02-02

Downloads
0

6 months
0

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references