- University of Gothenburg
- The Faculty of Arts
- Department of Philosophy, Linguistics and Theory of Science
- Research
- Seminars
- The Logic Seminar
- 2014-2018

To content
Read more about how we use cookies on gu.se
# 2014 - 2018

## Spring 2018 Schedule

## Schedule for 2017

### Algebraic Set Theory for NF and some of its variants

### Intuitionistic Ramified Type Theory

### Compositional vs Game-Theoretic Semantics for the Alternating-Time Temporal Logic ATL

### Indefiniteness, definiteness and semi-intuitionistic theories of sets

### Team semantics for logics with generalized quantifiers

## Fall 2017 Logic Seminar Schedule

## Schedule for 2016

## Schedule for 2015

## Schedule for 2014

**The archive of older seminars (starting 2005) is divided in two web pages. Here you will find all Logic Seminar Schedules from 2018 back to 2014. Schedules from earlier years, 2005 until 2013, you can find on this page.**

25 Jan: Informal Seminar. Room: T 340

8 Feb: **Rasmus Blanck **(FLoV). Room: T340!

**Hierarchical incompleteness and arithmetically definable fragments of arithmetic**

Abstract: There has been a recent interest in hierarchical generalisations of classic incompleteness results: at least two papers on the topic were published in 2017. In this talk, I will argue that such results are often easily obtained by replacing certain principles used in the proofs by their corresponding hierarchical versions, while the essence of the arguments remain the same. After introducing about a dozen of these (quite familiar) principles, I use them to prove a handful of hierarchical incompleteness results effectively subsuming those of the two aforementioned papers.

8 Mar: **Claes Strannegård** (Chalmers). Room: T340!

**Artificial animals and general intelligence**

Abstract: Some view logic as a tool for reasoning and reasoning as a tool for decision-making. Decision-making is in turn a part of cognition, which also contains learning as a fundamental component. In this talk I will zoom out from human cognition to animal cognition and describe a computational model for animal cognition that attempts to capture certain aspects of general intelligence. Each artificial animal in this framework has an ontology that can be understood as a set of formulas of temporal logic. This ontology evolves over time and its elements (i.e. concepts) can be activated by stimuli from the environment and form the basis of perception and decision-making.

22 Mar: **Mattias Olsson** (FLoV). Room T340!

**A Model-Theoretic Proof of Gödel's Theorem: Kripke's Notion of Fulfilment**

Abstract: We present the concept of a formula being fulfilled by a sequence of numbers, which is an approximation of the formula being true. This notion is subsequently formalised in IΣ_{1} and, given a consistent, recursively axiomatisable, Σ_{2}-sound extension T of PA, used to construct a sentence we will show to be independent of T. The proof of the latter is by first showing that the sentence is true in the standard model and then using the meaning of the sentence to construct a model of T where it is false. We finally (time permitting) generalise this method to show that every consistent, recursively axiomatisable, Σ_{2}-sound extension of IΣ_{1} is incomplete in a similar manner.

This talk essentially covers the contents of my master's thesis, which presents works originally by Kriple and Quinsey and earlier presented by Quinsey and Putnam.

5 Apr: **Gerhard Jäger** (Bern)

**About fixed points of monotone Σ _{1} operators in Kripke-Platek environments**

Abstract: Fixed points of monotone operators are well-studied objects in many areas of mathematical logic (and computer science). For example, the famous Knaster-Tarski theorem states that every monotone function F on a complete lattice has a least fixed point. This fixed point can be described as the intersection of all sets closed under F and, alternatively, it can be obtained by iterating F along sufficiently many ordinals. Also, in Kripke-Platek set theory (with infinity) the least fixed point of a positive arithmetic operator is Σ

This talk goes a step higher up in the logical complexity and is centered around fixed points of monotone Σ

19 Apr: **Peter Dybjer** (Chalmers)

**Tests, Domains, and Martin-Löf's Meaning Explanations**

Abstract: In his 1982 paper "Constructive Mathematics and Computer Programming" Martin-Löf not only gave a new formulation of his intuitionistic type theory but he also provided "meaning explanations" for the judgments of this theory. Martin-Löf has subsequently elaborated on these meaning explanations in a number of lectures and papers. In this talk we discuss the relevance of the informal notion of “test” as a basis for these meaning explanations. The focus is on the meaning of higher order functions, and we explain why “formal neighbourhoods” in the sense of Martin-Löf 1983 provide a possible framework for testing type-theoretic judgements. In particular we benefit from recent work by Coquand and Huber 2017 who provided an algorithm for type-checking formal neighbourhoods.

14 May: No seminar (Departmental conference)

11—13 June: **Scandinavian Logic Symposium** (website)

14 June: Thesis defence of **Paul Gorbow** (FLoV). Room T302 at 13:15.

**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

Tuesday 19 Sep: **Bartosz Wcisło** (Warsaw) NB. room T219

*Propositional constructions in compositional truth theories*

Abstract:

In our talk, we will describe a construction in propositional logic which proved very useful in the study of models of truth theories.

Many intuitive properties for the classical compositional theory of truth over Peano arithmetic called CT− fail because this theory does not enjoy the properties of disjunctive and conjunctive correctness. I.e., if M |= CT− is a model whose arithmetical part is nonstandard, we cannot typically expect that a disjunction of nonstandard length is true if and only if one of the disjuncts is true.

