Dialectica spaces are a categorical way of constructing models of

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. Although the logic has also be ...

. They were introduced by

Valeria de Paiva Valeria Correa Vaz de Paiva is a Brazilian mathematician, logician, and computer scientist. Her work includes research on logical approaches to computation, especially using category theory, knowledge representation and natural language semanti ...

Martin Hyland (John) Martin Elliott Hyland is professor of mathematical logic at the University of Cambridge and a fellow of King's College, Cambridge. His interests include mathematical logic, category theory, and theoretical computer science. Education H ...

's student, in her doctoral thesis, as a way of modeling both linear logic and Gödel's

Dialectica interpretation In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to pr ...

—hence the name. Given a

category Category, plural categories, may refer to: Philosophy and general uses * Categorization, categories in cognitive science, information science and generally *Category of being * ''Categories'' (Aristotle) *Category (Kant) *Categories (Peirce) * ...

''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 In mathematics, particularly in category theory, a morphism is a structure-preserving map from one mathematical structure to another one of the same type. The notion of morphism recurs in much of contemporary mathematics. In set theory, morphisms a ...

into ''K''. Morphisms of Dialectica spaces are similar to

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 (of points in open sets ...

morphisms, but instead of an equality condition, they have an

inequality Inequality may refer to: Economics * Attention inequality, unequal distribution of attention across users, groups of people, issues in etc. in attention economy * Economic inequality, difference in economic well-being between population groups * ...

condition, which is read as a

logical implication Logical consequence (also entailment) is a fundamental concept in logic, which describes the relationship between statements that hold true when one statement logically ''follows from'' one or more statements. A valid logical argument is one ...

: the first object implies the second.

References

* K. Gödel. "Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes - Dialectica", 1958. (Translation and analysis in ''Collected Works'', Vol II, Publications, 1937-1974—eds S. Feferman et al., 1990). * V. de Paiva. "The Dialectica Categories". In Proc. of Categories in Computer Science and Logic, Boulder, CO, 1987. Contemporary Mathematics, vol 92, American Mathematical Society, 1989 (eds. J. Gray and A. Scedrov) * V. de Paiva. "A dialectica-like model of linear logic". In ''Proc. Conf. on Category Theory and Computer Science, Springer-Verlag Lecture Notes in Computer Science'' 389, pp. 341–356, Manchester, September 1989. Category theory Logic {{Logic-stub