Dialectica space
Encyclopedia
Dialectica spaces are a categorical
way of constructing models of linear logic
.
They were introduced by Valeria de Paiva, Martin Hyland
's student, in her doctoral thesis, as a way of modeling both linear logic and Gödel
's dialectica interpretation
—hence the name.
Given a category C and a specific object K of C with certain (logical) properties, one can construct the category of Dialectica spaces over C, whose objects are pairs of objects of C, related by a C-morphism
into the given object. Morphisms of Dialectica spaces are similar to Chu space
morphisms, but instead of an equality condition, they have an inequality condition, which is read as a logical implication, the first object implies the second.
Category theory
Category theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
way of constructing models of linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
.
They were introduced by Valeria de Paiva, Martin Hyland
Martin Hyland
John Martin Elliott Hyland is professor of mathematics at King's College in the University of Cambridge, England where he is currently head of the Department of Pure Mathematics and Mathematical Statistics...
's student, in her doctoral thesis, as a way of modeling both linear logic and Gödel
Godel
Godel or similar can mean:*Kurt Gödel , an Austrian logician, mathematician and philosopher*Gödel...
's dialectica interpretation
Dialectica interpretation
In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic...
—hence the name.
Given a category C and a specific object K of C with certain (logical) properties, one can construct the category of Dialectica spaces over C, whose objects are pairs of objects of C, related by a C-morphism
Morphism
In mathematics, a morphism is an abstraction derived from structure-preserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
into the given object. Morphisms of Dialectica spaces are similar to Chu space
Chu space
Chu spaces generalize the notion of topological space by dropping the requirements that the set of open sets be closed under union and finite intersection, that the open sets be extensional, and that the membership predicate be two-valued...
morphisms, but instead of an equality condition, they have an inequality condition, which is read as a logical implication, the first object implies the second.