By a recent result of Pakhomov, compositional truth theory with the disjunctive correctness principle is in fact not conservative over Peano Arithmetic. However, in many applications we only in fact need a disjunctive correctness in a very specific circumstances, where we expect at most one disjunct to be true which is located at some standard syntactic depth of a given nonstandard disjunction. In such a case, the use of disjunctions may be replaced with another propositional construction invented by Smith (and preceded with a similar construction by Lachlan) which behaves in a controllable fashion already in CT−.

We show how this construction may be used to obtain a number of results on models of truth theories including more perspicuous proof of Lachlan’s Theorem on recursive saturation of models of CT−.

21 Sep: **Mateusz Łełyk** (Warsaw)

*Compositional Truth Theories, Bounded Induction and Reflection Principles*

Abstract:

One of the most important questions studied within the field of Axiomatic Truth Theories is to determine the arithmetical strength of various axioms for the truth predicate. In this talk we study three main types of such truth principles for the typed truth predicate: various kinds of compositionality, bounded induction and reflection principles, namely, we shall consider three basic compositional truth theories: CT-, in which the internal logic is classical, PT- and WPT-, in which the internal logic is modelled after the Strong and Weak Kleene Logic, respectively.

One of the surprising result explained in our talk is the theorem on multiple axiomatizations of CT- extended with a bounded induction (CT0): putting together the results of Cieśliński, Kotlarski, and myself we show that CT0 is deductively equivalent to extensions of CT- with various reflection principles.

Then we ask whether the above theorem is stable under weakening the compositional axioms: we investigate analogous extensions of PT- and WPT-. It turns out that adding bounded induction to PT- results in one more axiomatization of CT0, and the same is "almost true" for the Weak Kleene case. However differences between "completeness" and "closure" reflection principles become visible. We show that in general the former are much weaker then the latter.

2 Nov: **Stergios Chatzikyriakidis** (FLoV)

*Modern Type Theoretical Semantics and Reasoning with Natural Language *

Abstract:

In this talk, I will discuss the use of Modern Type Theories (MTTs), i.e. Type Theories within the tradition of Martin-Löf, to the study of Natural Language (NL) semantics. I will give a short overview of the way MTTs have been used in order to deal with a number of linguistic phenomena and I will argue that MTTs can be used as an alternative to simply type theory and Montague Semantics for NL semantics. I will then discuss the problem of Natural Language Inference (NLI), namely the task of determining of whether an NL sentence follows or not from another one. To this extent, I will argue that one way to deal with at least the NL cases where logical inference is involved, is to use MTT semantics plus proof assistant technology to reason about these semantics. I will exemplify this idea by presenting FraCoq, a system based on the Grammatical Framework (GF) to parse NL sentences and Coq to reason about the output semantics. In effect, FraCoq defines a correspondence between the abstract syntactic structures of GF and semantics in a Type Theoretical language. We show the result of evaluating against the FraCaS test suite. We will show that FraCoq achieves state of the art results (for logical approaches). I will conclude discussing future work, potential extensions of the system, proof-automation, as well as the prospect of using hybrid systems encompassing both logical and Machine/Deep Learning components.

16 Nov: **Albert Visser** (Utrecht): **2017 Lindström Lectures**

**Research Lecture:** *The Second Incompleteness Theorem in a (somewhat) General Setting* (13:15–17:00, T307)

**Public Lecture: ***De Interpretatione* (18:15–19:15, T307)

For abstracts, see here.

30 Nov: **Øystein Linnebo** (Oslo)

*Generality explained*

Abstract:

What explains a true universal generalization? This paper distinguishes two kinds of explanation. While an instance-based explanation proceeds via each instance of the generalization, a generic explanation is independent of each instance, relying instead on completely general facts about the properties or operations involved in the generalization. This distinction is illuminated by means of a truth-maker semantics, which is also used to show that instance-based explanations support classical logic, while generic explanations support only intuitionistic logic.

14 Dec: **Anton Broberg** (FLoV)

*Type-free compositional truth*

Abstract:

The theory FS (Friedman-Sheard) is an axiomatic theory of truth that is both type-free and compositional. FS barely escapes inconsistency by the hands of the famous liar sentence, but instead falls into omega-inconsistency because of another, slightly more complicated, self-referential "liar-style" sentence. This talk is about theories of truth that in some way or another are related to FS.

Mainly we'll talk about the theory CI of "generalised type-free compositionality" with axioms that states that arbitrary ”blocks" of truth predicates commute with the logical constants. We show that CI proves the same theorems as FS without the rule CONEC.

**February 17:** *Zachiri McKenzie*: **A new lower bound on the consistency strength of a weak version of the Axiom of Counting. **

Let T be Jensen’s NFU with axiom of infinity, but without the axiom of choice. Let A be the axiom which says that no finite set is smaller than its own set of singletons. I will show that T+A proves the consistency of the Simple Theory of Types with Infinity (TSTI). Combined with the consistency proof of NFU this shows that T+A proves the consistency of NFU. Since T can be viewed as a subtheory of NF, this also gives a new lower bound on the consistency of NF+A which is better than any known lower bound on the consistency strength of NF.

**Mars 16: ***Paul Gorbow*: **Kripke-Joyal semantics for basic intuitionistic set theory**

