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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

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

An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
A proof–theoretic study of the correspondence of hybrid logic and classical logic.H. Kushida & M. Okada - 2006 - Journal of Logic, Language and Information 16 (1):35-61.
Bounded linear-time temporal logic: A proof-theoretic investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
Reductive logic and proof-search: proof theory, semantics, and control.David J. Pym - 2004 - New York: Oxford University Press. Edited by Eike Ritter.
A proof-theoretic study of the correspondence of classical logic and modal logic.H. Kushida & M. Okada - 2003 - Journal of Symbolic Logic 68 (4):1403-1414.
The structure of logical consequence : proof-theoretic conceptions.Ole T. Hjortland - unknown
Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Proof-theoretic semantic values for logical operators.Nissim Francez & Gilad Ben-avi - 2011 - Review of Symbolic Logic 4 (3):466-478.
About the proof-theoretic ordinals of weak fixed point theories.Gerhard Jäger & Barbara Primo - 1992 - Journal of Symbolic Logic 57 (3):1108-1119.
Towards a Proof-Theoretic Semantics for Dynamic Logics.V. Sikimic - unknown
The proof-theoretic analysis of transfinitely iterated fixed point theories.Gerhard JÄger, Reinhard Kahle, Anton Setzer & Thomas Strahm - 1999 - Journal of Symbolic Logic 64 (1):53-67.
Universes in metapredicative analysis.Christian Rüede - 2003 - Archive for Mathematical Logic 42 (2):129-151.

Analytics

Added to PP
2014-01-16

Downloads
22 (#690,757)

6 months
1 (#1,510,037)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
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.
Bounded linear-time temporal logic: A proof-theoretic investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
A natural deduction system for bundled branching time logic.Stefano Baratella & Andrea Masini - 2013 - Journal of Applied Non-Classical Logics 23 (3):268 - 283.

View all 7 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.
On an Intuitionistic Modal Logic.G. M. Bierman & V. C. V. De Paiva - 2000 - Studia Logica 65 (3):383 - 416.

View all 10 references / Add more references