On the Semantics of Classical Disjunction

Research output: Contribution to journalArticle

Standard

On the Semantics of Classical Disjunction. / Ritter, Eike; Pym, D.

In: Journal of Pure and Applied Algebra, Vol. 159, No. 2-3, 24.05.2001, p. 315-338.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Ritter, Eike ; Pym, D. / On the Semantics of Classical Disjunction. In: Journal of Pure and Applied Algebra. 2001 ; Vol. 159, No. 2-3. pp. 315-338.

Bibtex

@article{a52029dfb5094808a831d4dfb6b1098e,
title = "On the Semantics of Classical Disjunction",
abstract = "The lambda mu -calculus provides a system of realizers for classical free (cf. natural) deduction in the absence of disjunction. We identify two forms of disjunction, one derived from Gentzen's sequent calculus LJ and one from LK, and develop the corresponding metatheory for lambda mu extended with disjunction. We describe a class of categorical models for the lambda mu -calculus with each of these disjunctions. Considering the calculus with LK-derived disjunction, lambda mu, we establish the standard metatheoretic properties and show that a class of continuations models of lambda mu can be elegantly extended to lambda mu nu. Comparing the two forms of disjunction, we show that any model which identifies them collapses to a trivial family of Boolean algebras. (C) 2001 Elsevier Science B.V. All rights reserved.",
author = "Eike Ritter and D Pym",
year = "2001",
month = may,
day = "24",
doi = "10.1016/S0022-4049(00)00161-4",
language = "English",
volume = "159",
pages = "315--338",
journal = "Journal of Pure and Applied Algebra",
issn = "0022-4049",
publisher = "Elsevier",
number = "2-3",

}

RIS

TY - JOUR

T1 - On the Semantics of Classical Disjunction

AU - Ritter, Eike

AU - Pym, D

PY - 2001/5/24

Y1 - 2001/5/24

N2 - The lambda mu -calculus provides a system of realizers for classical free (cf. natural) deduction in the absence of disjunction. We identify two forms of disjunction, one derived from Gentzen's sequent calculus LJ and one from LK, and develop the corresponding metatheory for lambda mu extended with disjunction. We describe a class of categorical models for the lambda mu -calculus with each of these disjunctions. Considering the calculus with LK-derived disjunction, lambda mu, we establish the standard metatheoretic properties and show that a class of continuations models of lambda mu can be elegantly extended to lambda mu nu. Comparing the two forms of disjunction, we show that any model which identifies them collapses to a trivial family of Boolean algebras. (C) 2001 Elsevier Science B.V. All rights reserved.

AB - The lambda mu -calculus provides a system of realizers for classical free (cf. natural) deduction in the absence of disjunction. We identify two forms of disjunction, one derived from Gentzen's sequent calculus LJ and one from LK, and develop the corresponding metatheory for lambda mu extended with disjunction. We describe a class of categorical models for the lambda mu -calculus with each of these disjunctions. Considering the calculus with LK-derived disjunction, lambda mu, we establish the standard metatheoretic properties and show that a class of continuations models of lambda mu can be elegantly extended to lambda mu nu. Comparing the two forms of disjunction, we show that any model which identifies them collapses to a trivial family of Boolean algebras. (C) 2001 Elsevier Science B.V. All rights reserved.

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

U2 - 10.1016/S0022-4049(00)00161-4

DO - 10.1016/S0022-4049(00)00161-4

M3 - Article

VL - 159

SP - 315

EP - 338

JO - Journal of Pure and Applied Algebra

JF - Journal of Pure and Applied Algebra

SN - 0022-4049

IS - 2-3

ER -