Research seminars prior 2020

The archive of seminars from 2005 to 2019 is divided into two pages. Below you will find all Logic Seminars from 2019 back to 2014. Schedules from earlier years, 2005 until 2013, are available on this page.

Seminar listings from 2020 onwards are found on the main seminar page.

2019 Autumn

6 September (Room T340) Ali Enayat (FloV) Some recent news about truth theories

Abstract: This talk is an expanded version of the talk I recently presented at the Logic Colloquium 2019 (Prague). I will report on the following two recent developments in the axiomatic study of truth theories. Item (1) resulted from my collaboration with Fedor Pakhomov (Steklov Institute, Moscow); while item (2) arose from my joint work with Mateusz Łełyk and Bartosz Wcisło (both from the University of Warsaw).

The nonconservativity of CT^-[PA] + DC over PA, where CT^-[PA] is the extension of PA (Peano arithmetic) with CT^- (compositional theory of truth without extra induction), and DC is the axiom stating that a finite disjunction is true iff one of its disjuncts is true.
Feasible reducibility of certain truth theories (including CT^-[PA]) to PA. A corollary of this result is that such truth theories exhibit at most polynomial speed-up over PA.

4 October (T340) Moa Johansson (Chalmers) Theory Exploration and Automated Induction

Abstract: Theorem provers typically work by reasoning from a given set of facts, searching for a proof of a given conjecture. But what about situations where there are missing lemmas? This can be the case if we’re trying to automating proofs by induction, as we don’t necessarily have cut elimination. Theory exploration is a technique for inventing new and interesting mathematical conjectures, given a set of functions, constants and datatypes. I will show a demo of a system called Hipster, which not only automatically generates new conjectures (using testing), but also tries to prove them automatically, and finally assesses if the proof was interesting enough to motivate showing it to the human user.

18 October (T340) Colin Zwanziger (Carnegie Mellon University) 3 Myths about Predicate Modal Logic

Abstract: Predicate modal logic has been controversial at least since the criticisms of Quine. While predicate modal logic is now accepted, questions remain about its formulation, which has been hampered by several myths. Among these are:

In the context of a modal operator, substitution of equals for equals fails.
In the context of a modal operator, ordinary quantifier rules such as existential generalization fail.
De re is the result of a modal operator occurring inside the scope of a quantifier or other scope-taking operator.

Applying lessons from modal type theory (Bierman and de Paiva 2000, Pfenning and Davies 2001, etc.), I argue for the following countervailing principle: A. In the context of a modal operator, all free variables will receive de re interpretation, and should be marked as such.

Where this is implemented (e.g. Zwanziger 2017), the rules for equality and quantifiers finally become unproblematic (as demanded by Quine), and de re is more evidently decoupled from scope taking operators. Further refinements should avoid Myths 1-3 by adhering to Principle A, roughly speaking.

1 November (T340) Daichi Hayashi (Hokkaido) On complete cut-elimination of several axiomatic theories of truth

Abstract: In this talk, I give cut-elimination arguments for compositional theories of truth, to obtain other proofs of their proof-theoretic strengths. Firstly, following Leigh and Rathen’s cut-elimination arguments, I discuss Friedman-Sheard theory (FS) and then apply the method to the analysis of typed theories. Secondly, I consider Kripke-Feferman theory (KF) with the consistency axiom (Cons); however, there is room for improvement in that my proof basically depends on Cantini’s original argument and thus it (partially) requires a model-theoretic procedure.

15 November (T340) Anton Broberg (FLoV) Friedman-Sheard and Co-Necessitation

Abstract: The axiomatic theory of truth commonly known as FS (for Friedman-Sheard) has two rules, NEC and CONEC (originally called T-Intro and T-Elim), that allows you to conclude Tr(A) if you have proven A, respectively allows you to conclude A if you have proven Tr(A).

In this talk we will outline a proof of that CONEC is an admissible rule in FS. First, we show that we can put some restrictions on the proofs of FS without limiting the strength of FS. This makes it possible to reformulate the original problem (is CONEC admissible in FS?) to an equivalent, slightly more manageable problem: can FS without CONEC prove anything that FS without NEC can?

We take on this reduced problem by taking a detour into an infinitary system of truth. We show a partial cut-elimination result for this system and we show that within ”reasonable” proof lengths we can embed FS without NEC in this (almost) cut-free, system. Eventually, with a formalised soundness argument for the infinitary system, within the theory FS without CONEC, we show that FS without CONEC can indeed show everything FS without NEC can, and the main result follows.

This is joint work with Graham Leigh.

29 November (T340) Ana María Mora Marquez (FLoV) What Is Formal In Aristotle’s Syllogistics?

Abstract: Using Dutilh-Novaes’ and MacFarlane’s taxonomies of the formal in relation to logic, and an additional one by myself, I intend to assess the ways, if any, in which Aristotle’s syllogistic in his Prior Analytics can be said to be ‘formal’. I conclude that it can be said to be formal primarily in relation to a mechanistic intention.

2019 Spring

