The Hauptsatz for Stratified Comprehension: A Semantic Proof

Mathematical Logic Quarterly 40 (4):481-489 (1994)
  Copy   BIBTEX

Abstract

We prove the cut-elimination theorem, Gentzen's Hauptsatz, for the system for stratified comprehension, i. e. Quine's NF minus extensionality.

Links

PhilArchive



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

External links

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

Through your library

Similar books and articles

Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Consistency of strictly impredicative NF and a little more ….Sergei Tupailo - 2010 - Journal of Symbolic Logic 75 (4):1326-1338.
A proof of Gentzen's Hauptsatz without multicut.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (1):9-18.
Proof theory and set theory.Gaisi Takeuti - 1985 - Synthese 62 (2):255 - 263.
Proof-relevance of families of setoids and identity in type theory.Erik Palmgren - 2012 - Archive for Mathematical Logic 51 (1-2):35-47.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Harrington’s conservation theorem redone.Fernando Ferreira & Gilda Ferreira - 2008 - Archive for Mathematical Logic 47 (2):91-100.
Relating Quine's NF to Feferman's EM.Andrea Cantini - 1999 - Studia Logica 62 (2):141-162.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.

Analytics

Added to PP
2013-12-01

Downloads
22 (#729,508)

6 months
9 (#352,597)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The Axiom Scheme of Acyclic Comprehension.Zuhair Al-Johar, M. Randall Holmes & Nathan Bowler - 2014 - Notre Dame Journal of Formal Logic 55 (1):11-24.
Cuts and gluts.Marcel Crabbé - 2005 - Journal of Applied Non-Classical Logics 15 (3):249-263.

Add more citations

References found in this work

Proof theory.Gaisi Takeuti - 1975 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.

Add more references