This paper considers a topos-theoretic structure for the interpretation of co-constructive logic for proofs and refutations following Trafford :22–40, 2015). It is notoriously tricky to define a proof-theoretic semantics for logics that adequately represent constructivity over proofs and refutations. By developing abstractions of elementary topoi, we consider an elementary topos as structure for proofs, and complement topos as structure for refutation. In doing so, it is possible to consider a dialogue structure between these topoi, and also control their relation such (...) that classical logic is simulated where proofs and refutations are conclusive. (shrink)

In this paper we introduce a novel way of building arithmetics whose background logic is R. The purpose of doing this is to point in the direction of a novel family of systems that could be candidates for being the infamous R#1/2 that Meyer suggested we look for.

We give an introduction to Turing categories, which are a convenient setting for the categorical study of abstract notions of computability. The concept of a Turing category first appeared in the work of Longo and Moggi; later, Di Paolo and Heller introduced the closely related recursion categories. One of the purposes of Turing categories is that they may be used to develop categorical formulations of recursion theory, but they also include other notions of computation, such as models of combinatory logic (...) and of the lambda calculus. In this paper our aim is to give an introduction to the basic structural theory, while at the same time illustrating how the notion is a meeting point for various other areas of logic and computation. We also provide a detailed exposition of the connection between Turing categories and partial combinatory algebras and show the sense in which the study of Turing categories is equivalent to the study of PCAs. (shrink)

This article puts forward the notion of “evolving diagram” as an important case of mathematical diagram. An evolving diagram combines, through a dynamic graphical enrichment, the representation of an object and the representation of a piece of reasoning based on the representation of that object. Evolving diagrams can be illustrated in particular with category-theoretic diagrams (hereafter “diagrams*”) in the context of “sketch theory,” a branch of modern category theory. It is argued that sketch theory provides a diagrammatic* theory of diagrams*, (...) that it helps to overcome the rivalry between set theory and category theory as a general semantical framework, and that it suggests a more flexible understanding of the opposition between formal proofs and diagrammatic reasoning. Thus, the aim of the paper is twofold. First, it claims that diagrams* provide a clear example of evolving diagrams, and shed light on them as a general phenomenon. Second, in return, it uses sketches, understood as evolving diagrams, to show how diagrams* in general should be re-evaluated positively. (shrink)

This paper introduces a natural deduction calculus for intuitionistic logic of belief \ which is easily turned into a modal \-calculus giving a computational semantics for deductions in \. By using that interpretation, it is also proved that \ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \ showing the general structure of such a modality for belief in an intuitionistic framework.

Kosta Došen argued in his papers Inferential Semantics (in Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 147–162. Springer, Berlin 2015) and On the Paths of Categories (in Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics, pp. 65–77. Springer, Cham 2016) that the propositions-as-types paradigm is less suited for general proof theory because—unlike proof theory based on category theory—it emphasizes categorical proofs over hypothetical inferences. One specific instance of this, Došen points out, is that the Curry–Howard isomorphism (...) makes the associativity of deduction composition invisible. We will show that this is not necessarily the case. (shrink)

In this paper I compare two well studied approaches to topological semantics – the domain-theoretic approach, exemplified by the category of countably based equilogical spaces, Equ and Typ Two Effectivity, exemplified by the category of Baire space representations, Rep . These two categories are both locally cartesian closed extensions of countably based T0-spaces. A natural question to ask is how they are related.First, we show that Rep is equivalent to a full coreflective subcategory of Equ, consisting of the so-called 0-equilogical (...) spaces. This establishes a pair of adjoint functors between Rep and Equ. The inclusion Rep → Equ and its coreflection have many desirable properties, but they do not preserve exponentials in general. This means that the cartesian closed structures of Rep and Equ are essentially different. How ever, in a second comparison we show that Rep and Equ do share a common cartesian closed subcategory that contains all countably based-T0 spaces. Therefore, the domain-theoretic approach and TTE yield equivalent topological semantics of computation for all higher-order types over countably based T0-spaces. We consider several examples involving the natural numbers and the real numbers to demonstrate how these comparisons make it possible to transfer results from one setting to another. (shrink)