ML p(r)ior | On the Semantics of Intensionality

On the Semantics of Intensionality

2016-02-03
1602.01365 | cs.LO
In this paper we propose a categorical theory of intensionality. We first revisit the notion of intensionality, and discuss we its relevance to logic and computer science. It turns out that 1-category theory is not the most appropriate vehicle for studying the interplay of extension and intension. We are thus led to consider the P-categories of \v{C}ubri\'{c}, Dybjer and Scott, which are categories only up to a partial equivalence relation (PER). In this setting, we introduce a new P-categorical construct, that of exposures. Exposures are very nearly functors, except that they do not preserve the PERs of the P-category. Inspired by the categorical semantics of modal logic, we begin to develop their theory. Our leading examples demonstrate that an exposure is an abstraction of well-behaved intensional devices, such as G\"odel numberings. The outcome is a unifying framework in which classic results of Kleene, G\"odel, Tarski and Rice find concise, clear formulations, and where each logical device or assumption involved in their proofs can be expressed in the same algebraic manner.
PDF

Highlights - Most important sentences from the article

Login to like/save this paper, take notes and configure your recommendations

Related Articles

2019-04-27

We introduce a new form of logical relation which, in the spirit of metric relations, allows us to a… show more
PDF

Highlights - Most important sentences from the article

2019-05-01

Computational philosophy is the use of mechanized computational techniques to unearth philosophical … show more
PDF

Highlights - Most important sentences from the article

2019-04-01

We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can… show more
PDF

Highlights - Most important sentences from the article

2018-10-19
1810.08380 | cs.LO

We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the… show more
PDF

Highlights - Most important sentences from the article

2019-04-22
1904.09810 | math.LO

We develop the Scott model of the programming language PCF in constructive predicative univalent typ… show more
PDF

Highlights - Most important sentences from the article

2019-05-10
1905.04058 | math.LO

Nets are generalisations of sequences involving possibly uncountable index sets; this notion was int… show more
PDF

Highlights - Most important sentences from the article

2019-01-23
1901.07820 | cs.LO

This paper describes how to use Lee, Jones and Ben Amram's size-change principle to check correctnes… show more
PDF

Highlights - Most important sentences from the article

2018-05-09

We present a device for specifying and reasoning about syntax for datatypes, programming languages, … show more
PDF

Highlights - Most important sentences from the article

2018-05-22

Reversible computing models settings in which all processes can be reversed. Applications include lo… show more
PDF

Highlights - Most important sentences from the article

2017-12-13
1712.04864 | cs.LO

The homotopical approach to intensional type theory views proofs of equality as paths. We explore wh… show more
PDF

Highlights - Most important sentences from the article

2018-02-15
1802.05629 | cs.LO

This paper introduces a new family of models of intensional Martin-L\"of type theory. We use constru… show more
PDF

Highlights - Most important sentences from the article

2018-04-09

This paper investigates modal type theories by using a new categorical semantics called change-of-ba… show more
PDF

Highlights - Most important sentences from the article

2019-04-02
1904.01679 | math.CT

The humble $\dagger$ ("dagger") is used to denote two different operations in category theory: Takin… show more
PDF

Highlights - Most important sentences from the article

2018-10-31

In type theory, coinductive types are used to represent processes, and are thus crucial for the form… show more
PDF

Highlights - Most important sentences from the article

2016-02-15
1602.04860 | cs.LO

We show how to derive natural deduction systems and modal lambda calculi for constructive versions o… show more
PDF

Highlights - Most important sentences from the article

2015-07-19
1507.05305 | cs.CC

We examine various categorical structures that can and cannot be constructed. We show that total com… show more
PDF

Highlights - Most important sentences from the article

2018-01-31
1802.00061 | cs.PL

We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define t… show more