We will look at a category theoretic analogue of the relationship between a set theory and an associated class theory (such as the relationship between ZF and NBG). The internal logic of a topos allows us to use set theoretic reasoning in it, but it only allows us to use quantifiers that are bounded by an object. To enable unbounded quantification, the notion of a category of classes has been introduced. Such a category is associated with a subcategory of sets, which turns out to be a topos. We also have that any topos embeds as the category of sets in a category of classes.

Categories of classes provide a sound and complete semantics for the first-order theory Basic Intuitionistic Set Theory (BIST), which accommodates both atoms and sets. BIST is a natural set theory, under which an arbitrary topos may be considered as a category of sets. In this seminar, we will outline the proof that categories of classes are sound for BIST.

**Mars 30: ***No seminar*

**April 13 (OBS! 10:15-12:00):** *Mateusz Łełyk and Bartosz Wcisło*: **On Comparing Strength of Various Theories of Truth (Part I)**

Our talk concerns axiomatic theories of truth. A theory of truth is an extension of a base theory B, which we may think of as a theory of syntax with some axioms governing a fresh predicate T(x) with the intended reading "x is a (code of a) true sentence". Our research revolves roughly around the following question: what assumptions make truth a substantial notion? There are several ways to make this question precise, one of which is the concept of (syntactic) conservativeness. It is one of the most important results in axiomatic theories of truth that the theory of truth based on classical compositional Tarskian axioms for arithmetical sentences yields a conservative extension over PA. On the other hand, one can readily show that if we add to this theory full induction for the formulae containing the truth predicate, then the resulting theory is no more conservative, since it proves e.g. the consistency of PA: It can be easily checked that the natural proof of non-conservativeness can be carried out already in the system with induction only for Σ_{1}-formulae containing the truth predicate.

We may restate our initial question in the following way: which natural extensions of the pure compositional axioms for the truth predicate cease to be conservative over PA and what are the relationships between these extensions with respect to their arithmetical strength?

It turns out that many different natural axioms governing the truth predicate give rise to theories of the same arithmetical strength. In our talk we will discuss a result stating that extensions of pure compositional truth over PA with any of the following principles share the same arithmetical consequences:

1. Induction scheme for Δ_{0}-formulae containing the truth predicate.

2. The global reflection principle: "Sentences provable from true premises in the first order logic are true".

3. The propositional reflection principle: "Sentences provable from true premises in the propositional logic are true".

4. The principle: "Tautologies of first order logic are true".

5. Disjunctive correctness: "A disjunction of arbitrary length is true if and only if some of its disjuncts is" together with the principle: "Axioms of Peano arithmetic are true"

The last part of our characterisation is even more surprising, once we know that by results of Enayat–Visser and Leigh the last principle alone, when added to the compositional axioms for the truth predicate yields a conservative extension of PA: Some of the above equivalences has been proved or follow from previous results proved by Cieśliński.

**April 13:** *Mateusz Łełyk and Bartosz Wcisło:* **On Comparing Strength of Various Theories of Truth (Part II)**

In the first talk we compare axiomatic truth theories with respect to how much new arithmetical sentences they prove. Another, more fine-grained, way to compare the logical strength of them is to look at their models. We shall say that Th is semantically no stronger than Th’ if every model of the base theory that expands to a model of Th’ can be expanded to a model of Th. We shall say that it is semantically weaker than Th’ if it is semantically no stronger, but there is a model of the base theory that can be expanded to a model of Th’ but cannot be expanded to a model of Th (notice that we cannot change the universe - we allow expanding a model - not extending it).

The philosophical reading of this definition is the following: we think about models of a theory as possible worlds allowed by this theory. If Th is weaker than Th’ then it means that Th’ precludes some possibilities which are allowed by Th. It puts more restrictions on the structure of universes possible from the point of view of the base theory. Let us note that, by a simple completeness argument, it is a refinement of the relation from the first part of our talk (we said there that Th is no stronger than Th’ if every consequence in the language of the base theory of Th follows also from Th’). Hence it can be used to compare axiomatic truth theories which has the same consequences in the language of the base theory. Let us recall, that for technical purposes we take PA to be our base theory. The good point to start is to look at truth theories that prove no PA unprovable arithmetical sentences. Such theories are said to be arithmetically conservative.

The interesting thing about arithmetically conservative truth theories is that they can be of very different syntactical shape. For example some of them are given by compositional axioms and allow no induction axioms for the truth predicate, others are axiomatized only by Tarski biconditional scheme, but admit full induction. We were interested whether differences in the character of those axioms project somehow onto their semantical strength. It turns out that they do.

We shall focus on the following arithmetically conservative, stratified (hence the truth predicate is defined only on arithmetical sentences) theories of truth:

1. 1. Purely disquotational, with full induction for the truth predicate: TB, UTB.

2. 2. Compositional and with no induction for the truth predicate: PT^{-}, CT^{-}.

3. 3. Compositional with a tiny bit of induction for the truth predicate: PTtot, PTint.

In our talk we shall define carefully all those theories and justify why comparing their strength is philosophically interesting. Putting together some previously known theorems and our own results we can show that some of them can be linearly ordered. For example PT^{-} is strictly weaker than TB, this one is strictly weaker than UTB and the last one in turn is no stronger than CT^{-}. If time permits, we will outline the most interesting steps in the proofs. At the end we shall state some problems that are still waiting to be resolved.

**April 27 (OBS 15:30): ***Maurice Chiodo**: ***The computational complexity of torsion for finitely presented groups**

