S. Baratella and A. Masini. A proof-theoretic investigation of a logic of positions. Annals of Pure and Applied Logic, 123:135-162, 2003.

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.

[ bib | http ]

Back