Mathematical Structures in Computer Science

Table of Contents - 2006 - Volume 16, Issue 01  


Paper

Intuitionistic phase semantics is almost classical

MAX I. KANOVICH a1, MITSUHIRO OKADA a2 1 and KAZUSHIGE TERUI a3 2
a1 Department of Computer Science, Queen Mary, University of London, Mile End Road, London E1 4NS and Department of Computer and Information Science, University of Pennsylvania Email: mik@dcs.qmul.ac.uk and maxkanov@cis.upenn.edu
a2 Department of Philosophy, Faculty of Letters, Keio University, 2-15-45 Mita, Minato-ku, Tokyo 108-8345, Japan Email: mitsu@abelard.flet.keio.ac.jp
a3 National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan Email: terui@nii.ac.jp

Article author query
kanovich mi   [Google Scholar] 
okada m   [Google Scholar] 
terui k   [Google Scholar] 
 

Abstract

We study the relationship between classical phase semantics for classical linear logic (LL) and intuitionistic phase semantics for intuitionistic linear logic (ILL). We prove that (i) every intuitionistic phase space is a subspace of a classical phase space, and (ii) every intuitionistic phase space is phase isomorphic to an ‘almost classical’ phase space. Here, by an ‘almost classical’ phase space we mean an intuitionistic phase space having a double-negation-like closure operator. Based on these semantic considerations, we give a syntactic embedding of propositional ILL into LL.

(Received August 31 2004)
(Revised October 24 2005)


Footnotes

1 Partly supported by the Grants-in-Aid for Scientific Research (MEXT), 21st Century Centre (CIRM) for Excellence on Humanity Sciences in Keio University (MEXT), and Oogata-Kenkyuu-Jyosei Grant (Keio University).

2 Partly supported by the Grants-in-Aid for Scientific Research (MEXT).


--