Sequent calculus proof theory of intuitionistic apartness and order relations

Archive for Mathematical Logic 38 (8):521-547 (1999)

Authors
Sara Negri
University of Helsinki
Abstract
Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories of constructive order over the usual theories of order.
Keywords Legacy
Categories (categorize this paper)
DOI 10.1007/s001530050137
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,330
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
Constructive Completions of Ordered Sets, Groups and Fields.Erik Palmgren - 2005 - Annals of Pure and Applied Logic 135 (1-3):243-262.
The Eskolemization of Universal Quantifiers.Rosalie Iemhoff - 2010 - Annals of Pure and Applied Logic 162 (3):201-212.

View all 7 citations / Add more citations

Similar books and articles

Proof-Theoretical Analysis of Order Relations.Sara Negri, Jan von Plato & Thierry Coquand - 2004 - Archive for Mathematical Logic 43 (3):297-309.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A Proof-Search Procedure for Intuitionistic Propositional Logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
An Approach to Infinitary Temporal Proof Theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
A Semantical Proof of De Jongh's Theorem.Jaap van Oosten - 1991 - Archive for Mathematical Logic 31 (2):105-114.
Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):71-92.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.

Analytics

Added to PP index
2013-12-01

Total views
37 ( #248,444 of 2,291,064 )

Recent downloads (6 months)
2 ( #580,277 of 2,291,064 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature