The logic seminar takes place on alternate Fridays between 10:15 and 12:00 at Olof Wijksgatan 6 in room T307.
27th January: Paul Gorbow (FLoV, Gothenburg)
Abstract: NFU is a set theory (with atoms) which allows unbounded comprehension in a restricted form. In particular, there is a universal set V, and each natural number n is implemented as the set of all sets with n elements. It can be axiomatized as stratified comprehension extensionality infinity. Any model of ZF that admits a non-trivial automorphism, may be turned into a model of NFU, by a simple reinterpretation of membership. NF is the strengthening of NFU, which does not allow for atoms. INF(U) is intuitionistic NF(U).
In this presentation, I give theories in the language of categories equiconsistent to each of (I)NF(U). The idea is to start from the axioms of a Heyting/Boolean category, which mirror a large chunk of the finite axiomatization of (I)NF(U). We add to this a predicate distinguishing the type-level morphisms, characterized by certain axioms, e.g. expressing that the type-level morphisms form a subcategory. This allows us to add a form of the axiom of power objects (familiar from topos theory) that is restricted to the type-level morphisms. The relationship between the subcategory of type-level morphisms and the full category, corresponds to the relationship between (I)NF(U) and its class theory (I)ML(U). As a corollary to the equiconsistency result, we obtain a simple proof of Con(NF) iff Con(NFU |V| = |P(V)|). Moreover, the subcategory of type-level morphisms has a natural subcategory of so called strongly Cantorian objects, which is a topos.
10 February: no seminar
24 February: Erik Palmgren (Stockholm)
Abstract: In this talk we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this interpretation some useful special cases of Russell’s reducibility axiom are valid. This is enough to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory IRTT suitable for this purpose. IRTT allows for all the basic set-theoretic constructions.
10 March: Valentin Goranko (Stockholm)
Abstract: In this talk I will first introduce multi-agent concurrent game models and the Alternating-time temporal logic ATL as the currently most popular logical system for formalizing reasoning about strategic abilities in multi-agent systems. Then, I will present the compositional semantics of ATL, will illustrate it with some examples and will discuss briefly the main logical decision problems for ATL. Next, I will present a recently developed game-theoretic semantics for ATL and will compare several versions of it: unbounded, ordinal-bounded and finitely bounded. The first two versions will be shown to be equivalent to the compositional semantics, whereas the last one is not. I will end with some open questions and brief concluding remarks.
24 March: Michael Rathjen (Leeds, UK)
Abstract: Brouwer argued that limitation to constructive reasoning is required when dealing with "unfinished" totalities. As a complement to that, the predicativists such as Poincaré and Weyl (of Das Kontinuum) accepted the natural numbers as a "finished" or definite totality, but nothing beyond that. In addition, the "semi-intuitionistic" school of descriptive set theory (DST) of Borel et al. in the 1920s took both the natural numbers and the real numbers as definite totalities and explored what could be obtained on that basis alone.
From a metamathematical point of view, these and other different levels of indefiniteness/definiteness can be treated in the single framework of semi-intuitionistic theories of sets, whose basic logic is intuitionistic, but for which the law of excluded middle is accepted for bounded formulas.
7 April: PhD defense of Martin Kaså
21 April: Fredrik Engström (FLoV, Gothenburg)
Abstract: In this talk I will introduce a variant of Dependence logic which is based on team semantics suitable for handling generalized quantifiers. Dependence logic, proposed by Väänänen is an elegant way of introducing dependencies between variables into the object language. The framework of Dependence logic, so-called team semantics, has turned out to be very flexible and allows for interesting generalizations. Instead of considering satisfaction with respect to a single assignment s, team semantics considers sets of assignments X, called teams. While the semantics of Dependence logic is based on the principle that a formula \phi is satisfied by a team X if every assignment s \in X satisfies \phi, we will replace this principle by the following: a formula \phi is satisfied by a team X if for every assignment s: s \in X iff s satisfies \phi replacing an implication by an equivalence. When only first-order logic is considered nothing exciting happens, it is only when we introduce new logical operations that things start to get more exciting.
5 May: no seminar
19 May: no seminar (Department conference)
2 June: PhD defense of Rasmus Blanck
There is a mailing list used for spreading information about the logic seminar. Please use the above link to subscribe to it.