Many algorithmic group properties have been shown to be unrecognisable amongst finitely presented groups. In this talk we will look at decision problems which have a complexity strictly harder than the halting set. In particular, we will analyse a standard construction of the Higman embedding theorem to show that:

1. The set of finite presentations of torsion-free groups is Π_{2} - complete in Kleene's arithmetic hierarchy.

2. There is a universal torsion-free finitely presented group; one into which all other finitely presented torsion-free groups embed.

3. A set of integers X appears as the set of orders of torsion elements in some finitely presented group if and only if X has a Σ_{2} description and is closed under multiplicative factors.

**May 4 (OBS! Joint seminar with theoretical philosophy, 10:15-12:00 in T340): ***Ed Zalta: ***Convergence in the Philosophy of Mathematics**

The Platonist answer to the question, "What is mathematical language about?", is that it is about abstract individuals (such as zero, the null set, omega, etc.) and abstract relations (such successor, less than, set membership, group addition, etc.), though the Platonist rarely has much to say about abstract relations. I describe what appears to be a Platonist foundation for mathematics by producing a formal, axiomatic theory of abstract individuals and abstract relations, and an analysis of mathematical language that yields denotations for the terms of mathematical theories and truth conditions for mathematical claims. After quickly reviewing the theory and its application to mathematics, I show how the formalism is subject to various interpretations. The Platonist interpretation is just one of several ways of interpreting the formalism and the analysis of mathematics. I develop fictionalist, structuralist, inferentialist, if-thenist, finitist, and logicist interpretations of the formalism. Since each interpretation offers us a clear, but different, answer to our initial question, the resulting analysis not only offers a way to make these philosophies of mathematics more precise, but also unifies them in a new and unsuspected way that explains why philosophers of mathematics often can’t even agree on the data.

**May 10 (OBS! Tuesday)(OBS! 11:00)(OBS! in T346)(OBS! via Skype): ***Greg Restall**: ***Terms for Classical Sequents: Proof Invariants and Strong Normalisation**

A proof for a sequent Σ⇒Δ shows you how to get from the premises to the Σ to the conclusions Δ. It seems very plausible that some valid sequents have different proofs. It also seems plausible that some different derivations for the one sequent don’t represent different proofs, but are merely different ways to present the same proof. These two plausible ideas are hard to make precise, especially in the case of classical logic.

In this paper, I give a new account of a kind of invariant for derivations in the classical sequent calculus, and show how it can formalise a notion of proof identity with pleasing behaviour. In particular, it has a confluent, strongly normalising cut elimination procedure.

**23/1: Ali Enayat** (Gothenburg) *Flexible Turing Machines *Suppose T is a consistent recursively enumerable extension of PA (Peano arithmetic). A TM (Turing machine) with program e is said to be T-flexible if for any given natural number m the theory T plus "the output of the TM with program e is precisely {m}" is consistent. T-flexible Turing machines were shown to exist by Kripke (1961); his work generalizes Mostwoski's notion of an independent-formula.

Recently Woodin (2011) introduced a new type of T-flexible Turing machine such that T proves:

(1) "the output of the TM with program e is finite", and

(2) for every countable model M of T and any M-finite set s extending the M-output of the TM with program e, there is an end extension N of M such that N satisfies T plus "the output of the TM with program e is precisely s".

In this talk I will (a) give an expository account of flexible TMs, and (b) present refinements of Woodin's theorem obtained in collaborative work of the author with A. Visser, V. Yu. Shavrukov, and R. Blanck.

**20/2: Zachiri McKenzie **(Gothenburg) *Universal-existential sentences in the simple theory of types with infinity*

This talk will report joint work done in collaboration with Anuj Dawar (University of Cambridge) and Thomas Forster (University of Cambridge).

The simple theory of types (TSTI) is a simplification, proposed independently by Ramsey and Chwistek, of the underlying system used in Russell and Whitehead’s Principia Mathematica. This theory apparently avoids the set theoretic paradoxes by partitioning the universe into types and only allowing sets at a given successor type to contain objects from the preceding type. It has been conjectured that TSTI decides every universal-existential sentence. In this talk I will show that every existential-universal sentence that is true in some model of TSTI is true in all models of TST (TSTI minus infinity) that are generated by a sufficiently large finite number of atoms. The talk will continue by identifying a class of universal-existential sentences such that if a sentence in this class is true in some model of TSTI then this sentence is true in all models of TST that are generated by a sufficiently large finite number of atoms. This shows that TSTI decides every universal-existential sentence in this class.

**6/3: Vladimir Yurievich Shavrukov **(Amsterdam)* **Sky-watching with applications*** **We present some recent developments in the study of prime filters on the lattice of r.e. sets. These include the total recursive sky structure of r.e. prime (aka cohesive) powers of N — the latter are what you get from r.e. prime filters by an ultrapower-like construction — and two applications to traditional recursion theory concerning r-maximal, hyperhypersimple and D-maximal r.e. sets. Based in part on joint work with James Schmerl.

**17/4: Thomas Forster** (Cambridge) *The Theory of Negative Types*

The Theory of Negative Types (TZT) is Simply Typed Set Theory with levels indexed by Z instead of N. Although it can be easily shown to be consistent by a compactness argument the models thus obtained are all pathological. This tour d'horizon will bring the reader up to speed with the history of this system, its connections with other theories, and present some recent work in which nicer models are obtained using *Omitting Types* constructions.

**17/4: Paul Gorbow** (OBS! 14:30-15:30) *A Monoidal Closed Category in N**F*

