Logic Seminar

---

Alexandru Muresan (Faculty of Mathematics and Computer Science, University of Bucharest)
A proposal of a unified theory for the foundations of mathematics
Abstract: We present a unified calculus for logic and set theory within the framework of hilbertian finitism.

Andrei Sipos (Faculty of Mathematics and Computer Science, University of Bucharest)
First steps into non-standard analysis III

Andrei Sipos (Faculty of Mathematics and Computer Science, University of Bucharest)
First steps into non-standard analysis II

Andrei Sipos (Faculty of Mathematics and Computer Science, University of Bucharest)
First steps into non-standard analysis
Abstract: We develop the theory of the hyperreal number system, following the exposition in Goldblatt's book, which will be occasionally supplemented with additional insights.

Andrei Sipos (Faculty of Mathematics and Computer Science, University of Bucharest)
An invitation to ultraproducts II

Andrei Sipos (Faculty of Mathematics and Computer Science, University of Bucharest)
An invitation to ultraproducts I
Abstract: We present an exposition of the basic theory of ultrafilters needed to motivate and define ultraproducts, followed by an excursion into generalizations and applications of the latter concept.

Daniel Ivan (IMAR)
Logical metatheorems for metric spaces II
Abstract: We will continue with the proof of the logical metatheorem started the previous week.

Daniel Ivan (IMAR)
Logical metatheorems for metric spaces I
Abstract

Razvan Diaconescu (IMAR)
1. Institution theory: introduction and 2. Institution theory: internal logic
Abstract: Institution theory is a major model theoretic trend of universal logic that formalizes within category theory the intuitive notion of a logical system, including syntax, semantics, and the satisfaction relation between them. It arose within computing science, especially specification theory [1], as a response to the population explosion of logics there and where it has become the most important foundational theory Later on institution theory has been succesfully used in pure logic studies in the spirit of universal logic.
This means the development of model and proof theory in the very abstract setting of arbitrary institutions, free of commitement to a particular logical system [2]. In this way we gain freedom to live without concrete models, sentences satisfaction, and so on, we gain another level of abstraction and generality and a deeper understanding of model theoretic phenomena not hindered by the largely irrelevant details of a particular logical system, but guided by structurally clean causality.
The latter aspect is based upon the fact that concepts come naturally as presumed features that a ``logic'' might exhibit or not and are defined at the most appropriate level of abstraction; hypotheses are kept as general as possible and introduced on a by-need basis, and thus results and proofs are modular and easy to track down regardless of their depth.
The continuous interplay between the specific and the general in institution theory brings a large array of new results for particular non-conventional, unifies several known results, produces new results in well-studied conventional areas, reveals previously unknown causality relations, and dismantles some which are usually assumed as natural. Access to highly non-trivial results is also considerably facilitated. The dynamic role played by institution theory within the wider universal logic project is illustrated by the fact that institution theory papers have come second and first, respectively, in the contests of the Montreux (2005) and Xi'and (2007) UNILOG, respectively.

In this tutorial we will start with a brief explanation of the historical and philosophical origins of institution theory, followed by a presentation of its basic mathematical concepts. We will also have a trip through the rather rich body of methods and results of the institution theoretic approach to logic and model theory.

Although institution theory is primarily a model theoretic approach we will also discuss recent proof theoretic developments in the area. However our real emphasis will be not on the actual mathematical developments but on the non-substantialist way of thinking and the top-down methodologies promoted by institution theory, that contrast sharply the substantialist view and the bottom-up methodologies that pervade and underly conventional logic, this being the most profound message of institution theory as a universal logic trend.

References:
[1] J. Goguen, R. Burstall, Institutions: Abstract Model Theory for Specification and Programming, J.ACM 39(1) 95-146, 1992.
[2] R. Diaconescu, Institution-independent Model Theory, Birkhauser, 2008.

Dan Hernest (IMAR)
The use of modal operators for more efficient functional synthesis I
Abstract: We present Prawitz Natural Deduction of classical, intuitionistic and minimal first-order logics

Laurentiu Leustean (IMAR)
An application of proof mining to nonlinear iterations IV

Laurentiu Leustean (IMAR)
An application of proof mining to nonlinear iterations III

Laurentiu Leustean (IMAR)
An application of proof mining to nonlinear iterations II

Laurentiu Leustean (IMAR)
An application of proof mining to nonlinear iterations
Abstract: This talk reports on results obtained in arXiv:1211.2991v2 [math.LO]. We present an application of proof mining to the asymptotic behaviour of the Ishikawa iteration associated to nonexpansive self-mappings of convex subsets of a class of uniformly convex geodesic spaces. We obtain highly uniform effective rates of asymptotic regularity for this iteration and, moreover, we show that these results are guaranteed by a combination of logical metatheorems for classical and semi-intuitionistic systems.

Daniel Ivan (IMAR)
Proof Interpretations IV
Abstract

Denisa Diaconescu (Faculty of Mathematics and Computer Science, University of Bucharest)
Omitting types theorem for a non-commutative many-valued logic
Abstract: The omitting types theorem for classical logic is one of the most important result in classical model theory. The generalization of classical model theory over many-valued logics is a new research trend. In this talk we will present a proof for an omitting types theorem for the non-commutative MTL logic.

Daniel Ivan (IMAR)
Proof Interpretations III
Abstract

Daniel Ivan (IMAR)
Proof Interpretations II
Abstract

Daniel Ivan (IMAR)
Proof Interpretations I
Abstract