A proof-theoretic view of intensionality

Abstract

We discuss a proof-theoretic view of intensionality. Based on a notion of the use of a formula in a proof we show how a proof-theoretic account can avoid some well-known difficulties of the representation of intensional phenomena. The key example is binary necessity, where we read "A is necessary for B . " as "Every proof of B uses A." Provided that A is an axiom or an atomic proposition we can give a formalized version of this reading. This theory is compared with the standard modal logic approach to necessity and two examples are given. Finally we give an outlook over further applications of the proof-theoretic view of intensionality which turn out to be a nice example of interdisciplinarity between logic, philosophy, linguistics and computer science.