Mohammad Ardeshir

Sharif University of Technology

We re-evaluate the standard proof interpretation Brouwer-Heyting-Kolmogorov (BHK). That leads to the new constructive Basic Logic, properly contained in Intuitionistic Logic.

Johan van Benthem

University of Amsterdam & Tsinghua University

Dependence is ubiquitous in science and daily life. We present a simple complete and decidable classical base logic for reasoning about functional dependence which can be seen as either a generalized first-order logic or as a modal logic interpreted epistemically. Next, we consider extensions for reasoning about correlations between variables, where the base logic for independence turns out to be undecidable. We end by enriching the framework with topological structure and continuous dependence.

This is joint work with Alexandru Baltag.

References.
Alexandru Baltag & Johan van Benthem, A Minimal Logic of Functional Dependence, Journal of Philosophical Logic, 2021. --,
Continuous Dependence and Varieties of Knowability, in progress.

Ali Enayat

University of Gothenburg

In 1975 Barwise and Schlipf published a landmark paper which launched the study of recursively saturated models of arithmetic; the main theorem of their paper asserts that a nonstandard model M of Peano Arithmetic is recursively saturated iff M can be expanded to a model of a particular subsystem of Second Order Arithmetic. The impression one gets from reading the Barwise-Schlipf paper is that the left-to-right direction of the theorem is deep since it relies on sophisticated techniques from admissible set theory and infinitary languages, and that the other direction is fairly routine. In hindsight, we can say that the exact opposite is the case: the left-to-right direction of the theorem lends itself to a relatively easy proof from first principles, but the right-to-left direction is the deep one. In this talk I will provide some background history, discuss a serious gap in the original 1975-proof of the right-to-left direction, and explain how the gap can be circumvented using a line of reasoning very different from the original one. This talk is a report of joint work with Jim Schmerl.

Lev D. Beklemishev

Steklov Mathematical Inistitute

We deal with the fragment of propositional modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. We call such fragments strictly positive. Strictly positive logics recently attracted attention both in the description logic and in the provability logic communities for their combination of efficiency and sufficient expressivity. Moreover, strictly positive logics allow for alternative interpretations that are quite natural from a proof-theoretic point of view.

We consider a series of modalities representing the operators associating with a given arithmetical theory \(T\) its fragment axiomatized by all theorems of \(T\) of arithmetical complexity \(\Pi^0_n\), for all \(n>0\). We note that such operators, in a strong sense, cannot be represented in the full language of modal logic. We formulate the corresponding  system of strictly positive provability logic and study its properties.

We show that in this system one is able to express iterations of reflection principles up to any ordinal \(<\epsilon_0\). Secondly, we provide normal forms for its variable-free fragment. Thereby, this fragment is shown to be algorithmically decidable and complete w.r.t. its natural arithmetical semantics. We also characterize its Lindenbaum--Tarski algebra and its dual Kripke structure. The elements of this algebra correspond to the sequences of proof-theoretic \(\Pi^0_{n+1}\)-ordinals of bounded fragments of Peano arithmetic called \emph{conservativity spectra}, as well as to the points of the well-known Ignatiev Kripke model.