[Two kestrels flying]

Home : Research Staff : Dusko Pavlovic : Math and Logic papers
 

Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel

Math and Logic

1991

Categorical Interpolation: Descent and the Beck-Chevalley Condition without Direct Images

Abstract
Fibred categories have been introduced by Grothendieck (1959, 1970) as the setting for his theory of descent. The present paper contains (in section 4) a characterisation of the effective descent morphisms under an arbitrary fibred category. This essentially geometric result complements a logical analysis of the Beck-Chevalley property (presented in section 1). This property was crucial in the well-known theorem on sufficient conditions for the descent under bifibrations, due to Benabou and Roubaud (1970) and Beck (unpublished). We describe the notion of interpolant as the common denominator of the concepts of descent and the Beck-Chevalley property.

1992

On the structure of paradoxes

Abstract
Paradox is a logical phenomenon. Usually, it is produced in type theory, over a type of "truth values". A formula p, as a term p:Prop is constructed, such that p is equivalent to its negation - whereupon everything can be proved. We describe a general pattern which many constructions of the formula follow: for example, the well known arguments of Cantor, Russell, and Goedel. We generalize their common underlying structure, and prove that Reynolds' construction of the type isomorphic to its second power type, contrary to his conjecture, cannot be extended to give a fixed point of every variable type derived from exponentiation. In particular, for contravariant types, such a fixed point would lead to a paradox.

1995

A categorical setting for the 4-Colour Theorem

Abstract
The 4-Colour Theorem has been proved in the late seventies , after more than a century of fruitless efforts. But the proof has provided very little new information about the map colouring itself. While trying to understand this phenomenon, we analyze colouring in terms of universal properties and adjoint functors.

It is well known that the 4-colouring of maps is equivalent to the 3-colouring of the edges of some graphs. We show that every slice of the category of 3-coloured graphs is a topos. The forgetful functor to the category of graphs is cotripleable; every loop-free graph is covered by a 3-coloured one in a universal way. In this context, the 4-Color Theorem becomes a statement about the existence of coalgebra structure on graphs.

In a sense, this approach seems complementary to the known combinatorial colouring procedures.

On completeness and cocompleteness in and around small categories

Abstract
The simple connection of completeness and cocompleteness of lattices grows in categories into the Adjoint Functor Theorem. The connection of completeness and cocompleteness of Boolean algebras - even simpler - is similarly related to Pare's Theorem for toposes. We explain these relations and then study the fibrational versionso of both theorems, for small complete categories. They can be interpreted as definability results in logic with proofs-as-constructions, and transferred into type theory.

Maps I: relative to a factorisation system

Abstract
Originally, categorical calculus of relations was developed using the canonical factorisations in regular categories. More recently, relations restricted to a proper factorisation systems have been studied by several authors. In the present paper, we consider the general situation, where relations are induced by an arbitrary stable factorisation. This extension of the calculus of relations is necessary for categorical development of strongly constructivist logic, and of semantics of computation, where non-monic relations come about naturally.

In this setting we analyze the correspondence of maps, i.e. the total, single-valued relations, and functions, as given by the arrows of the underlying category.

1996

Maps II: chasing diagrams in categorical proof theory

Abstract
In categorical proof theory, propositions and proofs are presented as objects and arrows in a category. It thus embodies the strong constructivist paradigms of propositions-as-types and proofs-as-constructions, which lie in the foundation of computational logic. Moreover, in the categorical setting, a third paradigm arises, not available elsewhere: logical-operations-as-adjunctions. It offers an answer to the notorious question of the equality of proofs. Diagram chasing comes about in algebra of proofs.

On the basis of these ideas, the present paper investigates proof theory of regular logic: the {\and,\exists}-fragment of the first order logic with equality. The corresponding categorical structure is regular fibration. The examples include stable factorisations, sites, triposes. Regular logic is exactly what is needed to talk about maps, as total and single-valued relations. However, when enriched with proofs-as-arrows, this familiar concept must be supplied with an additional conversion rule, connecting the proof of the totality with the proof of the single-valuedness. We explain the logical meaning of this rule, and then determine precise conditions under which a regular fibration supports the principle of function comprehension (that each map corresponds to a unique function viz arrow in the base), thus lifting a basic theorem from regular categories (that Map(Rel(C) = C), which was recently relativized to factorisation systems. The obtained results open an interesting possibility of extending the P-set construction from triposes to non-posetal fibrations.

1997

Chu I: cofree equivalences, dualities and *-autonomous categories

Abstract
We study three comonads derived from the comma construction. The induced coalgebras correspond to the three concepts displayed in the title of the paper. The comonad that yields the cofree *-autonomous categories is, in essence, the Chu construction, which has recently awaken much interest in computer science. We describe its couniversal property. It is right adjoint to the inclusion of *-autonomous categories among autonomous categories, with lax structure-preserving morphisms. Moreover, this inclusion turns out to be comonadic: *-autonomous categories are exactly the Chu-coalgebras.

 

 

- Back to Top -


- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -