Abstracts

Sergei Artemov — "New Foundations of Epistemic Logic"

All three pillars on which Epistemic Logic rests: modal language, Kripke-style semantics, and proof theory, need modernization.

  1. Modal language alone does not support such central topics in Epistemology as “knowledge vs. justified true belief” discussion, due to a lack of justifications as logical objects.
  2. Kripke semantics of possible worlds for epistemic logic is based on a hidden assumption of common knowledge of the model, CKM, manifested in the condition “if a sentence is valid at all possible states, then it is known.” In social scenarios, however, agents may possess asymmetric knowledge of the situation and CKM as a uniform assumption should be resisted. What we need here is a new theory of epistemic modeling in a general setting without assuming common knowledge of the model.
  3. A well-principled notion of epistemic theory as an axiomatic description of a given scenario incorporated into the possible worlds environment is conspicuously absent. Moreover, given an informal verbal description of a situation, a typical epistemic user cherry-picks a “natural model” and simple-mindedly regards it as a formalization of the original description, i.e. uses a model in lieu of a theory and ignores the fact that there might be many different “natural models” of the same description. In this respect, a systematic confusion of a theory and a model in Epistemic Logic resembles the pre-Goedelian state of mathematical logic, without a clear distinction between theories and models.
Situation in (1) is gradually improving with the introduction of Justification Logic but there is still a long way to go. In this talk, we outline a modernization program for (2) and (3). We introduce epistemic models which do not rely on CKM, and a matching framework of hypertheories for epistemic reasoning with partial information.

Michael Bärtschi — "Theories around Γ0"

(Joint work with Gerhard Jäger)

In the first part of the talk we will consider subsystems of second order arithmetic resulting from extending ACA0 with certain axiom schemas. We will sketch that these theories are equivalent to ATR0, i.e., ACA0 with the schema of arithmetic transfinite recursion.

In the second part we turn to set theories for admissible sets above the natural numbers as urelements with induction principles of varying strength. Of particular interest will be schemas of Σ and Π reduction. In order to establish the strengths of these theories we will make use of proof-theoretic methods and Simpson's suitable trees (see [1]).

  [1] Stephen G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, Cambridge University Press, 2009.

Andrey Bovykin — "The struggle for infrastructure: how unprovability proofs emerge and how they end"

I am going to take upon myself a difficult technical task of exploring an as-yet unarticulated topic, of which no stable philosophy exists but intuitions are ripe and ready.

What lies beyond the swamp of decidable stuff without infrastructure and the situations where unprovability kicks in?

Examples include questions like "When does MDRP phenomenon kick in?" "Which theories don't have recursive models?" "Can one build a model with a lot of induction without having some, even poor, induction on the ground?" "Can one build a model of a lot of comprehension without having a bit of comprehension on the ground?" "How to get something strong (for example Σ1-induction) from innocent mathematical bits? (Friedman's new spectacular Strict Reverse Mathematics)". The list can go on and on.

Sometimes the answer is provided by very strong known techniques: indiscernibles of various kinds or (set-theoretic) Reflection Principles. In high set-theoretic situations we know how ultrafilters or embeddings bring strength. Often the answer is unclear and the obstacles can be thought of as difficulties in coding. Here, the thresholds between coding and non-coding are number-theoretic in nature and we are lost.

I will give three recent examples:

  1. with a lot of infrastructure available - how to obtain strong unprovability by coloring countable ordinals (a clear but naive example);
  2. emergence of strength when considering all possible theories of some kinds (some assembled theories will be weak but some unexpectedly strong, often using L-like constructions that avoid all pillars of L);
  3. how indiscernibles give strength despite extremely poor infrastructure on the ground (example suggested to me by Harvey Friedman).

If time allows, I will quickly survey recent news from the world of Unprovability research.

Ulrik Buchholtz — "Homotopy type theory and operational systems"

I shall give a report on recent developments in homotopy type theory, and then speculate on future directions, including relationships between homotopy type theory and operational systems.

Lev Gordeev — "Continuity in weak constructive set theories"

Brouwer-Markov-Ceitin continuity theorems illuminate the most specific feature of constructive/recursive analysis. The well-known proofs use different ideas and formalisms like those underlying (mutually incompatible) Brouwer's fan theorem and Kleene's partial recursive functions. However, there is a more general set theoretic solution that can be easily formalized in basic weak constructive (extensional) set theory extended by an axiom saying, loosely speaking, that there exist enumerable but not decidable sets of natural numbers. By standard methods, this corresponds to analogous interpretation in Feferman's (intensional) applicative theory of functions and classes. This also raises proof theoretic conservativity problems of resulting formalisms over standard intuitionistic/constructive arithmetical formalisms.

Lukas Jaun — "Category Theory in Explicit Mathematics"

I will talk about some progress made in formalizing Category Theory in general and the category of sets in particular in Explicit Mathematics.

Reinhard Kahle — "Mahloness in Explicit Mathematics"

