Search

In the framework of pointfree topology, we discuss the role of Weil entourages in the study of structures such as uniformities, quasi-uniformities, nearnesses, quasi-nearnesses, proximities and infinitesimal relations.

The aim of this note is to prove that two uniform frames, with countable bases and the same underlying frame, are equal whenever they have the same totally bounded coreflection. As corollaries we get the localic counterparts of two well-known theorems of Efremovic (1952) for uniform spaces.

This paper deals with the algebra F(L) of real functions on a frame L and its subclasses LSC(L) and USC(L) of, respectively, lower and upper semicontinuous real functions. It is well known that F(L) is a lattice-ordered ring; this paper presents explicit formulas for its algebraic operations which allow to conclude about their behaviour in LSC(L) and USC(L).As applications, idempotent functions are characterized and previous pointfree results about strict insertion of functions are significantly improved: general pointfree formulations that correspond exactly to the classical strict insertion results of Dowker and Michael regarding, respectively, normal countably paracompact spaces and perfectly normal spaces are derived.The paper ends with a brief discussion concerning the frames in which every arbitrary real function on the α-dissolution of the frame is continuous.

Quasi-uniformities (not necessarily symmetric uniformities) are usually studied via entourages (special neighbourhoods of the diagonal in X × X ) where one can simply forget about the symmetry requirement. This has been done successfully in the point-free context as well, but there is a demand for a covering approach, a.o. because the point-free representation of the square X × X is not without difficulties. Based on the (spatial) ideas from Gantner and Steinlage (1972) [9] , a cover type quasi-uniformity was developed in Frith (1987) [6] and other papers using biframes, the point-free variant of bitopologies. In this paper we show that this can be avoided and present a cover type quasi-uniformity structure enriching that of frame directly.

\emph{Focused sequent calculi} are a refinement of sequent calculi, where additional side-conditions on the applicability of inference rules force the implementation of a proof search strategy. Focused cut-free proofs exhibit a special normal form that is used for defining identity of sequent calculi proofs. We introduce a novel focused display calculus fD.LG and a fully polarized algebraic semantics FP.LG for Lambek-Grishin logic by generalizing the theory of \emph{multi-type calculi} and their algebraic semantics with \emph{heterogenous consequence relations}. The calculus fD.LG has \emph{strong focalization} and it is \emph{sound and complete} w.r.t. FP.LG. This completeness result is in a sense stronger than completeness with respect to standard polarized algebraic semantics (see e.g. the phase semantics of Bastenhof for Lambek-Grishin logic or Hamano and Takemura for linear logic), insofar we do not need to quotient over proofs with consecutive applications of shifts over the same formula. We plan to investigate the connections, if any, between this completeness result and the notion of \emph{full completeness} introduced by Abramsky et al. We also show a number of additional results. fD.LG is sound and complete w.r.t. LG-algebras: this amounts to a semantic proof of the so-called \emph{completeness of focusing}, given that the standard (display) sequent calculus for Lambek-Grishin logic is complete w.r.t. LG-algebras. fD.LG and the focused calculus f.LG of Moortgat and Moot are equivalent with respect to proofs, indeed there is an effective translation from f.LG-derivations to fD.LG-derivations and vice versa: this provides the link with operational semantics, given that every f.LG-derivation is in a Curry-Howard correspondence with a directional $\overline\lambda\mu\widetilde{\mu}$-term.