It is well known that the category of sets and functions in NF lacks a desirable category theoretic property called cartesian closedness. From within NF, we have considered a certain category jREL, obtained from the category REL. The objects of jREL are sets and its morphisms are relations R between the unions of the domain, A, and co-domain, B, respectively, such that jR restricts to a function from A to B, where jR = {(a, b) : (for all y) (y is in b if and only if there is x in a s.t. xRy)}. We claim that jREL is monoidal closed, and sketch how this is proved. Monoidal closedness is a slightly weaker property than cartesian closedness.

**29/5: Vladimir Kanovei **(Moscow)** ***Countable definable sets of reals and Vitali classes*

We shall discuss the following problems:

1. Given a non-empty definable set X of reals, does X necessarily contain a definable element?

2. What about countable definable sets X?

It will be shown that this problem is independent (in both forms), that is, it admits different solutions in different models of set theory. Some historical remarks will be made, and some related problems will be discussed, too.

**5/6: Valentin Goranko** (Stockholm) *On the theories of almost sure validities in the finite in some fragments of monadic second-order logic* (**OBS!** 13:15-15:00)

This work stems from the well-known 0-1 law for the asymptotic probabilities of first-order definable properties of finite graphs (in general, relational structures). Fagin's proof of this result is based on a transfer between almost sure properties in finite graphs and true properties of the countable random graph (aka, Rado graph). Both the transfer theorem and the 0-1 law hold in some non-trivial extensions of first-order logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic second-order (MSO).

The main problem of this study is to characterise, axiomatically or model-theoretically, the set of almost surely valid in the finite formulae of MSO, i.e. those with asymptotic probability 1. The set of almost sure validities in the finite of any given logical language (where truth on finite structures is well-defined) is a well-defined logical theory, containing all logical validities of that language and closed under all sound finitary rules of inference. Beyond that, little is known about these theories in cases where the transfer theorem fails.

The talk will begin with a brief introduction to asymptotic probabilities and almost surely true properties of finite graphs, the 0-1 laws for first-order logic and in some extensions of it, and their relationship with the respective logical theories of infinite random graphs. Then I will focus on the almost sure theories in modal logic and in the Σ^{1}_{1} and Π^{1}_{1} fragments of MSO on binary relational structures, aiming at obtaining explicit logical characterisations of these theories. I will present such partial characterisations in terms of characteristic formulae stating almost sure existence (Σ^{1}_{1}) or non-existence (for Π^{1}_{1}) of bounded morphisms to special target finite graphs. Identifying explicitly the set of target finite graphs that generate almost surely valid characteristic formulae seems a quite challenging problem, to which we so far only provide some partial answers and conjectures.

**10/6: Matt Kaufmann **(Austin)** ***ACL2: Implementation of a Computational Logic* (**OBS!** 13:15-15:00)

ACL2 ("A Computational Logic for Applicative Common Lisp") is a programming language, a first-order logic, and a software system for proving theorems in that logic. In this talk I will give logicians a sense of what ACL2 is, what can be done with it, and especially what sorts of logical issues can arise when attempting to build a powerful yet sound mechanized reasoning system.

**26/6: Albert Visser **(Utrecht) *Extension-Interpretability Degrees *In this talk I discuss some aspects of the Extension-Interpretability Degrees of finitely axiomatised theories. The ultimate aim of this research is to characterise the notion of sequential theory in terms of this degree structure.

We will explain the notions of:

• Locally Faithful Interpretability

• Local Tolerance

• i-Bisimilarity and the fragment G

We provide separating examples for Locally Faithful Interpretability, Faithful Interpretability and Interpretability. We show how to characterise the theories with the finite model property. We discuss the insight that on the sequential theories mutual interpretability and i-bisimilarity coincide.

**15/9: Bahareh Afshari** (OBS! Tuesday 13:15-15:00 in T346) *When formal proofs meet formal grammars *

Herbrand's seminal work from 1930 demonstrates how to reduce first-order logic to propositional logic. Herbrand's theorem, in its simplest form, states that if an existential formula Ǝx F(x) (with F quantifier-free) is valid then there exist terms t0, ... , tk such that F(t0) v...v F(tk) is a tautology. In this talk I will introduce a novel approach to Herbrand's theorem based on a recently discovered connection between proof theory and formal language theory. To a proof of a formula F in first-order logic one can associate a formal grammar that succinctly generates the terms needed to form a tautology from F. The approach not only captures Herband's theorem but also opens the door to tackle a number of questions in proof theory such as proof equivalence, proof compression and proof complexity which will be discussed.

**16/9: Graham Leigh** *The simple truth*** **The 'truth bi-conditionals' are the statements of the form ‘A <-> T[A]’ where A is a sentence, T is a predicate symbol and [A] denotes a name for A (e.g. Gödel code of A). Theories defined in terms of truth bi-conditionals are known to be deductively and conceptually simple. As observed already by Tarski, compositional truth principles, such as ‘for all sentences A, B: T[A & B] <-> T[A] & T[B]’, are not derivable from the basic bi-conditionals except in trivial cases. Nevertheless, many philosophers (e.g. Quine, Horwich, Williams) have proposed that the truth bi-conditionals are all there is to truth. In this talk I present proof-theoretic support for this extreme view and show how remarkably strong systems (both truth- and proof-theoretically) are implicit in very weak truth-theoretic assumptions.