(Joint work with Anton Setzer)

We discuss two different versions of introducing Mahlo universes in Explicit Mathematics; in particular, an "extended predicative" version is presented which allows for an induction principle for a Mahlo universe.

Elena Nogina — "On Reflection Principles and Iterated Consistencies"

We consider reflection principles comprising proof and/or provability predicates in Peano Arithmetic. Every such principle is shown to be provably equivalent to either local reflection or an iterated consistency assertion.

Wolfram Pohlers — "A note on the limits of predicativity"

Call an ordinal attainable if it is a hereditarily transitive set whose well–foundedness can be "secured from below". Call it pre–attainable if all its predecessors are at- tainable. It has been shown by Schütte that no strongly critical ordinal is attainable. Schütte and Feferman have independently shown that the attainability of ω entails the pre–attainability of Γ0.

In this talk we sketch a slight generalization of the Schütte–Feferman theorem and ask the question whether there are philosophical reasons which corroborate the role of Γ0 as the limit of predicativity.

Kentaro Sato — "Conservations of second order Σ11collection and Σ11closure"

Making-a-detour method was introduced by the speaker with Zumbrunnen in their 2015 paper. This allows us to interpret classical theories in classical ones via intuitionistic theories, by combining three interpretations: Goedel-Gentzen negative interpretation; Coquand-Hofmann-Avigad forcing interpretation; and various kinds of realizability interpretation. With this method, ultrafinitistic proofs of the lowerbounds have previously been given to choiceless operational set theory and explicit mathematics T0.

Second order Σ11collection and Σ11closure schemata are variants of Σ11-AC and Σ11-DC and, in the presence of arithmetical (elementary) comprehension, they are equivalent. With the making-a-detour method with respective variants of realizability interpretation, we will give ultrafinitistic proofs (with concrete interpretations) to the following conservations:

(1) both WKL0 + Σ11collection and WKL0 + Σ11closure are Π12conservative over WKL0 with van Oosten's Lifschitz-style functional realizability;

(2) Δ11-CA0 + Σ11collection is Π12conservative over Δ11-CA0 and Δ11-CA0 + Π1n+1induction + Σ11closure is Π12conservative over Δ11-CA0 + Π1n+1induction with newly developed hyperarithmetical realizability.

In (1) WKL0 can be replaced with WKL*0, and any Π11axiom can be added in (1) and (2).

Note that (1) implies the Π11conservations of RCA0 + Σ11collection and of RCA0 + Σ11closure over RCA0, because of the famous conservation of WKL0.

Whereas (2) itself is a very famous result that has been proved in various ways, what (the speaker thinks) is new is the concrete interpretation for (2) and the provability in the ultrafinitistic meta-theory. This implies that there is no speed-up beyond polynomial-time between the theories.

Silvia Steila — "Fixed point statements in the locally predicative and impredicative spotlights"

(Joint work with Gerhard Jäger)

Given a monotone function on a complete lattice the least fixed point is defined as the minimum among the fixed points. This is an impredicative definition, as it ranges over a totality to which the entity being defined (i.e. the least fixed point) belongs. Tarski Knaster Theorem states that every monotone function on a complete lattice has a least fixed point.

There are two standard proofs of Tarski Knaster Theorem. The first one exploits the fact that given a monotone function F on a complete lattice "the least fixed point is the intersection of all sets which are closed under F". Since the fixed point z is closed under F (i.e. F(z) is a subset of z), this property can be consider as an alternative impredicative definition of the least fixed point. The second one is based instead on the inductive definition by stages (i.e. Iα = F(∪β<α Iβ)), which can be considered as a locally predicative definition of the least fixed point (i.e. "there exists an ordinal alpha such that z = Iα and F(Iα)=Iα"), at least if the definition clause is arithmetic .

Over ZFC the powerset of the natural numbers (P(ω)) is not only a set but also a complete lattice, and Tarski Knaster Theorem holds for it. If we move to weaker set theories (e.g., extensions of Kripke Platek Set Theory (KP)) in which we avoid in particular the powerset axiom, Tarski Knaster Theorem for P(ω) might turn out to be unprovable.

In the first part of the talk we summarise some results obtained in this direction over a conservative second order extension of KP, by showing that the difference between the "locally predicative" and "impredicative" arguments plays a crucial role in term of provability of the corresponding principles. In the second part we are going to focus on the problems which arise by comparing the proof theoretic strength of such principles, presenting some new directions to be explored.

James Walsh — "Hierarchies of proof-theoretic strength"

It is well-known that natural axiomatic theories are well-ordered by proof-theoretic strength, for various popular metrics of proof-theoretic strength. However, without a precise mathematical definition of "natural," it is unclear how to prove this, or even how to state it. We will discuss two approaches to explaining this phenomenon, both of which emphasize the role of iterated reflection principles. The first approach is from joint work with Antonio Montalbán; the second approach is from joint work with Fedor Pakhomov.