24 January (Room 112, Dicksonsgatan 4) Graham E. Leigh (FLoV) Iterating self-applicable truth

7 February (Room T340): Informal meeting

7 March (T219) Peter Pagin (Stockholm) Indexicality and time

Abstract: In this talk, I shall briefly present the Switcher Semantics framework and the related idea of general compositionality. I shall then move on to David Kaplan’s arguments that we need to postulate temporal propositions, true/false at world-time pairs, as the meanings-in-context of some natural language sentences, more precisely sentences with temporal context dependence. Kaplan’s arguments concern the rejection of vacuous temporal operations and the compositionality of content, that is, meaning-in-context.

I shall present the arguments, some of the reactions to them in the literature (if there is time), and the Switcher Semantics solution. I will finally consider the question whether validity in Kaplan’s Logic of Demonstratives is preserved in the switcher semantics for these sentences.

21 March (T340) Devdatt Dubhashi (Chalmers) Independence Results in Machine Learning

Abstract: The celebrated results in the foundations of Mathematics by Goedel and Cohen showed that statements such as the Axiom of Choice (AC) and the Continuum Hypothesis (CH) were independent of standard (ZF) Set Theory. Recent results have shown that surprisingly such results also bedevil machine learning. Although machine learning is identified in the popular imagination as a practical engineering field, there is in fact a well developed underlying statistical theory which also guides practical applications. Some basic statements on learnability in this framework turn out to be independent of set theory just as AC and CH are. We will give an introductory survey of independence results in general and on these recent results in machine learning in particular.

4 April (T340) Graham E Leigh When proofs become grammars

Abstract: I will present some recent results from structural proof theory linking automated theorem proving to formal language theory. Using this idea, the existence of (simple) proofs by induction is equivalent to the existence of tree grammars covering particular term languages. This seminar is intended as an informal follow-up on some applications of learning theory brought up in Devdatt Dubhashi’s talk two weeks ago. The results I will be presenting are due to the research group in mathematics at TU Wien, specifically recent work of Stefan Hetzl and Sebastian Eberhard.

2 May (T346) Paul Gorbow (FloV) The reflective multiverse of set theory

Abstract: I present a construction of a model of an expansion of set theory. It embodies a conception of a multiverse of universes of set theory, with an untyped notion of truth-relative-to-a-universe. The construction is partly motivated by the philosophical concern of the significance of having proofs from the axioms of a set theory such as ZF. Here are three potential answers to this question:

(Universe) The conclusions of proofs from ZF are true about sets.
(Multiverse) The conclusions of proofs from ZF are true in every structure/universe satisfying ZF.
(Formal foundation) For a proof p from ZF to gain significance it needs to be interpreted in a particular mathematical theory or structure founded in ZF, e.g. as establishing a truth about the real numbers.

I will argue that the these three viewpoints can coexist and, together, motivate a construction I call the Reflective Multiverse, an expansion of ZF by a primitive notion of truth-relative-to-a-universe. In this talk I will explain the construction and detail some of the philosophical story behind it. As this is work in progress, I’m keen to receive feedback.

16 May Departmental conference

23 May (Room 112, Dicksonsgatan 4) Anders Lundstedt (Stockholm) Necessarily non-analytic induction proofs

Abstract: Sometimes when trying to prove a fact F by induction one gets “stuck” when trying to prove the induction step. The solution is sometimes to instead prove a “stronger” fact S by induction. This proof method is usually called something like “strengthening of the induction hypothesis”. However, there need not always be a precise sense in which the fact S is “stronger”. Thus, following Hetzl and Wong (2018), we use the more general terminology “non-analytic induction proofs” for such proofs. A natural question for such proofs is whether the non-analyticity is necessary—that is, whether one could prove F without the “detour” via proving S. Hetzl and Wong have made precise sense of this question for first-order theories and sentences of arithmetic. Based on this, we investigate whether some particular induction proofs are necessarily non-analytic. This is joint work with Eric Johannesson.

Reference: Stefan Hetzl and Tin Lok Wong (2018). “Some observations on the logical foundations of inductive theorem proving”. Logical Methods in Computer Science 13.4, pp. 1–26.

30 May no seminar (public holiday).

2018 Autumn

27 Sep Volker Halbach (Oxford). Room T340! Classical and determinate truth (joint work with Kentaro Fujimoto)

Abstract: We present an axiomatic theory of truth over PA formulated in the language of arithmetic with two new unary predicate symbols D and T. The axioms for truth state that truth commutes with connectives and quantifiers for the entire language. Moreover we have an axiom schema stating the T-sentences for all determinate sentences. Determinacy is expressed by the symbol D, which is also axiomatized. The axioms allow for serious interaction between truth and determinacy.

We argue that this system satisfies several requirements that make the theory very useful. In particular, we argue that it can alleviate some worries Kreisel had about the model-theoretic definition of logical consequence.

A proof-theoretic analysis of system shows that it is slightly stronger than the Kripke-Feferman theory of truth or ramified analysis up to ε0.

11 Oct Bahareh Afshari (FLoV & CS). Room: T340! Nested sequents for the modal mu-calculus

