### 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.

Original language | English |
---|---|

Pages (from-to) | 67-86 |

Number of pages | 20 |

Journal | Mathematical Structures in Computer Science |

Volume | 16 |

Issue number | 1 |

DOIs | |

Publication status | Published - 2006 Feb |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science Applications
- Mathematics (miscellaneous)

### Cite this

*Mathematical Structures in Computer Science*,

*16*(1), 67-86. https://doi.org/10.1017/S0960129505005062

**Intuitionistic phase semantics is almost classical.** / Kanovich, Max I.; Okada, Mitsuhiro; Terui, Kazushige.

Research output: Contribution to journal › Article

*Mathematical Structures in Computer Science*, vol. 16, no. 1, pp. 67-86. https://doi.org/10.1017/S0960129505005062

}

TY - JOUR

T1 - Intuitionistic phase semantics is almost classical

AU - Kanovich, Max I.

AU - Okada, Mitsuhiro

AU - Terui, Kazushige

PY - 2006/2

Y1 - 2006/2

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33750692687&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33750692687&partnerID=8YFLogxK

U2 - 10.1017/S0960129505005062

DO - 10.1017/S0960129505005062

M3 - Article

AN - SCOPUS:33750692687

VL - 16

SP - 67

EP - 86

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 1

ER -