A proof-theoretic investigation of a logic of positions

Annals of Pure and Applied Logic 123 (1-3):135-162 (2003)
  Copy   BIBTEX

Abstract

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,486

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

2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
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, Advances in Modal Logic. CSLI Publications. pp. 43-66.
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, Advances in Modal Logic. CSLI Publications. pp. 43-66.
Strong normalization results by translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.
Constructive theories through a modal lens.Matteo Tesi - 2025 - Logic Journal of the IGPL 33 (1):149-172.
Atomic polymorphism.Fernando Ferreira & Gilda Ferreira - 2013 - Journal of Symbolic Logic 78 (1):260-274.

Analytics

Added to PP
2014-01-16

Downloads
40 (#598,982)

6 months
10 (#312,841)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Natural deduction calculi for classical and intuitionistic S5.S. Guerrini, A. Masini & M. Zorzi - 2023 - Journal of Applied Non-Classical Logics 33 (2):165-205.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
A Natural Deduction Calculus for S4.2.Simone Martini, Andrea Masini & Margherita Zorzi - 2024 - Notre Dame Journal of Formal Logic 65 (2):127-150.
Strong Normalization of Program-Indexed Lambda Calculus.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (1/2):65-78.

View all 8 citations / Add more citations

References found in this work

Semantical Analysis of Modal Logic I. Normal Propositional Calculi.Saul A. Kripke - 1963 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9 (5‐6):67-96.
Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.
On an intuitionistic modal logic.G. M. Bierman & V. C. V. de Paiva - 2000 - Studia Logica 65 (3):383-416.
Sequent-systems for modal logic.Kosta Došen - 1985 - Journal of Symbolic Logic 50 (1):149-168.
2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.

View all 8 references / Add more references