Abstract: Modal logic provides an effective language for expressing properties of state-based systems. When equipped with operators that can test for infinite behaviour like looping and reachability, the logic becomes a powerful tool for specifying correctness of nonterminating reactive processes such as communication protocols and control systems. An elegant example of such a logic is the modal mu-calculus which extends basic modal logic by two quantifiers for defining inductive and co-inductive operators.

In this talk I will introduce the modal mu-calculus and present a complete proof system for it based on nested sequents. We will see how the proof system can be used to obtain both old and new results for the mu-calculus and its extensions.

25 Oct Sven-Ove Hansson (KTH) Choosing the objects of (epistemic) choice Abstract. In traditional belief revision theory, the epistemic agent is assumed to make choices either among possible worlds or among maximally consistent subsets (“remainders”) of logically closed sets representing the belief state. This is cognitively unrealistic, and some of the problematic properties of the traditional models are directly connected with these constructions of choice. An alternative model, in which choices are made among potential belief states, is shown to avoid most of the problems associated with the traditional models.

8 Nov Jakub Szymanik (Amsterdam) Ease of learning explains semantic universals Abstract: Despite extraordinary differences between natural languages, linguists have identified many semantic universals – shared properties of meaning – that are yet to receive a unified explanation. We analyze universals in a domain of content words (color terms) and a domain of function words (quantifiers). Using tools from machine learning, we show that meanings satisfying attested universals are easier to learn than those that are not. Thus, ease of learning can explain the presence of semantic universals in many different linguistic domains.

22 Nov Andrea Vezzosi (Chalmers) Cubical Agda and its Implementation

Abstract. Cubical Type Theory (CTT) [1] gives a computational interpretation to the univalence axiom [2]. It also supports function extensionality and higher inductive types and can be extended with other extensionality principles, like bisimulation as equality for coinductive types.

Cubical Agda is the extension of the proof assistant Agda with the features from Cubical Type Theory. Agda is a feature rich language and interactive editing environment, whose implementation spans around 100k lines of Haskell code. In this talk I will present how CTT has been adapted to better fit the language and implementation of Agda, while still maintaining soundness with regard to the denotational model.

[1] Cubical Type Theory: a constructive interpretation of the univalence axiom. arXiv

[2] Homotopy Type Theory: Univalent Foundations of Mathematics. arXiv

5 Dec Ali Enayat (FloV). How far is a truth theory from its base?

Abstract. In the first part of the talk, I will review some basic results about conservativity and interpretability of truth theories in relation to their base theory. In the second part, I will report on recent joint work with Mateusz Łełyk and Bartosz Wcisło on feasible proof-theoretic reduction of the following theories to PA:

(1) Compositional truth over PA (with no extra induction);

(2) Friedman-Sheard truth over PA (with no extra induction); and

(3) Kripke-Feferman truth over PA (with no extra induction).

6 Dec Gothenburg–Warsaw Workshop on Truth See workshop page for details.

2018 Spring

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 Σ1 definable but does not necessarily form a set.

This talk goes a step higher up in the logical complexity and is centered around fixed points of monotone Σ1 operators. We are interested in their logical structure, and in order to get a hold of that we also look at some related principles. This approach provides some interesting insight concerning the size of our universe.

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

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

2017 Spring

27 January Paul Gorbow (FLoV, Gothenburg) Algebraic Set Theory for NF and some of its variants

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) Intuitionistic Ramified Type Theory

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) Compositional vs Game-Theoretic Semantics for the Alternating-Time Temporal Logic ATL

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) Indefiniteness, definiteness and semi-intuitionistic theories of sets

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) Team semantics for logics with generalized quantifiers

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

2017 Autumn

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)

Abstracts for talks are on the Lindström Lectures webpage.

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.

2016

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

Abstract: 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

Abstract: 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)

Abstract: 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:

Induction scheme for Δ0-formulae containing the truth predicate.
The global reflection principle: “Sentences provable from true premises in the first order logic are true”.
The propositional reflection principle: “Sentences provable from true premises in the propositional logic are true”.
The principle: “Tautologies of first order logic are true”.
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)

Abstract: 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:

Purely disquotational, with full induction for the truth predicate: TB, UTB.
Compositional and with no induction for the truth predicate: PT-, CT-.
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

Abstract: 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:

The set of finite presentations of torsion-free groups is Π2 - complete in Kleene’s arithmetic hierarchy.
There is a universal torsion-free finitely presented group; one into which all other finitely presented torsion-free groups embed.
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

Abstract: 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

Abstract: 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.

2015

23/1 Ali Enayat (Gothenburg) Flexible Turing Machines

Abstract: 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/: 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 NF

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:

Given a non-empty definable set X of reals, does X necessarily contain a definable element?
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 Σ11 and Π11 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 (Σ11) or non-existence (for Π11) 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.

2014

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). ACA0 and Z2, 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 ATR0 and Π11-CA0.

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) Formalizing 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, Π11 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.

2013 and earlier

The archive of older seminars (2005–2013) is available on a separate page.

Logic@GU