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

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(03)00021-6

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

My notes

Similar books and articles

The Faithfulness of Fat: A Proof-Theoretic Proof.Fernando Ferreira & Gilda Ferreira - 2015 - Studia Logica 103 (6):1303-1311.
2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.
Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.
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.
A Syntactic Proof of the Decidability of First-Order Monadic Logic.Eugenio Orlandelli & Matteo Tesi - 2024 - Bulletin of the Section of Logic 53 (2):223-244.
The modalized Heyting calculus: a conservative modal extension of the Intuitionistic Logic ★.Leo Esakia - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):349-366.

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