Mathematical Logic in Padua

Events

1WFTop 1997 - Abstracts

Giovanni Sambin: "The Paulus Venetus Program"

Some general consideration on the philosophy underlying recent research work in Padova, mainly Basic Logic and Basic Picture.

Kosta Dosen: "Logical constants and adjunction"

I would address matters close to your ideas about basic logic

Ferruccio Guidi: "The Third Gödel-Kreisel Theorem"

The Third Gödel-Kreisel Theorem states that strong completeness for the negative fragment of intuitionistic logic with respect to naive semantic, implies the validity of Markov's proof (involving Friedman-Dragalin translation, closure of Heyting arithmetic under Markov's rule and the soundness theorem) is presented.

Maria Emilia Maietti: "Quotiens in type theory"

We consider to extend Martin-Löf's Constructive Set Theory with effective quotient sets, since the type theory of categorical universes, like topoi, supports a particular kind of them. Effectiveness turns out to be problematic, because under certain conditions we lose constructivity.

Silvia Gebellato: "The Essence of Continuity"

Basic pairs are the main tool of a new conception of topology, where the formal side is included in the picture. This is particularly clear when defining morphisms between basic pairs, that is pairs of relations giving rise to a commutative square. Usual continuous functions, also between formal spaces, are particular cases. We also prove (impredicatively) that any function between formal spaces respecting the inclusion of formal points is actually induced by a continuous relation between the corrsponding formal topologies. We hope to be able to give a predicative presentation of the Vietoris topology.

Silvio Valentini: "The generalized cover: motivations, first results and open problems"

After the introduction of formal topologies, which are a constructive, i.e. intuitioniscic and predicative, approach to topology, fully developed inside Martin-Löf's Type Theory, the problem to deal whith closed subsets remained open for a long time. In fact, while it was immediately obviuos that the strightforward identification of closed subsets with the complements of the open sets cannot work in an intuitionistic framework, it was only the recent introduction of the notion of basic pair by Sambin and Gebellato which allowed to achieve the result to deal with closed subsets in a formal way, and hence within intuitionistic type theory.

The problem which was not solved in the Sambin-Gebellato approach was that some conditions, which are naturally valid in any basic pair, could not be proved.
In my talk I want to recall all the main definitions of the basic pairs and then to show that a natural generalization of the notion of cover relation is all what is needed in order to be able to give them a very natural explanation in term of topology induced on a closed subset. After these definitions I will show that most of the known results for formal topologies can easily be adapted to this new framework.

Giovanni Curi: "Formal spaces with weight and distance: a framework for constructive analysis within intuitionistic type theory"

We present a framework for developing analysis within intuitionistic type theory: a formal topology A can be endowed with a weight and a distance (respecting the axioms that hold for a diameter and a distance of any metric space) and with a predicate D to give a structure (A,|-|, d(-,-), D). Building up the usual completion of the formal topology, weight and distance can be canonically extended to give two maps, still a weight and a distance, defined on the space of formal points.

The definition of maximal approximation is then given and proved to be a generalization of the one introduced by Martin-Löf. The collection of maximal approximations forms a metric space; the predicate D then allows to define the concept of morphisms of topologies with weight and distance, thus obtaining also continuous functions in a predicative way. Some elementary analysis is then developed. Some specific interesting results are derived: simple presentations of spaces which are in general introduced by means of covers defined by infinitary axioms are now possible (e.g. the real numbers).

Kosta Dosen: "Cut-elimination in adjunction"

"I will present some, more recent, related results"

Giulia Battilotti: "Embeddings into basic logic: a solution in a particular case and some proposal"

We give an embedding of classical logic into basic orthologic, obtained by adopting a modality which is defined on primitive literals and which is extended by definition to all formulae. It allows the coexistence of classical logic and basic orthologic in the same system. The same technique is hopefully useful to face the problem of the control of context in general and hence to obtain translations also for other logics.

Claudia Faggian: "Basic logic: a unifying approach to normalization"

All traditional logics (classical, linear, intuitionistic and its dual) can be obtained from basic logic by the addition of structural rules. Basic logic is the fixed common core containing the operational rules. The whole system (that is, the operational rules and all the structural rules) corresponds to classical logic. The main result is that the cut-elimination procedure for the whole system respects all the underlying logics.
This amounts to have a single unique normalization procedure that is at the same time a normalization procedure for each of the (eight) logics considered in the framework.

Nicola Granà: "Proof search in Basic Logic. From Basic Logic to its extensions by selection"

• Bounding the number of formulae which appear in a sequent make silmpler the proof search.
• We can extend the basic sequent calculus in a modular way to represent eight logics (such as the classical one). The basic idea is to formalize the selection of formulae to be connected by any operational rule.

Sara Sadocco: "Una deduzione naturale per l'Intersection Type Inference"

Nel seguente lavoro viene presentato un sistema di deduzione naturale per la logica introdotta da Betti Venneri in Intersection Type as Logical Formulae, J. Logic Computat, Vol. 4 No. 2, pp. 109-124 1994. Questo sistema di deduzione naturale riesce a simulare il parallellismo e la sincronizzazione di processi. Noi dimostreremo che esiste un metodo effettivo per associare deduzioni nel sistema di Intersection Type Inference a prove nella nuova deduzione naturale, che chiameremo Deduzione Naturale Parallela (PND, Parallel Natural Deduction), mostrando in tal modo la completezza e la correttezza del nostro calcolo rispetto alla Intersection Type Inference.

Michele Bugliesi: "Extensible Objects are Recursive Records of Polymorphic Functions"

We present an interpretation of a calculus of extensible objects in terms of well-understood purely functional concepts. Specifically, we give a (sub)type preserving translation of an object calculus that supports method invocation, functional method override, and extension into a polymorphic lambda-calculus with recursive types and (higher-order) subtyping. The translation clarifies the nature of extensible objects by characterizing them as recursive records that incorporate the basic functionalities of classes and class instances in class-based object-oriented models. It also clarifies the relationship between the calculi of extensible and non-extensible objects presented in the recent literature.

Damiano Macedonio: "A semantics for BS (Structured Basic Logic)"

Given an arbitrary basic formal topology S, we define the valutation of a formula as a pair of subset of S: an open formal subset and a closed formal one. The basic idea is that fomal opens act as generalized tuth values and formal values of form.