**30/9: Zachiri McKenzie** *The largest initial segment of a model of set theory pointwise fixed by a non-trivial automorphism*

I will speak about research that has been done in collaboration with Ali Enayat and Matt Kaufmann.

The research I will speak about today investigates the first-order theory and structure of the largest initial segment of a model of a subsystem of ZFC that is pointwise fixed by a non-trivial automorphism. We will restrict our attention to models of MOST Set Theory, a subsystem of ZFC obtained by restricting collection to bounded formulae and separation to formulae in first level of the Levy hierarchy, that admit a non-trivial automorphism which hereditarily fixes the natural numbers. We will completely classify the first-order theory that holds in structures of the language of set theory that appear as the largest initial segment of a model of MOST which is pointwise fixed by a non-trivial automorphism that hereditarily fixes the natural numbers. We will also show that every countable transitive and countable recursively saturated model of MOST plus bounded-in-powerset collection can be realized as the largest initial segment of a model of MOST that is pointwise fixed by a non-trivial automorphism.

**11/11: Rasmus Blanck ***Illusory Models of Peano Arithmetic*** **In this talk, I present some highlights from the forthcoming paper Illusory Models of Peano Arithmetic by Makoto Kikuchi and Taishi Kurahashi.

The main objects of study are the sets Thm(M) = { a : M |= Pr(a) }, where M is a model of PA. We say that a model M is

(1) illusory, if Thm(M) contains a sentence that does not have a standard proof, and

(2) sane, if M satisfies Con(PA).

Since Thm(M) is the set of all sentences whenever M satisfies incon(PA), the illusory sane models are the most interesting ones in the present setting. I will give an overview of what is known about these models, sketch some proofs to give examples of methodology, and also discuss some open problems.

**25/11: Kit Fine ***Guide to Truthmaker Semantics*** **I will give a sketch of truthmaker semantics and consider its application to classical logic, intuitionistic logic and various forms of relevance logic.

**2/12: Paul Gorbow ***Set theoretic Foundations for Category theory*** **Right from the start, category theory faces foundational issues: How do we even obtain the existence of Grp = the category of groups, Top = the category of topological spaces, etc., that motivate the study in the first place? We will look at two semi-compatible statements of the whole foundational problem of category theory, one (R) suggested by Solomon Feferman and the other (S) implicit in an exposition by Michael Shulman. (R) asks for the unrestricted existence of the category of all groups, the category of all categories, the category of all functors between two categories, etc. (S) asks for a certain flexible distinction between large and small sets, where both enjoy the full benefits of the ZFC axioms. In this seminar we will assess Feferman’s proposed solutions to (R) and (S), with a focus on the needs they meet and the opportunities they provide for category theory. We will also speculate on a third solution, intended to attain the benefits of both.

Feferman’s proposed solution to (R), stems from the familiar fact that NFU allows for the construction of the set of all sets, and ultimately the category of all groups, the category of all categories, etc. However, NFU does not provide enough of a solution to (S), so Feferman proves the consistency of an extension of NFU that directly interprets ZFC by a constant. Zachiri McKenzie has just optimized the combinatorics of Feferman’s proof, thus proving the consistency of the theory from ZFC + 1 inaccessible.

A widely accepted partial (because inflexible) solution to (S) is chosen by Saunders Mac Lane in his standard reference “Categories for the Working Mathematician”, namely the theory ZFC + 1 inaccessible. Here the sets of rank less than the inaccessible are regarded as small. A similar full (i.e. flexible) solution to (S) due to Alexander Grothendieck, requires arbitrarily large inaccessibles. But Feferman observes that what category theory really needs, is already supplied by the reflection theorem in ZFC. By a simple trick he obtains a conservative extension of ZFC, which fully solves (S), albeit with a certain annoying consequence.

Lastly, we will speculate on whether NFUA (a natural extension of NFU) might provide a foundation that combines the best from both approaches. Robert Solovay showed that NFUA is equiconsistent with ZFC + for each natural number n there is an n-Mahlo cardinal.

**24/1: Ali Enayat** (Göteborg) *What can we gain from satisfaction classes? (part 1)*

This is a first of a series of talks on joint work with Albert Visser (Utrecht). The setting is as follows: we start with a sufficiently expressive "base theory" B formulated in a language L (such as B = Peano arithmetic, or B = Zermelo-Fraenkel theory), and then we extend B to a new theory B* consisting of B plus a set of sentences Σ formulated in the language obtained by adding a new binary predicate symbol S to L, where Σ expresses this or that natural feature of Tarskian satisfaction predicates over ω-models of B (i.e., models of B with no nonstandard integers). These talks aim to provide an overview of our current knowledge of the relationship between B and B* in connection with the following questions, for various choices of B and Σ:

(1) Is B* semantically conservative over B, i.e., does every model of B expand to a model of B*?

(2) Is B* syntactically conservative over B, i.e., if some L-sentence φ is provable in B*, then is φ provable in B?

(3) Is B* interpretable in B?

(4) What type of speed-up (if any) does B* have over B?

**31/1: Ali Enayat** (Göteborg) *What can we gain from satisfaction classes? (part 2)*

This part will first review fundamental model-theoretic results about recursively saturated models that are relevant to the study of axiomatic theories of truth, and then will concentrate on the relationship between PA and PA with a partial inductive satisfaction class (in relation with the four key questions specified in the abstract of part-1). Time permitting, I will also begin the discussion of the relationship between B and B with a full satisfaction class when B = ZF, and when B = PA.

**7/2: Anton Pertun Broberg** (Göteborg) *Infinite time computations*

Infinite Time Turing Machines (ITTMs) is a computational model that extends the Turing machine concept to transfinite ordinal length of time. In this talk ITTMs will be defined and some basic results will be shown, focusing on the `clockable ordinals', i.e. the length of certain infinite time computations. A stronger machine model, Cardinal Recognizing Infinite Time Turing Machines (CRITTMs), and the corresponding `clockable ordinals' will be examined as well.

**14/2: Ali Enayat** (Göteborg) *What can we gain from satisfaction classes? (part 3)*

This part will wrap up the discussion of the relationship between PA and PA with a partial inductive satisfaction class, and will begin discussing the relationship between B and B equipped a full satisfaction class, for arbitrary base theories B.

**21/2: Lawrence (Tin Lok) Wong** (KGRC, Vienna) *Internal and external counting in nonstandard models of arithmetic*

The interplay between internal and external counting is one of the most beautiful aspects of the model theory of nonstandard arithmetic. I will present a couple of classical examples around the regularity scheme, and mention some relevant ongoing work about cuts.

**7/3: Ali Enayat** (Göteborg) *What can we gain from satisfaction classes? (part 4)*

**14/3: Fredrik Engström** (Göteborg) *Implicit definability as a criterion for logicality?* In this tallk I will give background for, summary of, and comments on a text by Feferman from 2011 Which Quantifiers are Logical? A combined semantical and inferential criterion. The talk will be based on a similar talk I gave back in 2011, but with some more commentary and new ideas. I also hope to get help with some open questions related to the project.

**21/3: Rasmus Blanck** (Göteborg) *Formulae expressing the same property*

It is a widespread conception that arithmetical formulae express arithmetical properties, but it seems difficult to formulate criteria for when two formulae express the same property. Unfairly, the two extremist positions can be described in the following way: The extreme extensionalist claims that any two formulae that numerate the same set express the same property, while the opposing extremist holds that even A(x) and A(y) express different properties, since the formulae differ in their mode of presentation. In this talk I will discuss some problems that afflict even the less extreme positions, as well as the possibility of arriving at a more modest, but still coherent, position.

**4/4 (in T219): Anton Pertun Broberg** (Göteborg) *Arithmetical forcing*

**11/4: Anton Pertun Broberg **(Göteborg)* Arithmetical forcing, part II *

**25/4: Philip Welch** (Bristol) *Transfinite Computational Models*

In the last decade and half there has been a resurgence in studying our standard computational models, such as that if Turing Machine, Register machine etc, but allowing them to run transfinitely, so 'beyond omega'. In order to do this one has to make sense of limit stages in computational processes (with the finite successor step stage being just the usual Turing machine etc step.) We consider here the Infinite Time Turing Machines of Hamkins and Kidder, explaining in detail how these work, and how the standard Recursion and s-m-n theorems can be implemented in this context. We illustrate their relationship to various form of inductive definition, and the Goedel constructible hierarchy of sets. If time permits we intend to discuss the infinitary versions of Blum-Shub-Smale machines, which act directly on real numbers in finitely many registers. We indicate how they tie up with a form of Church-Turing thesis for polynomial time computation on omega-length strings.

**2/5 (10:15-12:00): Arianna Betti** (Göteborg / Amsterdam) *Polish Axiomatics and Its Truth*

Tarski's philosophical background in Warsaw was varied, and for some aspects also surprisingly far from present day's mainstream conceptions of logic and language. In this talk I survey some salient aspects of Tarski's Polish background, with particular attention for the history of Tarski's professional relationship with his supervisor, Stanislaw Lesniewski, an extraordinary and powerful figure, whose methodological rigor has no comparison in the history of logic. I focus on the divergence between Lesniewski's and Tarski's views on metamathematics, and Ajdukiewicz's influence upon the development of Tarski's views on the common concept of logical consequence and the definition of semantic notions. The Ajdukiewicz connection is also important, as it gives long sought-after evidence of the link between Bolzano's notion of Ableitbarkeit and Tarski's (logical) consequence. This is the paper forming the basis of this talk.

**23/5: Ali Enayat **(Göteborg) *Gödel's second incompleteness theorem and its generalizations.*

Gödel's second incompleteness theorem states that no sufficiently expressive consistent theory can prove its own consistency. In this talk I will first survey various proofs of this result, and then I will focus on generalizations of Gödel's second incompleteness theorem, including Pudlák's generalization that states that no sequential theory can even prove its own consistency on a "cut" of its natural numbers.

**16-18/6: JAF33**

**12/9: Kentaro Sato** (University of Bern) *Similarities and dissimilarities between second order number and set theory*

I overview similarities and dissimilarities between second order number theory (second order arithmetic) and second order set theory (class theory). ACA_{0} and Z_{2}, on the number theory side, correspond to NBG (von Neumann-Bernays-Goedel set theory) and MK (Morse-Kelley set theory), on the other side, respectively. We will see many dissimilarities among assertions that are, on number theory side, between ATR_{0} and Π^{1}_{1}-CA_{0}.

**26/9: Ali Enayat** (Göteborg)* Leibnizian themes in model theory and set theory *

I will begin with explaining Quine's four formulations of Leibniz's principle of identity of indiscernibles in his 1976-paper Grades of Discriminability. Then I will focus on some interesting results and open questions in model theory and set theory that are inspired by Leibniz's principle.

**10/10: Claes Strannegård **(Göteborg) *F**ormalizing Radical Constructivism*** **I will present a formalism and a program for learning and computing with bounded resources in symbolic domains. The program starts from scratch and gradually learns general rules of symbolic domains from specific examples. Thus it can learn e.g. simple arithmetic, propositional logic, and elementary grammar. The program searches for proofs with bounded resources and the axioms are not provided manually, but learned in a dynamic process subject to belief revision. The formalism contains elements of (1) constructivist epistemology, where theories are constructed from experience in a gradual process, (2) radical constructivism that focuses on viability of theories rather than truth, (3) bounded rationality that takes into account limited computational resources, (4) abstract term rewriting, and (5) introspection as a method for generating and testing hypotheses.

**24/10: Joan Rand Moschovakis** (13:15-15:00) **(Lindström lectures)** *Now Under Construction: Intuitionistic Reverse Analysis *Each variety of reverse mathematics attempts to determine a minimal axiomatic basis for proving a particular mathematical theorem. Classical reverse analysis asks which set existence axioms are needed to prove particular theorems of classical second-order number theory. Intuitionistic reverse analysis asks which intuitionistically accepted properties of numbers and functions suffice to prove particular theorems of intuitionistic analysis using intuitionistic logic; it may also consider the relative strength of classical principles which do not contradict intuitionistic analysis.

S. Simpson showed that many theorems of classical analysis are equivalent, over a weak system **PRA** of primitive recursive arithmetic, to one of the following set existence principles: recursive comprehension, arithmetical comprehension, weak Konig's Lemma, arithmetical transfinite recursion, Π^{1}_{1} comprehension. Intermediate principles are studied also. Intuitionistic analysis depends on function existence principles: countable and dependent choice, fan and bar theorems, continuous choice.

The fan and bar theorems have important mathematical equivalents. W. Veldman, building on a proof by T. Coquand, recently showed that over intuitionistic two-sorted recursive arithmetic **BIM** the principle of open induction is strictly intermediate between the fan and bar theorems, and is equivalent to intuitionistic versions of a number of classical theorems. Intuitionistic logic separates classically equivalent versions of countable choice, and it matters how decidability is interpreted. R. Solovay recently showed that Markov's Principle is surprisingly strong in the presence of the bar theorem. The picture gradually becomes clear.

**24/10****:**** Yiannis Moschovakis** (15:30-17:15) **(Lindström lectures)** *The logical form and meaning of attitudinal sentences*

The language **L** over a fixed vocabulary K is an (applied) * typed λ-calculus* with additional constructs for *acyclic recursion* and * attitudinal application*, an extension of Montague's *Language of Intensional Logic* **LIL** as formulated by Daniel Gallin. It is denotationally interpretable in the classical typed λ-calculus over K, but intensionally richer: in particular, it can define the *referential intension* of each term A, an abstract algorithm which computes the denotation of A and provides a plausible explication of its meaning.

The key mathematical construction of **L** is an effective *reduction calculus* which compiles each term A into an (essentially) unique *canonical form* cf(A), a denotational term which explicates the *logical form* of A and from which the referential intension of A can be read off. The central open problem about **L** (over a finite, interpreted vocabulary) is the * decidability of global synonymy* – and it is a problem about the classical, interpreted typed λ-calculus.

**7/11: Anton Pertun Broberg **(Göteborg)** ***Formalizing (deflationary?) truth *I will look at consequences of adding truth as an operator to first order logic (instead of as a predicate in the base theory), together with allowing for ´sentence quantification'.

**21/11: Kerkko Luosto **(University of Tampere)** ***Problems arising from branching of generalized quantitiers.*

Branching of quantifiers is a regularly recurring theme in logic. Its modern treatment can be traced back to Henkin or branching quantifiers (Henkin 1959). An important work on Henkin quantifiers is the paper of Blass and Gurevich (1986) relating them to complexity theory and second order logic; it is also known that they form a hierarchy (Hella 1989 etc.).

Most interesting is, however, that the idea of braching has re-appeared in many various forms ,e.g., Hintikka has strongly advocated the independence logic, and Väänänen introduced the dependence logic. And in linguistics, it was realized that not only the branching of existential and universal quantifiers is important, but the idea can be adapted to branching of generalized quantifiers (Keenan 1979, Westerståhl, Keenan).

I shall concentrate on the case of branching of generalized quantifiers, developing some facts and observations related to the subject matter. The main point is to raise some open problems that might be worth studying.

**5/12: ****Thierry Coquand** (Göteborg) *Univalent foundation and constructive mathematics*

This talk will be a general introduction to Voevodsky's program of providing a foundation of mathematics based on type theory. The main insight is that dependent type theory provides a good system of notations for representing directly the notion of (weak) omega-groupoid/homotopy types. This point of view suggests a stratification of types in propositions, sets, groupoids, … Type theory appears in this way to be a generalization of set theory. It also suggests the axiom of univalence, which corresponds to Church's axiom of extensionality for propositions in simple type theory. I will try to explain how this approach solves some basic issues in constructive mathematics.

The logic seminar takes place on alternate Thursdays between 13:15 and 15:00 at Olof Wijksgatan 6 in room T 307 (unless otherwises stated).

The archive of older seminars (starting 2005) is divided into two web pages: 2005-2013 Logic Seminars and 2014-2017.